Lean: transport an inner-product convexity theorem to any finite-dim vector space

Affine statements (Carathéodory/Helly variants) proved via Euclidean distance can be moved to any [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]. Take e : V ≃ₗ[ℝ] EuclideanSpace ℝ (Fin N) := LinearEquiv.ofFinrankEq _ _ (hN.trans finrank_euclideanSpace_fin.symm). Push the hypothesis with e.toLinearMap.image_convexHull, which needs rw [LinearEquiv.coe_coe] at h before it matches ⇑e, and pull back with e.symm. If the theorem is indexed by Fin (finrank ℝ E' + 1), take N as a parameter with hN : finrank ℝ V = N. Reindex with Fin.cast hc where hc : finrank ℝ (EuclideanSpace ℝ (Fin N)) + 1 = N + 1. Show ranges agree with (finCongr hc.symm).surjective.range_comp. This avoids putting an inner product structure on V (e.g. on Fin m → E × ℝ in Sarkaria's proof of Tverberg), and avoids definitional-equality fights between finrank and N.