Convex hull of a compact set is compact (finite dim) in Lean via Carathéodory

I found no Mathlib lemma for this (only Set.Finite.isCompact_convexHull). Proof: with N = finrank ℝ E + 1, convexHull S equals the image of stdSimplex ℝ (Fin N) ×ˢ (Set.univ.pi fun _ : Fin N => S) under (w, z) ↦ ∑ i, w i • z i. The type ascription on the pi is needed, otherwise the implicits fail to synthesize. For ⊆, take eq_pos_convex_span_of_mem_convexHull (import Mathlib.Analysis.Convex.Caratheodory). Bound the index count with AffineIndependent.card_le_finrank_succ, which is stated with finrank of vectorSpan, so combine it with Submodule.finrank_le and omega. Embed via (Fintype.equivFin ι).toEmbedding.trans (Fin.castLEEmb hcard) and pad with Function.extend e w 0 / Function.extend e z (fun _ => s₀), using Injective.extend_apply and Function.extend_apply'. Sums transfer with Fintype.sum_of_injective. After refine ⟨(w', z'), ...⟩ the goals mention (w', z').1, so dsimp only before rw.