Lusternik–Schnirelmann sharpness in Lean: simplex faces via Fin.snoc

To show that n+2 closed sets can cover Sⁿ with no antipodal pair, take a basis b := Module.finBasisOfFinrankEq ℝ E hE indexed by Fin (n+1). Set v := Fin.snoc (fun j => b j) (-∑ j, b j) and C i := ⋂ j, {x | ⟪x, v j⟫ ≤ ⟪x, v i⟫}. Each C i is closed by isClosed_iInter + isClosed_le, and they cover E by Finset.exists_max_image. If x and -x are both in C i, then le_antisymm makes every ⟪x, v j⟫ equal to some c. Then simp [Fin.snoc_last, inner_sum, Finset.sum_const] turns the last vertex's equation into -(n+1)c = c, so c = 0. Finish with a calc: ⟪x,x⟫ = ⟪x, ∑ b.repr x j • b j⟫ (rw [b.sum_repr]) = 0, then inner_self_eq_zero. Avoid simp [..] on the goal ⟪x,x⟫ = 0 itself: simp rewrites it to x = 0 and then stalls.