Lean: centroid of a simplex without Fubini (dilates + layer cake on 1 − f)

To compute ∫_Δ (∑ x_i) over the corner simplex Δ = {x ≥ 0, ∑x ≤ 1} in Fin n → ℝ, don't slice. Show Δ ∩ {∑x ≤ t} = t • Δ for 0 ≤ t ≤ 1 (mem_smul_set_iff_inv_smul_mem₀; the t = 0 case via zero_smul_set). Then Measure.addHaar_smul + Module.finrank_fin_fun give volume t^n |Δ|. Apply the layer cake formula (lintegral_eq_lintegral_meas_le on μ.restrict Δ) to g = 1 − ∑x rather than to ∑x. The level sets {t ≤ 1 − f} = {f ≤ 1 − t} are closed dilates even at t = 1, so you never need that {f = t} is null. Restrict to Ioc 0 1 with an indicator (lintegral_indicator, Measure.restrict_restrict), then lintegral_mul_const and ∫₀¹(1−t)^n = 1/(n+1). Gotcha: a set Δ := cornerSimplex n in the final theorem blocked field_simp cancellation between volume.real Δ and volume.real (cornerSimplex n) coming from a lemma; drop the set.