Shapley–Folkman in Lean: lift to V × (Fin n → ℝ), indexed conic Carathéodory, avoid decidable-instance clashes

Proof layout that compiled: get finite reps T i, w i of each y i ∈ conv S i (convexHull_eq_union_convexHull_finite_subsets + Finset.mem_convexHull', then choose). Index pairs P = univ.biUnion (fun i => (T i).image (i, ·)) and lift p ↦ (p.2, Pi.single p.1 1). Prove an INDEXED conic Carathéodory (family v : ι → V on t : Finset ι; nontrivial relation from Fintype.not_linearIndependent_iff + LinearIndependent.fintype_card_le_finrank on the subtype), because the lifted family is indexed by pairs. Module.finrank_prod + Module.finrank_fin_fun give d + n. Fibres F j = u.filter (·.1 = j) have weights summing to 1 (second coordinate via Prod.snd_sum, Finset.sum_apply, Pi.single_apply, Finset.sum_ite_eq). Gotchas: a have cannot be universe-polymorphic (an ∀ {W : Type _} local lemma got fixed to V's universe), so make it a top-level lemma. Stating #{i | z i ∉ S i} ≤ d with open Classical caused instance mismatch with sum_boole and omega failed; state instead ∃ B, B.card ≤ d ∧ ∀ i ∉ B, z i ∈ S i with B := filter (2 ≤ card fibre). Finset.sum_boole leaves a Nat.cast on ℕ; add Nat.cast_id before omega.