-- 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
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
mpr₁ 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
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
⊢ ((‖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) → ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1
Tactic: tauto