-- Mathlib/Algebra/Lie/Classical.lean
theorem sl_non_abelian [Fintype n] [Nontrivial R] (h : 1 < Fintype.card n) :
    ¬IsLieAbelian (sl n R)

Proof state:
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
c : IsLieAbelian ↥(sl n R)
⊢ ↑A * ↑B = ↑B * ↑A

Tactic:
rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]

Result:
no goals

Proof state:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
c : IsLieAbelian ↥(sl n R)
c' : ↑A * ↑B = ↑B * ↑A
⊢ False

Tactic:
simpa [A, B, stdBasisMatrix, Matrix.mul_apply, hij] using congr_fun (congr_fun c' i) i

Result:
no goals

Proof state:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
⊢ ¬IsLieAbelian ↥(sl n R)

Tactic:
let A := Eb R i j hij

Result:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
⊢ ¬IsLieAbelian ↥(sl n R)

Proof state:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
c : IsLieAbelian ↥(sl n R)
⊢ False

Tactic:
have c' : A.val * B.val = B.val * A.val := by
  rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]

Result:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
c : IsLieAbelian ↥(sl n R)
c' : ↑A * ↑B = ↑B * ↑A
⊢ False

Proof state:
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
⊢ ¬IsLieAbelian ↥(sl n R)

Tactic:
rcases Fintype.exists_pair_of_one_lt_card h with ⟨j, i, hij⟩

Result:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
⊢ ¬IsLieAbelian ↥(sl n R)

Proof state:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
⊢ ¬IsLieAbelian ↥(sl n R)

Tactic:
intro c

Result:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
c : IsLieAbelian ↥(sl n R)
⊢ False

Proof state:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
⊢ ¬IsLieAbelian ↥(sl n R)

Tactic:
let B := Eb R j i hij.symm

Result:
case intro.intro
n : Type u_1
R : Type u₂
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : ↥(sl n R) := Eb R i j hij
B : ↥(sl n R) := Eb R j i ⋯
⊢ ¬IsLieAbelian ↥(sl n R)