Theorem: quotient_comm_contains_commutators_iff (Jordan/Mathlib/Commutators.lean)

State before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ _root_.commutator G ≤ N
Tactic:
constructor
State after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
⊢ (Std.Commutative fun x x_1 => x * x_1) → _root_.commutator G ≤ N

case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
⊢ _root_.commutator G ≤ N → Std.Commutative fun x x_1 => x * x_1

State before:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
⊢ (Std.Commutative fun x x_1 => x * x_1) → _root_.commutator G ≤ N
Tactic:
intro hcomm
State after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
⊢ _root_.commutator G ≤ N

State before:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
⊢ _root_.commutator G ≤ N
Tactic:
rw [commutator_eq_normalClosure]
State after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
⊢ normalClosure (commutatorSet G) ≤ N

State before:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
⊢ normalClosure (commutatorSet G) ≤ N
Tactic:
rw [← Subgroup.normalClosure_subset_iff]
State after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
⊢ commutatorSet G ⊆ ↑N

State before:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
⊢ commutatorSet G ⊆ ↑N
Tactic:
intro x hx
State after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
x : G
hx : x ∈ commutatorSet G
⊢ x ∈ ↑N

State before:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
x : G
hx : x ∈ commutatorSet G
⊢ x ∈ ↑N
Tactic:
obtain ⟨p, q, rfl⟩ := hx
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ⁅p, q⁆ ∈ ↑N

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ⁅p, q⁆ ∈ ↑N
Tactic:
simp only [SetLike.mem_coe]
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ⁅p, q⁆ ∈ N

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ⁅p, q⁆ ∈ N
Tactic:
rw [← QuotientGroup.eq_one_iff]
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑⁅p, q⁆ = 1

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑⁅p, q⁆ = 1
Tactic:
rw [commutatorElement_def]
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑(p * q * p⁻¹ * q⁻¹) = 1

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑(p * q * p⁻¹ * q⁻¹) = 1
Tactic:
simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑p * ↑q * (↑p)⁻¹ * (↑q)⁻¹ = 1

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑p * ↑q * (↑p)⁻¹ * (↑q)⁻¹ = 1
Tactic:
rw [← commutatorElement_def]
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ⁅↑p, ↑q⁆ = 1

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ⁅↑p, ↑q⁆ = 1
Tactic:
rw [commutatorElement_eq_one_iff_mul_comm]
State after:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑p * ↑q = ↑q * ↑p

State before:
case mp.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hcomm : Std.Commutative fun x x_1 => x * x_1
p q : G
⊢ ↑p * ↑q = ↑q * ↑p
Tactic:
apply hcomm.comm
State after:
no goals

State before:
case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
⊢ _root_.commutator G ≤ N → Std.Commutative fun x x_1 => x * x_1
Tactic:
intro hGN
State after:
case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
⊢ Std.Commutative fun x x_1 => x * x_1

State before:
case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
apply Std.Commutative.mk
State after:
case mpr.comm
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
⊢ ∀ (a b : G ⧸ N), a * b = b * a

State before:
case mpr.comm
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
⊢ ∀ (a b : G ⧸ N), a * b = b * a
Tactic:
rintro x'
State after:
case mpr.comm
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x' : G ⧸ N
⊢ ∀ (b : G ⧸ N), x' * b = b * x'

State before:
case mpr.comm
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x' : G ⧸ N
⊢ ∀ (b : G ⧸ N), x' * b = b * x'
Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
State after:
case mpr.comm.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x : G
⊢ ∀ (b : G ⧸ N), (QuotientGroup.mk' N) x * b = b * (QuotientGroup.mk' N) x

State before:
case mpr.comm.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x : G
⊢ ∀ (b : G ⧸ N), (QuotientGroup.mk' N) x * b = b * (QuotientGroup.mk' N) x
Tactic:
intro y'
State after:
case mpr.comm.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x : G
y' : G ⧸ N
⊢ (QuotientGroup.mk' N) x * y' = y' * (QuotientGroup.mk' N) x

State before:
case mpr.comm.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
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'
State after:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) x * (QuotientGroup.mk' N) y = (QuotientGroup.mk' N) y * (QuotientGroup.mk' N) x

State before:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
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]
State after:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) ⁅x, y⁆ = 1

State before:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) ⁅x, y⁆ = 1
Tactic:
simp only [QuotientGroup.mk'_apply]
State after:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ↑⁅x, y⁆ = 1

State before:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ↑⁅x, y⁆ = 1
Tactic:
rw [QuotientGroup.eq_one_iff]
State after:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N

State before:
case mpr.comm.intro.intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N
Tactic:
apply hGN
State after:
case mpr.comm.intro.intro.a
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ _root_.commutator G

State before:
case mpr.comm.intro.intro.a
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ _root_.commutator G
Tactic:
rw [commutator_eq_closure]
State after:
case mpr.comm.intro.intro.a
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ closure (commutatorSet G)

State before:
case mpr.comm.intro.intro.a
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ closure (commutatorSet G)
Tactic:
apply Subgroup.subset_closure
State after:
case mpr.comm.intro.intro.a.a
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ commutatorSet G

State before:
case mpr.comm.intro.intro.a.a
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ commutatorSet G
Tactic:
exact commutator_mem_commutatorSet x y
State after:
no goals