Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le (Jordan/V4.lean)

State before:
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ commutator G ≤ H
Tactic:
constructor
State after:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ (Std.Commutative fun x x_1 => x * x_1) → commutator G ≤ H

case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ commutator G ≤ H → Std.Commutative fun x x_1 => x * x_1

State before:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ (Std.Commutative fun x x_1 => x * x_1) → commutator G ≤ H
Tactic:
intro h
State after:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutator G ≤ H

State before:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutator G ≤ H
Tactic:
simp only [commutator_eq_closure, Subgroup.closure_le]
State after:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutatorSet G ⊆ ↑H

State before:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutatorSet G ⊆ ↑H
Tactic:
rintro g ⟨g1, g2, rfl⟩
State after:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ ↑H

State before:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ ↑H
Tactic:
simp only [SetLike.mem_coe, ← QuotientGroup.eq_one_iff]
State after:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1

State before:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1
Tactic:
rw [← QuotientGroup.mk'_apply, map_commutatorElement (QuotientGroup.mk' H) g1 g2]
State after:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1

State before:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1
Tactic:
simp only [QuotientGroup.mk'_apply, commutatorElement_eq_one_iff_mul_comm, h.comm]
State after:
no goals

State before:
case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ commutator G ≤ H → Std.Commutative fun x x_1 => x * x_1
Tactic:
intro h
State after:
case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ Std.Commutative fun x x_1 => x * x_1

State before:
case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
State after:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ ∀ (a b : G ⧸ H), a * b = b * a

State before:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ ∀ (a b : G ⧸ H), a * b = b * a
Tactic:
intro a b
State after:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
a b : G ⧸ H
⊢ a * b = b * a

State before:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
a b : G ⧸ H
⊢ a * b = b * a
Tactic:
obtain ⟨g1, rfl⟩ := QuotientGroup.mk'_surjective H a
State after:
case mpr.comm.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
b : G ⧸ H
g1 : G
⊢ (QuotientGroup.mk' H) g1 * b = b * (QuotientGroup.mk' H) g1

State before:
case mpr.comm.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
b : G ⧸ H
g1 : G
⊢ (QuotientGroup.mk' H) g1 * b = b * (QuotientGroup.mk' H) g1
Tactic:
obtain ⟨g2, rfl⟩ := QuotientGroup.mk'_surjective H b
State after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) g1 * (QuotientGroup.mk' H) g2 = (QuotientGroup.mk' H) g2 * (QuotientGroup.mk' H) g1

State before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) g1 * (QuotientGroup.mk' H) g2 = (QuotientGroup.mk' H) g2 * (QuotientGroup.mk' H) g1
Tactic:
rw [← commutatorElement_eq_one_iff_mul_comm]
State after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1

State before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1
Tactic:
rw [← map_commutatorElement _ g1 g2]
State after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) ⁅g1, g2⁆ = 1

State before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) ⁅g1, g2⁆ = 1
Tactic:
rw [QuotientGroup.mk'_apply]
State after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1

State before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1
Tactic:
rw [QuotientGroup.eq_one_iff]
State after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ H

State before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ H
Tactic:
apply h
State after:
case mpr.comm.intro.intro.a
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ commutator G

State before:
case mpr.comm.intro.intro.a
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ commutator G
Tactic:
apply Subgroup.commutator_mem_commutator
State after:
case mpr.comm.intro.intro.a.h₁
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g1 ∈ ⊤

case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤

State before:
case mpr.comm.intro.intro.a.h₁
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g1 ∈ ⊤

case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤
Tactic:
refine' Subgroup.mem_top g1
State after:
case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤

State before:
case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤
Tactic:
refine' Subgroup.mem_top g2
State after:
no goals