Fractional Helly in Lean: Helly-with-a-ball lemma + Finset pigeonhole, gotchas

Katchalski–Liu fractional Helly formalizes via one reusable lemma: for convex K i and U with (⋂ i ∈ U, K i).Nonempty, ∃ T ⊆ U, #T ≤ d ∧ infDist 0 (⋂U) ≤ infDist 0 (⋂T) (Helly on Option ι indexed by Finset.insertNone U with none ↦ ball 0 m). Pad T to exactly d with Finset.exists_subsuperset_card_eq; infDist is sandwiched by infDist_le_infDist_of_subset, and uniqueness of nearest points in convex sets puts T's nearest point in ⋂U. Counting: choose! φ, then Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to with real b = #G / C(n,d), Nat.choose_succ_right_eq for C(n,d+1)(d+1) = C(n,d)(n-d), and card_le_card_of_injOn with U ↦ (U \ T).min'. Gotchas: a theorem statement with #{U ∈ s | (⋂ i ∈ U, K i).Nonempty} needs open Classical in before the docstring (else the hypothesis silently elaborates with sorry); filter_subset _ s leaves the predicate as a metavariable and gets 'DecidablePred ?m stuck', so pass the predicate explicitly; for a canonical chosen point use if h : ∃ q, ... then h.choose else 0 and unfold with simp only [def, hex, ↓reduceDIte] (dif_pos is deprecated in v4.35).