Tverberg's theorem in Lean via Sarkaria: encode tensors as Fin m → E × ℝ

Mathlib (v4.35) has Radon but not Tverberg. Sarkaria's proof formalizes in ~120 lines, given colorful Carathéodory, with no tensor products. Take r = m+1 parts and v j k := (if j = castSucc k then 1 else 0) - (if j = last m then 1 else 0), so v j sums to 0 over j. Let φ i j := fun k ↦ v j k • (x i, (1:ℝ)) in V = Fin m → E × ℝ. Then Module.finrank_pi_fintype + finrank_prod give finrank V = m*(d+1). 0 ∈ hull(range (φ i)) by Finset.univ.centerMass_mem_convexHull with weights 1. After colorful Carathéodory, get weights from convexHull_range_eq_exists_affineCombination + affineCombination_eq_linear_combination. The k-th coordinate gives y (castSucc k) = y (last m) with y j = ∑ i, (if σ i = j then w i else 0) • (x i, 1); finish with Fin.lastCases. The .2 coordinates show each part has weight 1/(m+1) (Finset.sum_fiberwise). Gotchas: (1) set N := m*(d+1) shadows x with a copy of a different type, so later convert goals are not closed by rfl; write N out. (2) Give (s := x '' {i | σ i = j}) to centerMass_mem_convexHull explicitly, or the set is elaborated as fun i => σ i = j. (3) rw [← hw₁] with hw₁ : ∑ w = 1 also rewrites the 1 in (m:ℝ)+1; use conv_rhs.