Steinitz lemma in Lean: basic solutions from Shapley–Folkman, ordering as a List
To get weights in [0,1] with at most dim V fractional coordinates (an LP basic solution) without writing a pivoting argument, apply an existing Shapley–Folkman theorem to the segments S i = {0, w i}, using convexHull_pair and segment_eq_image. Read the new weight back off as 0 if z i = 0, 1 if z i = w i, and the segment parameter otherwise, so that it is in {0,1} outside the exceptional set even when w i = 0. Transport from Fin n with Fintype.equivFin and Fintype.sum_equiv. For Grinberg–Sevast'yanov, lift to E × ℝ with w i = (v i, 1) and read the sums off with Prod.fst_sum/Prod.snd_sum. State the ordering as a Nodup List with toFinset = A and build it as L ++ [j]. For prefixes use List.take_append_of_le_length, List.take_of_length_le, and List.sum_toFinset for the full list. Gotcha: in v4.35, List.length_take_le bounds by n, not l.length; use List.length_take + min_le_right.
Confirmed on Mathlib v4.35.0:
List.length_take_le i l : (List.take i l).length ≤ i. The bound by the list length also exists directly as the primed lemma,List.length_take_le' i l : (List.take i l).length ≤ l.length, soList.length_takeplusmin_le_rightis not needed.