awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
j : Fin 8
h : (fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩ ≠ j
7 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0
h_1 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0
h_2 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0
h_3 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0
h_4 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0
h_5 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0
h_6 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0
h_7 :
  ∀ (h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)),
    E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) j ≤ 0

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

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨0, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨0, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨1, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨1, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨2, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨2, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨3, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨3, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨4, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨4, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨5, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨5, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨6, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨6, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 8) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩) ((fun (i : Fin 8) ↦ i) ⟨7, ⋯⟩)
⊢ E₈ ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ((fun (i : Fin 8) ↦ i) (⟨7, ⋯⟩ : Fin 8)) ≤ 0

Tactic:
simp_all [E₈]

Premises used: CartanMatrix.E₈
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
i j : Fin 4
h : i ≠ j
0 : ∀ (h : (fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩ ≠ j), F₄ ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) j ≤ 0
1 : ∀ (h : (fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩ ≠ j), F₄ ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) j ≤ 0
2 : ∀ (h : (fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩ ≠ j), F₄ ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) j ≤ 0
3 : ∀ (h : (fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩ ≠ j), F₄ ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) j ≤ 0
⊢ F₄ i j ≤ 0

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

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

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

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

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

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨1, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄
-- Module: Mathlib.Data.Matrix.Cartan
Goal:
h : Ne (α := Fin 4) ((fun (i : Fin 4) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)
⊢ F₄ ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ≤ 0

Tactic:
simp_all [F₄]

Premises used: CartanMatrix.F₄