Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i j : Fin 8
h : i ≠ j
⊢ E₈ i j ≤ 0

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «0».«2»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «0».«3»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «0».«4»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «0».«5»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «0».«6»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «0».«7»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «1».«2»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «1».«3»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «1».«4»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «1».«5»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «1».«6»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «1».«7»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «2».«0»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «2».«1»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «2».«2»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «2».«3»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «2».«4»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «2».«5»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «2».«6»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «2».«7»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «3».«0»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «3».«1»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «3».«2»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «3».«3»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «3».«4»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «3».«5»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «3».«6»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «3».«7»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «4».«0»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «4».«1»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «4».«2»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «4».«3»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «4».«4»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «4».«5»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «4».«6»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «4».«7»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «5».«0»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «5».«1»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «5».«2»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «5».«3»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «5».«4»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «5».«5»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «5».«6»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «5».«7»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «6».«0»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «6».«1»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «6».«2»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «6».«3»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «6».«4»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «6».«5»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «6».«6»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «6».«7»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0

case «7».«0»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «7».«1»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «7».«2»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

case «7».«3»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

case «7».«4»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

case «7».«5»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

case «7».«6»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

case «7».«7»
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ (fun i ↦ i) ⟨7, ⋯⟩
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) ≤ 0