-- Mathlib/GroupTheory/Abelianization.lean
theorem Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top {N : Subgroup G} [N.Normal]
    {H : Subgroup G} (hHN : N ⊔ H = ⊤) (hH : Subgroup.IsCommutative H) :
    _root_.commutator G ≤ N

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤

Tactic:
rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Function.Surjective ⇑(QuotientGroup.mk' N)

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
⊢ _root_.commutator G ≤ N

Tactic:
rw [← quotient_commutative_iff_commutator_le]

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
⊢ Std.Commutative fun x1 x2 => x1 * x2

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Function.Surjective ⇑(QuotientGroup.mk' N)

Tactic:
exact QuotientGroup.mk'_surjective N

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ ((QuotientGroup.mk' N).comp H.subtype).range = ⊤

Tactic:
simp only [φ, MonoidHom.range_eq_map, ← Subgroup.map_map]

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Subgroup.map (QuotientGroup.mk' N) (Subgroup.map H.subtype ⊤) = ⊤

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Function.Surjective ⇑φ

Tactic:
rw [MulHom.coe_coe, ← MonoidHom.range_eq_top]

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ ((QuotientGroup.mk' N).comp H.subtype).range = ⊤

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
apply Function.Surjective.mul_comm (f := φ) _ hH.is_comm

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Function.Surjective ⇑φ

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ Subgroup.map H.subtype ⊤ = N ⊔ (N ⊔ H)

Tactic:
simp [← MonoidHom.range_eq_map]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
⊢ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
let φ : H →ₙ* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Std.Commutative fun x1 x2 => x1 * x2

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ Subgroup.map (QuotientGroup.mk' N) (Subgroup.map H.subtype ⊤) = ⊤

Tactic:
have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ := by
  rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
  exact QuotientGroup.mk'_surjective N

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ Subgroup.map (QuotientGroup.mk' N) (Subgroup.map H.subtype ⊤) = ⊤

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ Subgroup.map (QuotientGroup.mk' N) (Subgroup.map H.subtype ⊤) = ⊤

Tactic:
simp only [← this, Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN]

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : H.IsCommutative
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ Subgroup.map H.subtype ⊤ = N ⊔ (N ⊔ H)