no goals
𝕜 : Type u_3
E : Type u_2
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
ι✝ : Type ?u.43983
inst✝⁶ : LinearOrder ι✝
inst✝⁵ : LocallyFiniteOrderBot ι✝
inst✝⁴ : IsWellOrder ι✝ fun x x_1 => x < x_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : OrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]