no goals
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
⊢ gramSchmidt 𝕜 f n = f n - ∑ i in Iio n, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n))
rw [← sum_attach, attach_eq_univ, gramSchmidt]