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

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]
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

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)
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

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
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 ⇑↑φ

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]
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 ⇑φ

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]
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 φ = ⊤

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
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 φ) = ⊤

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]
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 φ)

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
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 φ)

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]
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 φ

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 _
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 φ

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
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 φ

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 ∈ ⊤
y : G := Quotient.out' x
⊢ x ∈ MonoidHom.range φ
Tactic:
have hy : y ∈ φ.range.comap (QuotientGroup.mk' N) := by rw [S_top]; exact Subgroup.mem_top y
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
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ x ∈ MonoidHom.range φ

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 ∈ ⊤
y : G := Quotient.out' x
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ x ∈ MonoidHom.range φ
Tactic:
rw [← QuotientGroup.out_eq' x]
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
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ ↑(Quotient.out' x) ∈ MonoidHom.range φ

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 ∈ ⊤
y : G := Quotient.out' x
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ ↑(Quotient.out' x) ∈ MonoidHom.range φ
Tactic:
exact Subgroup.mem_comap.mp hy
State after:
no goals

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 ∈ ⊤
y : G := Quotient.out' x
⊢ y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
rw [S_top]
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
⊢ y ∈ ⊤

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 ∈ ⊤
y : G := Quotient.out' x
⊢ y ∈ ⊤
Tactic:
exact Subgroup.mem_top y
State after:
no goals

State before:
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 φ)
Tactic:
intro g hg
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)
g : G
hg : g ∈ N
⊢ g ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)

State before:
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)
g : G
hg : g ∈ N
⊢ g ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
rw [Subgroup.mem_comap]
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)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g ∈ MonoidHom.range φ

State before:
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)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g ∈ MonoidHom.range φ
Tactic:
convert (MonoidHom.range φ).one_mem
State after:
case h.e'_4
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)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g = 1

State before:
case h.e'_4
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)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g = 1
Tactic:
simp only [hg, QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff]
State after:
no goals

State before:
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 φ)
Tactic:
intro h hh
State after:
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 : G
hh : h ∈ H
⊢ h ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)

State before:
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 : G
hh : h ∈ H
⊢ h ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
simp only [mem_comap, QuotientGroup.mk'_apply, MonoidHom.mem_range, MonoidHom.coe_comp,
  QuotientGroup.coe_mk', coeSubtype, Function.comp_apply, Subtype.exists, exists_prop, φ]
State after:
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 : G
hh : h ∈ H
⊢ ∃ a ∈ H, ↑a = ↑h

State before:
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 : G
hh : h ∈ H
⊢ ∃ a ∈ H, ↑a = ↑h
Tactic:
use h
State after:
no goals