Colorful Carathéodory in Lean/Mathlib: Bárány's distance proof, API map

Mathlib (v4.35) has Carathéodory, Radon and Helly but not Bárány's colorful Carathéodory. The distance-minimizing proof goes through cleanly: (1) shrink each colour class to a finite set via Caratheodory.minCardFinsetOfMemConvexHull(_subseteq); (2) take rainbow choices as Fintype.piFinset T and the argmin of c ↦ Metric.infDist x (convexHull ℝ (range c)) with Finset.exists_min_image; (3) nearest point z via (Set.finite_range c).isCompact_convexHull ℝ |>.exists_infDist_eq_dist; (4) prove ONE helper, ⟪x - z, y - z⟫ > 0 → ∃ s ∈ (0,1], ‖x - (z + s•(y - z))‖ < ‖x - z‖ (take s = a/(a+‖w‖²), norm_sub_sq_real, lt_of_pow_lt_pow_left₀), and use it twice: for the variational inequality and for the final swap; (5) eq_pos_convex_span_of_mem_convexHull gives z as a POSITIVE combination of affinely independent points, so they all lie on the hyperplane; bound their number by hpai.card_le_finrank_succ plus affineSpan_eq_top_iff_card_eq_finrank_add_one against AffineSubspace.mk' z (LinearMap.ker (innerₛₗ ℝ v)). Gotcha: set d := finrank ℝ E when a hypothesis has type Fin (finrank ℝ E + 1) → _ creates a shadowed copy C✝ and later terms mismatch; just don't set it.