internlm/Lean-Github huggingface dataset:
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = id a
Tactic:
simp only [id.def]
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = a
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = a
Tactic:
exact hk
Proof state after:
no goals
Theorem: mem_commutatorSet_of_isConj_sq
Proof state before:
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
hg : IsConj g (g ^ 2)
⊢ g ∈ commutatorSet G
Tactic:
obtain ⟨h, hg⟩ := hg
Proof state after:
case intro
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G
Theorem: mem_commutatorSet_of_isConj_sq
Proof state before:
case intro
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G
Tactic:
use ↑h
Proof state after:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ∃ g₂, ⁅↑h, g₂⁆ = g
Theorem: mem_commutatorSet_of_isConj_sq
Proof state before:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ∃ g₂, ⁅↑h, g₂⁆ = g
Tactic:
use g
Proof state after:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g
Theorem: mem_commutatorSet_of_isConj_sq
Proof state before:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g
Tactic:
rw [commutatorElement_def, hg]
Proof state after:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g
Theorem: mem_commutatorSet_of_isConj_sq
Proof state before:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g
Tactic:
simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]
Proof state after:
no goals
Theorem: Subgroup.map_top_eq_range
Proof state before:
G✝ : Type ?u.1324
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
⊢ map f ⊤ = MonoidHom.range f
Tactic:
simp only [map_eq_range_iff, codisjoint_top_left]
Proof state after:
no goals
Theorem: Subgroup.map_commutator_eq
Proof state before:
G✝ : Type ?u.2272
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
⊢ map f (_root_.commutator H) = ⁅MonoidHom.range f, MonoidHom.range f⁆
Tactic:
rw [_root_.commutator_def, Subgroup.map_commutator, Subgroup.map_top_eq_range]
Proof state after:
no goals
Theorem: Subgroup.commutator_eq'
Proof state before:
G✝ : Type ?u.3265
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map (Subgroup.subtype H) (_root_.commutator ↥H) = ⁅H, H⁆
Tactic:
simp only [map_commutator_eq, subtype_range]
Proof state after:
no goals
Theorem: surj_to_comm
Proof state before:
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
⊢ a * b = b * a
Tactic:
obtain ⟨a', ha'⟩ := is_surj a
Proof state after:
case intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
⊢ a * b = b * a
Theorem: surj_to_comm
Proof state before:
case intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
⊢ a * b = b * a
Tactic:
obtain ⟨b', hb'⟩ := is_surj b
Proof state after:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ a * b = b * a
Theorem: surj_to_comm
Proof state before:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ a * b = b * a
Tactic:
simp only [← ha', ← hb', ← map_mul]
Proof state after:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ φ (a' * b') = φ (b' * a')
Theorem: surj_to_comm
Proof state before:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ φ (a' * b') = φ (b' * a')
Tactic:
rw [is_comm.comm]
Proof state after:
no goals
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof state after:
no goals
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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'
Proof 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'
Theorem: quotient_comm_contains_commutators_iff
Proof 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'
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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'
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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'
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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]
Proof 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)
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof 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
Theorem: quotient_comm_contains_commutators_iff
Proof 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
Proof state after:
no goals
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
⊢ _root_.commutator G ≤ N
Tactic:
rw [← quotient_comm_contains_commutators_iff nN]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
let φ : H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
refine' surj_to_comm φ.toMulHom _ hH.is_comm
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ Function.Surjective ⇑↑φ
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ Function.Surjective ⇑↑φ
Tactic:
simp only [MulHom.coe_mk, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ Function.Surjective ⇑φ
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ Function.Surjective ⇑φ
Tactic:
rw [← MonoidHom.range_top_iff_surjective]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ MonoidHom.range φ = ⊤
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ MonoidHom.range φ = ⊤
Tactic:
suffices S_top : φ.range.comap (QuotientGroup.mk' N) = ⊤ by
  rw [eq_top_iff]
  intro x _
  let y := Quotient.out' x
  have hy : y ∈ φ.range.comap (QuotientGroup.mk' N) := by rw [S_top]; exact Subgroup.mem_top y
  rw [← QuotientGroup.out_eq' x]
  exact Subgroup.mem_comap.mp hy
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
Tactic:
rw [eq_top_iff, ← hHN, sup_le_iff]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ N ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ) ∧ H ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ N ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ) ∧ H ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
constructor
Proof state after:
case left
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ N ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ)

case right
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ H ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
⊢ MonoidHom.range φ = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
⊢ ⊤ ≤ MonoidHom.range φ
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
⊢ ⊤ ≤ MonoidHom.range φ
Tactic:
intro x _
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
⊢ x ∈ MonoidHom.range φ
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
⊢ x ∈ MonoidHom.range φ
Tactic:
let y := Quotient.out' x
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
⊢ x ∈ MonoidHom.range φ