-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_orthogonal (f : ι → E) {a b : ι} (h₀ : a ≠ b) :
    ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0

Proof state:
case neg.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
h : ¬gramSchmidt 𝕜 f a = 0
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) ≠ 0

Tactic:
rwa [inner_self_ne_zero]

Result:
no goals

Proof state:
case h.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
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
hia₁ : i < a
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f a) = 0

Tactic:
exact ih a h₀ i hia₁

Result:
no goals

Proof state:
case h.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
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
hia₁ : i < a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0

Tactic:
rw [inner_eq_zero_symm]

Result:
case h.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
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
hia₁ : i < a
⊢ inner (gramSchmidt 𝕜 f i) (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
b : ι
⊢ ∀ a < b, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0

Tactic:
apply wellFounded_lt.induction b

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 : ι
⊢ ∀ (x : ι),
    (∀ y < x, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0) →
      ∀ a < x, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f x) = 0

Proof state:
case h.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
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
hia₂ : a < i
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0

Tactic:
exact ih i (mem_Iio.1 hi) a hia₂

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
a b : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0

Tactic:
revert a

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 : ι
⊢ ∀ a < b, 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
⊢ ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0

Tactic:
intro a b 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
a b : ι
h₀ : a < b
⊢ 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 : ι
⊢ ∀ (x : ι),
    (∀ y < x, ∀ a < y, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0) →
      ∀ a < x, inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f x) = 0

Tactic:
intro b ih a 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) (gramSchmidt 𝕜 f b) = 0

Proof state:
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

Tactic:
exact this _ _ ha

Result:
no goals

Proof state:
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

Tactic:
rcases hia.lt_or_lt with hia₁ | hia₂

Result:
case h.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
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
hia₁ : i < a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0

case h.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
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
hia₂ : a < i
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0