-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_orthogonal (f : ι → E) {a b : ι} (h₀ : a ≠ b) :
    ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    0

Tactic:
by_cases h : gramSchmidt 𝕜 f a = 0

Result:
case pos
𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
h : gramSchmidt 𝕜 f a = 0
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    0

case neg
𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    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 ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0

Tactic:
rcases h₀.lt_or_lt with ha | hb

Result:
case inl
𝕜 : 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
ha : a < b
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0

case inr
𝕜 : 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
hb : b < a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ inner (gramSchmidt 𝕜 f i) (f b) / ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0

Tactic:
simp only [mul_eq_zero, div_eq_zero_iff, inner_self_eq_zero]

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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ (inner (gramSchmidt 𝕜 f i) (f b) = 0 ∨ ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) = 0) ∨
    inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0

Proof state:
case inr
𝕜 : 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
hb : b < a
⊢ inner (gramSchmidt 𝕜 f b) (gramSchmidt 𝕜 f a) = 0

Tactic:
exact this _ _ hb

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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      ∑ x ∈ Iio b,
        inner (gramSchmidt 𝕜 f x) (f b) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f x) =
    0

Tactic:
rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr h₀)]

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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    0

𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ ∀ b_1 ∈ Iio b,
    b_1 ≠ a →
      inner (gramSchmidt 𝕜 f b_1) (f b) / ↑(‖gramSchmidt 𝕜 f b_1‖ ^ 2) *
          inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b_1) =
        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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ ∀ b_1 ∈ Iio b,
    b_1 ≠ a →
      inner (gramSchmidt 𝕜 f b_1) (f b) / ↑(‖gramSchmidt 𝕜 f b_1‖ ^ 2) *
          inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b_1) =
        0

Tactic:
intro i hi hia

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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ inner (gramSchmidt 𝕜 f i) (f b) / ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f 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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ (inner (gramSchmidt 𝕜 f i) (f b) = 0 ∨ ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) = 0) ∨
    inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0

Tactic:
right

Result:
case 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0