awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Cartan
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
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
⊢ 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:
split_ifs
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : n ≤ 2
⊢ LE.le (α := ℤ) 0 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬n ≤ 2
h_3 : (↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬n ≤ 2
h_3 : ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n)
h_4 : (↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬n ≤ 2
h_3 : ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n)
h_4 : ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n)
h_5 : (↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n)
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬n ≤ 2
h_3 : ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n)
h_4 : ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n)
h_5 : ¬((↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n))
h_6 : (↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n)
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
h_1 : ¬i = j
h_2 : ¬n ≤ 2
h_3 : ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∧ (↑j : ℕ) + 2 < n)
h_4 : ¬((↑j : ℕ) + 1 = (↑i : ℕ) ∧ (↑i : ℕ) + 2 < n)
h_5 : ¬((↑i : ℕ) + 3 = n ∧ ((↑j : ℕ) + 2 = n ∨ (↑j : ℕ) + 1 = n))
h_6 : ¬((↑j : ℕ) + 3 = n ∧ ((↑i : ℕ) + 2 = n ∨ (↑i : ℕ) + 1 = n))
⊢ LE.le (α := ℤ) 0 0

Tactic:
omega
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
a : ∀ (i j : Fin n), (A n)ᵀ i j = A n i j
⊢ (A n)ᵀ = A n

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
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)
⊢ (A n)ᵀ i j = A n i j

Tactic:
simp only [A, transpose_apply, of_apply]

Premises used: CartanMatrix.A, Matrix.of_apply, Matrix.transpose_apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
⊢ 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:
grind
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
⊢ (A n).IsSymm

Tactic:
A_transpose n

Premises used: Matrix.IsSymm, CartanMatrix.A_transpose
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
a : ∀ (i j : Fin n), (B n)ᵀ i j = C n i j
⊢ (B n)ᵀ = C n

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
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)
⊢ (B n)ᵀ i j = C n i j

Tactic:
simp only [B, C, transpose_apply, of_apply]

Premises used: CartanMatrix.C, Matrix.of_apply, CartanMatrix.B, Matrix.transpose_apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
⊢ 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:
grind
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
rw : (C n)ᵀ = (B n)ᵀᵀ
rw₁ rw₂ : (C n)ᵀ = (C n)ᵀ
⊢ (C n)ᵀ = B n

Tactic:
rw [← (B n).transpose_transpose, B_transpose]

Premises used: Matrix.transpose_transpose, CartanMatrix.B_transpose, CartanMatrix.B
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
a : ∀ (i j : Fin n), (D n)ᵀ i j = D n i j
⊢ (D n)ᵀ = D n

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
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)
⊢ (D n)ᵀ i j = D n i j

Tactic:
simp only [D, transpose_apply, of_apply]

Premises used: Matrix.of_apply, CartanMatrix.D, Matrix.transpose_apply
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
i j : Fin n
⊢ 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:
grind
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
n : ℕ
⊢ (D n).IsSymm

Tactic:
D_transpose n

