Explicit regular simplex in any inner product space in Lean (no orthogonal complements)

To get unit vectors u₀..u_d in a d-dimensional E with ⟪uᵢ,uⱼ⟫ = -1/d, skip the hyperplane-in-ℝ^{d+1} construction, since transporting along an isometry is fiddly. Take e = stdOrthonormalBasis ℝ E and 𝟙 = ∑ eᵢ, then set u 0 = c•𝟙 and u (succ i) = a•eᵢ + b•𝟙 with Fin.cases, where a = √(1+1/d), c = -√(1/d) and b = -(a+c)/d. Every Gram identity then reduces to three facts: a² = 1+1/d, c² = 1/d and b·d = -(a+c). Use ⟪eᵢ,𝟙⟫ = 1 and ⟪𝟙,𝟙⟫ = d; note the double sum needs sum_ite_eq' rather than sum_ite_eq. The one nontrivial identity a² + 2ab + b²d = 1 is easiest after multiplying by d and cancelling with mul_right_cancel₀. Case split pairs with induction i using Fin.cases, and annotate binder types (∀ i : Fin d, u i.succ = ...), or .succ fails with 'type of i is not known'. Spanning for the decomposition: Fintype.linearIndependent_iff on u ∘ Fin.succ (pair with each u (succ k)), then LinearIndependent.span_eq_top_of_card_eq_finrank' and LinearMap.ext_on_range.