awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
mp :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
have mpr : (‖v‖ = 1 ∧
    (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0) →
  (‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
    (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
      Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
mp :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mpr :
  (‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0) →
    (‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
have mp₁ : ‖Matrix.vecCons v vs 0‖ = 1 →
  (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
    (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
      (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
        ‖v‖ = 1 ∧
          (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
mp :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mpr :
  (‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0) →
    (‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0
mp₁ mp₂ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ‖v‖ = 1 ∧
            (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
have mp₃ : ‖Matrix.vecCons v vs 0‖ = 1 →
  (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
    (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
      (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) → ‖v‖ = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
mp :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mpr :
  (‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0) →
    (‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0
mp₁ mp₂ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ‖v‖ = 1 ∧
            (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mp₃ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) → ‖v‖ = 1
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
have mp₄ : ‖Matrix.vecCons v vs 0‖ = 1 →
  (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
    (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
      (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
        ∀ (i : Fin n), ⟪v, vs i⟫ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
mp :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mpr :
  (‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0) →
    (‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0
mp₁ mp₂ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ‖v‖ = 1 ∧
            (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mp₃ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) → ‖v‖ = 1
mp₄ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ∀ (i : Fin n), ⟪v, vs i⟫ = 0
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
have mp₅ : ‖Matrix.vecCons v vs 0‖ = 1 →
  (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
    (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
      (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
        ∀ (i : Fin n), ‖vs i‖ = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
mp :
  ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mpr :
  (‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0) →
    (‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0
mp₁ mp₂ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ‖v‖ = 1 ∧
            (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
mp₃ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) → ‖v‖ = 1
mp₄ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ∀ (i : Fin n), ⟪v, vs i⟫ = 0
mp₅ :
  ‖Matrix.vecCons v vs 0‖ = 1 →
    (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
        (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
          ∀ (i : Fin n), ‖vs i‖ = 1
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧
      (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
have mp₆ : ‖Matrix.vecCons v vs 0‖ = 1 →
  (∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) →
    (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) →
      (Pairwise fun (i j : Fin n) ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) →
        Pairwise fun (i j : Fin n) ↦ ⟪vs i, vs j⟫ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
h : Orthonormal 𝕜 v
i : ι
this : (↑‖v i‖₊ : ℝ) = 1
⊢ ‖v i‖₊ = 1
have norm_cast : ∀ (this : ‖v i‖₊ = 1), ‖v i‖₊ = 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
h : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖₊ = 1
have suffices : (↑‖v i‖₊ : ℝ) = 1
Tactic: suffices (‖v i‖₊ : ℝ) = 1 by norm_cast at this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
h : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖ₑ = 1
have rw : ENNReal.ofReal ‖v i‖ = 1
Tactic: rw [← ofReal_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
have mp : Orthonormal 𝕜 v → ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
mp : Orthonormal 𝕜 v → ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
have mpr : (∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) → Orthonormal 𝕜 v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0
have pos : ∀ (h : i = j), ⟪v i, v j⟫ = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
pos : ∀ (h : i = j), ⟪v i, v j⟫ = 1
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j), ⟪v i, v j⟫ = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ Orthonormal 𝕜 v
have mpr : ∀ (i : ι), ‖v i‖ = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
mpr : ∀ (i : ι), ‖v i‖ = 1
⊢ Orthonormal 𝕜 v
have mpr₁ : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
have rw : (re : (a : 𝕜) → ℝ) (if i = i then 1 else 0) = HPow.hPow (α := ℝ) (β := ℕ) 1 2
Tactic: rw [@norm_sq_eq_re_inner 𝕜, h i i]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ = 1
have h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
Tactic: have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by
        rw [@norm_sq_eq_re_inner 𝕜, h i i]; simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ ‖v i‖ = 1
have h₁ : 0 ≤ ‖v i‖
Tactic: have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
h₁ : 0 ≤ ‖v i‖
⊢ ‖v i‖ = 1
have h₂ : LE.le (α := ℝ) 0 1
Tactic: have h₂ : (0 : ℝ) ≤ 1 := zero_le_one
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : HPow.hPow (β := ℕ) ‖v i‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
h₁ : 0 ≤ ‖v i‖
h₂ : LE.le (α := ℝ) 0 1
⊢ ‖v i‖ = 1
have mpr : ∀ (h' : ‖v i‖ = 1) (h₁ : 0 ≤ ‖v i‖) (h₂ : LE.le (α := ℝ) 0 1), ‖v i‖ = 1
Tactic: rwa [sq_eq_sq₀ h₁ h₂] at h'
Cleared hypotheses: h', h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq E
s : Set E
⊢ Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) ↔
    ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0
have rw : (∀ (i j : { x : E // x ∈ s }), ⟪(↑i : E), (↑j : E)⟫ = if i = j then 1 else 0) ↔
  ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0
Tactic: rw [orthonormal_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ ⟪(linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l, v i⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜)
have rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
Tactic: rw [← inner_conj_symm, hv.inner_right_finsupp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
rw :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
⊢ ⟪(linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l, v i⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜)
have rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
Tactic: rw [← inner_conj_symm, hv.inner_right_finsupp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, l₁ i • v i) (∑ i ∈ s, l₂ i • v i) =
    ∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)
have simp_rw : Eq.{u_1 + 1} (α := 𝕜)
  (∑ x ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ x) : 𝕜) ⟪v x, ∑ i ∈ s, l₂ i • v i⟫)
  (∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i))
Tactic: simp_rw [sum_inner, inner_smul_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ x ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ x) : 𝕜) ⟪v x, ∑ i ∈ s, l₂ i • v i⟫)
    (∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i))
have refine : ∀ (i : ι) (hi : i ∈ s),
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) ⟪v i, ∑ i ∈ s, l₂ i • v i⟫ =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) ⟪v i, ∑ i ∈ s, l₂ i • v i⟫ =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)
have rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i) =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)
Tactic: rw [hv.inner_right_sum l₂ hi]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
⊢ LinearIndependent 𝕜 v
have rw : ∀ (l : ι →₀ 𝕜), Eq.{u_2 + 1} (α := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l : E) (0 : E) → l = 0
Tactic: rw [linearIndependent_iff]