-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_inv_triangular (v : ι → E) {i j : ι} (hij : i < j) :
    ⟪gramSchmidt 𝕜 v j, v i⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ k < i

Tactic:
simpa using hki'

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j) (gramSchmidt 𝕜 v i) +
      ∑ x ∈ Iio i,
        inner (gramSchmidt 𝕜 v x) (v i) / ↑‖gramSchmidt 𝕜 v x‖ ^ 2 * inner (gramSchmidt 𝕜 v j) (gramSchmidt 𝕜 v x) =
    0

Tactic:
set b : ι → E := gramSchmidt 𝕜 v

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ inner (b j) (b i) + ∑ x ∈ Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j) (v i) = 0

Tactic:
rw [gramSchmidt_def'' 𝕜 v]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j)
      (gramSchmidt 𝕜 v i +
        ∑ i_1 ∈ Iio i, (inner (gramSchmidt 𝕜 v i_1) (v i) / ↑‖gramSchmidt 𝕜 v i_1‖ ^ 2) • gramSchmidt 𝕜 v i_1) =
    0

Proof state:
case h.e'_2.h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ inner (b j) (b i) = 0

Tactic:
exact gramSchmidt_orthogonal 𝕜 v hij.ne'

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
this : inner (b j) (b k) = 0
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0

Tactic:
have hki : k < i := by simpa using hki'

Result:
case h.e'_2.h.e'_6.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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j)
      (gramSchmidt 𝕜 v i +
        ∑ i_1 ∈ Iio i, (inner (gramSchmidt 𝕜 v i_1) (v i) / ↑‖gramSchmidt 𝕜 v i_1‖ ^ 2) • gramSchmidt 𝕜 v i_1) =
    0

Tactic:
simp only [inner_add_right, inner_sum, inner_smul_right]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j) (gramSchmidt 𝕜 v i) +
      ∑ x ∈ Iio i,
        inner (gramSchmidt 𝕜 v x) (v i) / ↑‖gramSchmidt 𝕜 v x‖ ^ 2 * inner (gramSchmidt 𝕜 v j) (gramSchmidt 𝕜 v x) =
    0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ inner (b j) (b i) + ∑ x ∈ Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0

Tactic:
convert zero_add (0 : 𝕜)

Result:
case h.e'_2.h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ inner (b j) (b i) = 0

case h.e'_2.h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ∑ x ∈ Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0

Proof state:
case h.e'_2.h.e'_6.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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0

Tactic:
have : ⟪b j, b k⟫ = 0 := gramSchmidt_orthogonal 𝕜 v (hki.trans hij).ne'

Result:
case h.e'_2.h.e'_6.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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
this : inner (b j) (b k) = 0
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0

Proof state:
case h.e'_2.h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ∑ x ∈ Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case h.e'_2.h.e'_6.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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ∀ x ∈ Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0