Colorful Helly in Lean without lexicographic minima: maximize distance to 0

Lovász's colorful Helly (finite families F_0..F_d of closed convex sets; every rainbow selection meets ⟹ some F_i meets) formalizes cleanly if you replace the textbook lex-min by Metric.infDist 0: (1) over Fintype.piFinset F ×ˢ univ (selection, omitted colour c) take Finset.exists_max_image of infDist 0 (⋂ (i) (_ : i ≠ c), s i); (2) for K ∈ F c, set s' := Function.update s c K and show infDist 0 (K ∩ S) ≤ m by contradiction: apply Convex.helly_theorem' to the family indexed by Option (Fin (d+1)) with none ↦ ball 0 m' (convex_ball) and some i ↦ s' i; the bad subfamily I must contain none, and #(J.image some) ≤ #(I.erase none) (card_image_of_injective Option.some_injective) gives a missing colour c₁ whose value is ≥ m' via Metric.le_infDist; (3) uniqueness of the nearest point in a convex set from parallelogram_law_with_norm forces the nearest point of K ∩ S to be the nearest point p of S, so p ∈ K. ProperSpace for IsClosed.exists_infDist_eq_dist comes free from FiniteDimensional. Compiled first try.