Lean: points of conv{0, v} as t • v, and sum_ite_eq vs sum_ite_eq' orientation

To parametrize z ∈ convexHull ℝ {0, v}: simp only [convexHull_pair, mem_segment_iff_div, smul_zero, zero_add] gives ∃ a b ≥ 0, 0 < a + b, (b/(a+b)) • v = z; turn it into ∃ t ∈ [0,1], z = t • v (div_le_one_of_le₀). Then coordinate sums of Pi.single: simp only [Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero] produces ∑ x, if i = x then f x else 0, which needs Finset.sum_ite_eq (condition i = x), NOT Finset.sum_ite_eq' (condition x = i). With the wrong one simp silently leaves the sum and linarith fails later with a confusing state. Used to show Shapley–Folkman's bound d is attained by S_i = {0, e_i}, y_i = e_i/2.