𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
rw [gramSchmidt_def' 𝕜 f i]
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i +
      ∑ x in Finset.Iio i, (inner (gramSchmidt 𝕜 f x) (f i) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
simp_rw [orthogonalProjection_singleton]
no goals
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i +
      ∑ x in Finset.Iio i, (inner (gramSchmidt 𝕜 f x) (f i) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
exact Submodule.add_mem _ (subset_span <| mem_image_of_mem _ hij)
  (Submodule.sum_mem _ fun k hk => smul_mem (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) _ <|
    subset_span <| mem_image_of_mem (gramSchmidt 𝕜 f) <| (Finset.mem_Iio.1 hk).le.trans hij)