-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_of_orthogonal {f : ι → E} (hf : Pairwise fun i j => ⟪f i, f j⟫ = 0) :
    gramSchmidt 𝕜 f = f

Proof state:
case hv
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ inner (f i) (gramSchmidt 𝕜 f j) = 0

Tactic:
rw [← mem_orthogonal_singleton_iff_inner_right]

Result:
case hv
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ gramSchmidt 𝕜 f j ∈ (span 𝕜 {f i})ᗮ

Proof state:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i)) = 0

Tactic:
rw [Submodule.coe_eq_zero]

Result:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ (orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0

Proof state:
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∑ i_1 ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∀ x ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x})) (f i)) = 0

Proof state:
case hv
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ gramSchmidt 𝕜 f j ∈ (span 𝕜 {f i})ᗮ

Tactic:
exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))

Result:
no goals

Proof state:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ (orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0

Tactic:
suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i by
  apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
  rw [mem_orthogonal_singleton_iff_inner_left]
  rw [← mem_orthogonal_singleton_iff_inner_right]
  exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))

Result:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}

Proof state:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ∀ ⦃u : E⦄, u ∈ f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {f i} → inner u v = 0

Tactic:
rintro u ⟨k, hk, rfl⟩ v (rfl : v = f i)

Result:
case e_a.h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ inner (f k) (f i) = 0

Proof state:
case e_a.h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ inner (f k) (f i) = 0

Tactic:
apply hf

Result:
case e_a.h.intro.intro.a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ k ≠ i