-- Mathlib/GroupTheory/Abelianization.lean
theorem Subgroup.Normal.quotient_commutative_iff_commutator_le {N : Subgroup G} [N.Normal] :
    Std.Commutative (· * · : G ⧸ N → _ → _) ↔ _root_.commutator G ≤ N

Proof state:
case mpr.comm.intro.intro.a
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ closure (commutatorSet G)

Tactic:
exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

Result:
no goals

Proof state:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ↑p * ↑q = ↑q * ↑p

Tactic:
apply hcomm.comm

Result:
no goals

Proof state:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ↑(p * q * p⁻¹ * q⁻¹) = 1

Tactic:
simp only [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def,
  QuotientGroup.mk_mul, QuotientGroup.mk_inv]

Result:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ↑p * ↑q * (↑p)⁻¹ * (↑q)⁻¹ = 1

Proof state:
case mpr
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
⊢ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
apply Std.Commutative.mk

Result:
case mpr.comm
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
⊢ ∀ (a b : G ⧸ N), a * b = b * a

Proof state:
case mpr.comm.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N

Tactic:
apply hGN

Result:
case mpr.comm.intro.intro.a
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ _root_.commutator G

Proof state:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
⊢ _root_.commutator G ≤ N

Tactic:
rw [commutator_eq_normalClosure]

Result:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
⊢ normalClosure (commutatorSet G) ≤ N

Proof state:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ (Std.Commutative fun x1 x2 => x1 * x2) → _root_.commutator G ≤ N

Tactic:
intro hcomm

Result:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
⊢ _root_.commutator G ≤ N

Proof state:
case mpr.comm
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' : G ⧸ N
⊢ ∀ (b : G ⧸ N), x' * b = b * x'

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'

Result:
case mpr.comm.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x : G
⊢ ∀ (b : G ⧸ N), (QuotientGroup.mk' N) x * b = b * (QuotientGroup.mk' N) x

Proof state:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ⁅p, q⁆ ∈ ↑N

Tactic:
rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]

Result:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ↑(p * q * p⁻¹ * q⁻¹) = 1

Proof state:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
⊢ normalClosure (commutatorSet G) ≤ N

Tactic:
rw [← Subgroup.normalClosure_subset_iff]

Result:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
⊢ commutatorSet G ⊆ ↑N

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ (Std.Commutative fun x1 x2 => x1 * x2) ↔ _root_.commutator G ≤ N

Tactic:
constructor

Result:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ (Std.Commutative fun x1 x2 => x1 * x2) → _root_.commutator G ≤ N

case mpr
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ _root_.commutator G ≤ N → Std.Commutative fun x1 x2 => x1 * x2

Proof state:
case mpr.comm.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x : G
⊢ ∀ (b : G ⧸ N), (QuotientGroup.mk' N) x * b = b * (QuotientGroup.mk' N) x

Tactic:
intro y'

Result:
case mpr.comm.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x : G
y' : G ⧸ N
⊢ (QuotientGroup.mk' N) x * y' = y' * (QuotientGroup.mk' N) x

Proof state:
case mpr.comm.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x : G
y' : G ⧸ N
⊢ (QuotientGroup.mk' N) x * y' = y' * (QuotientGroup.mk' N) x

Tactic:
obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'

Result:
case mpr.comm.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) x * (QuotientGroup.mk' N) y = (QuotientGroup.mk' N) y * (QuotientGroup.mk' N) x

Proof state:
case mpr.comm.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) x * (QuotientGroup.mk' N) y = (QuotientGroup.mk' N) y * (QuotientGroup.mk' N) x

Tactic:
rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement,
  QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff]

Result:
case mpr.comm.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N

Proof state:
case mpr.comm
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
⊢ ∀ (a b : G ⧸ N), a * b = b * a

Tactic:
rintro x'

Result:
case mpr.comm
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' : G ⧸ N
⊢ ∀ (b : G ⧸ N), x' * b = b * x'

Proof state:
case mpr.comm.intro.intro.a
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ _root_.commutator G

Tactic:
rw [commutator_eq_closure]

Result:
case mpr.comm.intro.intro.a
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ closure (commutatorSet G)

Proof state:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ↑p * ↑q * (↑p)⁻¹ * (↑q)⁻¹ = 1

Tactic:
simp only [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm]

Result:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ↑p * ↑q = ↑q * ↑p

Proof state:
case mp
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
⊢ commutatorSet G ⊆ ↑N

Tactic:
rintro x ⟨p, q, rfl⟩

Result:
case mp.intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : Std.Commutative fun x1 x2 => x1 * x2
p q : G
⊢ ⁅p, q⁆ ∈ ↑N

Proof state:
case mpr
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ _root_.commutator G ≤ N → Std.Commutative fun x1 x2 => x1 * x2

Tactic:
intro hGN

Result:
case mpr
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
⊢ Std.Commutative fun x1 x2 => x1 * x2