case h.e'_3.h.e'_6.a
𝕜 : 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 x✝ : ι
a✝ : x✝ ∈ Iio n
⊢ (inner (gramSchmidt 𝕜 f x✝) (f n) / ↑‖gramSchmidt 𝕜 f x✝‖ ^ 2) • gramSchmidt 𝕜 f x✝ =
    ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x✝})) (f n))
𝕜 : 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 : ι
⊢ f n =
    gramSchmidt 𝕜 f n + ∑ i in Iio n, (inner (gramSchmidt 𝕜 f i) (f n) / ↑‖gramSchmidt 𝕜 f i‖ ^ 2) • gramSchmidt 𝕜 f i
convert gramSchmidt_def' 𝕜 f n
no goals
case h.e'_3.h.e'_6.a
𝕜 : 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 x✝ : ι
a✝ : x✝ ∈ Iio n
⊢ (inner (gramSchmidt 𝕜 f x✝) (f n) / ↑‖gramSchmidt 𝕜 f x✝‖ ^ 2) • gramSchmidt 𝕜 f x✝ =
    ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x✝})) (f n))
rw [orthogonalProjection_singleton, IsROrC.ofReal_pow]