awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ B n i j ≤ 0
have simp : LE.le (α := ℤ)
  (if i = j then 2
  else
    if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1 else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
  0
Tactic: simp only [B, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0
have pos : i = j → LE.le (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0
have pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0
have neg : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
neg : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0
have pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
neg : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then if (↑j : ℕ) = n - 1 then -2 else -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
    0
have neg₁ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ C n i j ≤ 0
have simp : LE.le (α := ℤ)
  (if i = j then 2
  else
    if (↑i : ℕ) + 1 = (↑j : ℕ) then -1 else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
  0
Tactic: simp only [C, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0
have pos : i = j → LE.le (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0
have pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0
have pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → (↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → LE.le (α := ℤ) (-1) 0
pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → (↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0
have neg : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → ¬(↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) → LE.le (α := ℤ) (-1) 0
pos₂ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → (↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-2) 0
neg : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → (↑j : ℕ) + 1 = (↑i : ℕ) → ¬(↑i : ℕ) = n - 1 → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) then -1
      else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
    0
have neg₁ : ¬i = j → ¬(↑i : ℕ) + 1 = (↑j : ℕ) → ¬(↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ D n i j ≤ 0
have simp : LE.le (α := ℤ)
  (if i = j then 2
  else
    if n ≤ 2 then 0
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
      else
        if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
        else
          if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
          else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
  0
Tactic: simp only [D, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have pos : i = j → LE.le (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have pos₁ : ¬i = j → n ≤ 2 → LE.le (α := ℤ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → n ≤ 2 → LE.le (α := ℤ) 0 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have pos₂ : ¬i = j → ¬n ≤ 2 → (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → n ≤ 2 → LE.le (α := ℤ) 0 0
pos₂ : ¬i = j → ¬n ≤ 2 → (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have pos₃ : ¬i = j →
  ¬n ≤ 2 →
    ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) → (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → n ≤ 2 → LE.le (α := ℤ) 0 0
pos₂ : ¬i = j → ¬n ≤ 2 → (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
pos₃ :
  ¬i = j →
    ¬n ≤ 2 →
      ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) → (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have pos₄ : ¬i = j →
  ¬n ≤ 2 →
    ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) →
      ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n) →
        (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → n ≤ 2 → LE.le (α := ℤ) 0 0
pos₂ : ¬i = j → ¬n ≤ 2 → (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
pos₃ :
  ¬i = j →
    ¬n ≤ 2 →
      ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) → (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
pos₄ :
  ¬i = j →
    ¬n ≤ 2 →
      ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) →
        ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n) →
          (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have pos₅ : ¬i = j →
  ¬n ≤ 2 →
    ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) →
      ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n) →
        ¬((↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n)) →
          (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → n ≤ 2 → LE.le (α := ℤ) 0 0
pos₂ : ¬i = j → ¬n ≤ 2 → (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
pos₃ :
  ¬i = j →
    ¬n ≤ 2 →
      ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) → (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n → LE.le (α := ℤ) (-1) 0
pos₄ :
  ¬i = j →
    ¬n ≤ 2 →
      ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) →
        ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n) →
          (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) → LE.le (α := ℤ) (-1) 0
pos₅ :
  ¬i = j →
    ¬n ≤ 2 →
      ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) →
        ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n) →
          ¬((↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n)) →
            (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ)
    (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
          else
            if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
            else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
    0
have neg : ¬i = j →
  ¬n ≤ 2 →
    ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n) →
      ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n) →
        ¬((↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n)) →
          ¬((↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n)) → LE.le (α := ℤ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
⊢ (A n)ᵀ = A n
have a : ∀ (i j : Fin n), (A n)ᵀ i j = A n i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
⊢ (A n)ᵀ i j = A n i j
have a : Eq (α := ℤ) (if j = i then 2 else if (↑j : ℕ) + 1 = (↑i : ℕ) ∨ (↑i : ℕ) + 1 = (↑j : ℕ) then -1 else 0)
  (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0)
Tactic: simp only [A, transpose_apply, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
⊢ (B n)ᵀ = C n
have a : ∀ (i j : Fin n), (B n)ᵀ i j = C n i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
⊢ (B n)ᵀ i j = C n i j
have a : Eq (α := ℤ)
  (if j = i then 2
  else
    if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else if (↑i : ℕ) + 1 = (↑j : ℕ) then -1 else 0)
  (if i = j then 2
  else
    if (↑i : ℕ) + 1 = (↑j : ℕ) then -1 else if (↑j : ℕ) + 1 = (↑i : ℕ) then if (↑i : ℕ) = n - 1 then -2 else -1 else 0)
Tactic: simp only [B, C, transpose_apply, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
⊢ (C n)ᵀ = B n
have rw : (C n)ᵀ = (B n)ᵀᵀ
Tactic: rw [← (B n).transpose_transpose, B_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
rw : (C n)ᵀ = (B n)ᵀᵀ
⊢ (C n)ᵀ = B n
have rw₁ : (C n)ᵀ = (C n)ᵀ
Tactic: rw [← (B n).transpose_transpose, B_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
⊢ (D n)ᵀ = D n
have a : ∀ (i j : Fin n), (D n)ᵀ i j = D n i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
⊢ (D n)ᵀ i j = D n i j
have a : Eq (α := ℤ)
  (if j = i then 2
  else
    if n ≤ 2 then 0
    else
      if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
      else
        if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
        else
          if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1
          else if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1 else 0)
  (if i = j then 2
  else
    if n ≤ 2 then 0
    else
      if (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n then -1
      else
        if (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n then -1
        else
          if (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n) then -1
          else if (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n) then -1 else 0)
Tactic: simp only [D, transpose_apply, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 6
⊢ E₆ i i = 2
have 0 : E₆ ((fun (i : Fin 6) ↦ i) (⟨0, sorry⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, sorry⟩ : Fin 6)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 6
0 : E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) = 2
⊢ E₆ i i = 2
have 1 : E₆ ((fun (i : Fin 6) ↦ i) (⟨1, sorry⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, sorry⟩ : Fin 6)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 6
0 : E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) = 2
1 : E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) = 2
⊢ E₆ i i = 2
have 2 : E₆ ((fun (i : Fin 6) ↦ i) (⟨2, sorry⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, sorry⟩ : Fin 6)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 6
0 : E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) = 2
1 : E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) = 2
2 : E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) = 2
⊢ E₆ i i = 2
have 3 : E₆ ((fun (i : Fin 6) ↦ i) (⟨3, sorry⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, sorry⟩ : Fin 6)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 6
0 : E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) = 2
1 : E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) = 2
2 : E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) = 2
3 : E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) = 2
⊢ E₆ i i = 2
have 4 : E₆ ((fun (i : Fin 6) ↦ i) (⟨4, sorry⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, sorry⟩ : Fin 6)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 6
0 : E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) = 2
1 : E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) = 2
2 : E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) = 2
3 : E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) = 2
4 : E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) = 2
⊢ E₆ i i = 2
have 5 : E₆ ((fun (i : Fin 6) ↦ i) (⟨5, sorry⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, sorry⟩ : Fin 6)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
⊢ E₇ i i = 2
have 0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2
have 1 : E₇ ((fun (i : Fin 7) ↦ i) (⟨1, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2
1 : E₇ ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2
have 2 : E₇ ((fun (i : Fin 7) ↦ i) (⟨2, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨2, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2
1 : E₇ ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) = 2
2 : E₇ ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2
have 3 : E₇ ((fun (i : Fin 7) ↦ i) (⟨3, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨3, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2
1 : E₇ ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) = 2
2 : E₇ ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) = 2
3 : E₇ ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2
have 4 : E₇ ((fun (i : Fin 7) ↦ i) (⟨4, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨4, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2
1 : E₇ ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) = 2
2 : E₇ ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) = 2
3 : E₇ ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) = 2
4 : E₇ ((fun (i : Fin 7) ↦ i) (⟨4, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨4, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2
have 5 : E₇ ((fun (i : Fin 7) ↦ i) (⟨5, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨5, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 7
0 : E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2
1 : E₇ ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) = 2
2 : E₇ ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) = 2
3 : E₇ ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) = 2
4 : E₇ ((fun (i : Fin 7) ↦ i) (⟨4, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨4, ⋯⟩ : Fin 7)) = 2
5 : E₇ ((fun (i : Fin 7) ↦ i) (⟨5, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨5, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2
have 6 : E₇ ((fun (i : Fin 7) ↦ i) (⟨6, sorry⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨6, sorry⟩ : Fin 7)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 8
⊢ E₈ i i = 2
have 0 : E₈ ((fun (i : Fin 8) ↦ i) (⟨0, sorry⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, sorry⟩ : Fin 8)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 8
0 : E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) = 2
⊢ E₈ i i = 2
have 1 : E₈ ((fun (i : Fin 8) ↦ i) (⟨1, sorry⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, sorry⟩ : Fin 8)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 8
0 : E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) = 2
1 : E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) = 2
⊢ E₈ i i = 2
have 2 : E₈ ((fun (i : Fin 8) ↦ i) (⟨2, sorry⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, sorry⟩ : Fin 8)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 8
0 : E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) = 2
1 : E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) = 2
2 : E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) = 2
⊢ E₈ i i = 2
have 3 : E₈ ((fun (i : Fin 8) ↦ i) (⟨3, sorry⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, sorry⟩ : Fin 8)) = 2
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
i : Fin 8
0 : E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) = 2
1 : E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) = 2
2 : E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) = 2
3 : E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) = 2
⊢ E₈ i i = 2
have 4 : E₈ ((fun (i : Fin 8) ↦ i) (⟨4, sorry⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, sorry⟩ : Fin 8)) = 2
Tactic: fin_cases i
Cleared hypotheses: i