Premises used: CartanMatrix.D_transpose, Matrix.IsSymm
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 1) (Fin 1) ℤ) (A 1) !![2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (A 2) !![2, -1; -1, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 3) (Fin 3) ℤ) (A 3) !![2, -1, 0; -1, 2, -1; 0, -1, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 1) (Fin 1) ℤ) (B 1) (A 1)

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 1) (Fin 1) ℤ) (C 1) (A 1)

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 1) (Fin 1) ℤ) (D 1) (A 1)

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (D 2) !![2, 0; 0, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (B 2) !![2, -2; -1, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (C 2) !![2, -1; -2, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 3) (Fin 3) ℤ) (D 3) !![2, -1, -1; -1, 2, 0; -1, 0, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 3) (Fin 3) ℤ)
    ((reindex (Cycle.formPerm (↑[0, 1] : Cycle (Fin 3)) ⋯) (Cycle.formPerm (↑[0, 1] : Cycle (Fin 3)) ⋯) :
          (a : Matrix (Fin 3) (Fin 3) ℤ) → Matrix (Fin 3) (Fin 3) ℤ)
        (D 3) :
      Matrix (Fin 3) (Fin 3) ℤ)
    (A 3 : Matrix (Fin 3) (Fin 3) ℤ)

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ Eq (α := Matrix (Fin 4) (Fin 4) ℤ) (D 4) !![2, -1, 0, 0; -1, 2, -1, -1; 0, -1, 2, 0; 0, -1, 0, 2]

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
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
5 : E₆ ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) = 2
⊢ E₆ i i = 2

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
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
6 : E₇ ((fun (i : Fin 7) ↦ i) (⟨6, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨6, ⋯⟩ : Fin 7)) = 2
⊢ E₇ i i = 2

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨0, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨1, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨2, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨3, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨4, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨4, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨5, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨5, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₇ ((fun (i : Fin 7) ↦ i) (⟨6, ⋯⟩ : Fin 7)) ((fun (i : Fin 7) ↦ i) (⟨6, ⋯⟩ : Fin 7)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
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
4 : E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) = 2
5 : E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) = 2
6 : E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) = 2
7 : E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) = 2
⊢ E₈ i i = 2

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
i : Fin 4
0 : F₄ ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) = 2
1 : F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) = 2
2 : F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) = 2
3 : F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) = 2
⊢ F₄ i i = 2

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
i : Fin 2
0 : G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = 2
1 : G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = 2
⊢ G₂ i i = 2

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
⊢ G₂ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = 2

Tactic:
decide
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
i j : Fin 6
h : i ≠ j
0 : ∀ (h : (fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩ ≠ j), E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) j ≤ 0
1 : ∀ (h : (fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩ ≠ j), E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) j ≤ 0
2 : ∀ (h : (fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩ ≠ j), E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) j ≤ 0
3 : ∀ (h : (fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩ ≠ j), E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) j ≤ 0
4 : ∀ (h : (fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩ ≠ j), E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) j ≤ 0
5 : ∀ (h : (fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩ ≠ j), E₆ ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) j ≤ 0
⊢ E₆ i j ≤ 0

Tactic:
fin_cases i
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 6
h : (fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ≤ 0
h_2 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ≤ 0
h_3 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ≤ 0
h_4 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ≤ 0
h_5 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ≤ 0
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) j ≤ 0

Tactic:
fin_cases j
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 6
h : (fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ≤ 0
h_2 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ≤ 0
h_3 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ≤ 0
h_4 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ≤ 0
h_5 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ≤ 0
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) j ≤ 0

Tactic:
fin_cases j
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 6
h : (fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩ ≠ j
2 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ≤ 0
h_2 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ≤ 0
h_3 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ≤ 0
h_4 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ≤ 0
h_5 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ≤ 0
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) j ≤ 0

Tactic:
fin_cases j
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 6
h : (fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩ ≠ j
3 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ≤ 0
h_2 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ≤ 0
h_3 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ≤ 0
h_4 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ≤ 0
h_5 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ≤ 0
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) j ≤ 0

Tactic:
fin_cases j
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 6
h : (fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩ ≠ j
4 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨0, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨0, ⋯⟩ : Fin 6)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨1, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨1, ⋯⟩ : Fin 6)) ≤ 0
h_2 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨2, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨2, ⋯⟩ : Fin 6)) ≤ 0
h_3 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨3, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨3, ⋯⟩ : Fin 6)) ≤ 0
h_4 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ≤ 0
h_5 :
  ∀ (h : Ne (α := Fin 6) ((fun (i : Fin 6) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 6) ↦ i) ⟨5, ⋯⟩)),
    E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) ((fun (i : Fin 6) ↦ i) (⟨5, ⋯⟩ : Fin 6)) ≤ 0
⊢ E₆ ((fun (i : Fin 6) ↦ i) (⟨4, ⋯⟩ : Fin 6)) j ≤ 0

Tactic:
fin_cases j