Module: Mathlib.LinearAlgebra.Matrix.Cartan

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
<;>

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 «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 «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 «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 «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 «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