-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_orthonormal {f : ι → E} (h₀ : LinearIndependent 𝕜 f) :
    Orthonormal 𝕜 (gramSchmidtNormed 𝕜 f)

Proof state:
case right
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0

Tactic:
repeat' right

Result:
case right.h.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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0

Proof state:
case right
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0

Tactic:
simp only [gramSchmidtNormed, inner_smul_left, inner_smul_right, RCLike.conj_inv,
  RCLike.conj_ofReal, mul_eq_zero, inv_eq_zero, RCLike.ofReal_eq_zero, norm_eq_zero]

Result:
case right
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0

Proof state:
case left
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
⊢ ∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1

Tactic:
simp only [gramSchmidtNormed_unit_length, h₀, eq_self_iff_true, imp_true_iff]

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
h₀ : LinearIndependent 𝕜 f
⊢ (∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1) ∧
    Pairwise fun i j => inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0

Tactic:
constructor

Result:
case left
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
⊢ ∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1

case right
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
⊢ Pairwise fun i j => inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0

Proof state:
case right
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
⊢ Pairwise fun i j => inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0

Tactic:
intro i j hij

Result:
case right
𝕜 : 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0

Proof state:
case right.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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f i = 0 ∨ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0

Tactic:
right

Result:
case right.h.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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0

Proof state:
case right.h.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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0

Tactic:
exact gramSchmidt_orthogonal 𝕜 f hij

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
h₀ : LinearIndependent 𝕜 f
⊢ Orthonormal 𝕜 (gramSchmidtNormed 𝕜 f)

Tactic:
unfold Orthonormal

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
h₀ : LinearIndependent 𝕜 f
⊢ (∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1) ∧
    Pairwise fun i j => inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0