-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem mem_center_iff {A : SpecialLinearGroup n R} :
    A ∈ center (SpecialLinearGroup n R) ↔ ∃ (r : R), r ^ (Fintype.card n) = 1 ∧ scalar n r = A

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
rcases isEmpty_or_nonempty n with hn | ⟨⟨i⟩⟩

Result:
case inl
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

case inr.intro
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) → ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
aesop

Result:
no goals

Proof state:
case inr.intro
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩

Result:
case inr.intro.refine_1
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ ↑A i i ^ Fintype.card n = 1

case inr.intro.refine_2
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ (scalar n) (↑A i i) = ↑A

case inr.intro.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B

Proof state:
case inr.intro.refine_1
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
this : ((scalar n) (↑A i i)).det = 1
⊢ ↑A i i ^ Fintype.card n = 1

Tactic:
simpa using this

Result:
no goals

Proof state:
case inr.intro.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ ↑(B * A) = ↑(A * B)

Tactic:
simpa only [coe_mul, ← hr] using (scalar_commute (n := n) r (Commute.all r) B).symm

Result:
no goals

Proof state:
case inr.intro.refine_2
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ (scalar n) (↑A i i) = ↑A

Tactic:
exact scalar_eq_self_of_mem_center h i

Result:
no goals

Proof state:
case inl
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
exact ⟨by aesop, by simp [Subsingleton.elim A 1]⟩

Result:
no goals

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ (∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A) → A ∈ center (SpecialLinearGroup n R)

Tactic:
simp [Subsingleton.elim A 1]

Result:
no goals

Proof state:
case inr.intro.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B

Tactic:
suffices ↑ₘ(B * A) = ↑ₘ(A * B) from Subtype.val_injective this

Result:
case inr.intro.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ ↑(B * A) = ↑(A * B)

Proof state:
case inr.intro.refine_1
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ ↑A i i ^ Fintype.card n = 1

Tactic:
have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property

Result:
case inr.intro.refine_1
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
this : ((scalar n) (↑A i i)).det = 1
⊢ ↑A i i ^ Fintype.card n = 1