awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = ⁅H, H⁆
rw₁ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = ⁅H, H⁆
rw₂ : ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆
rw₃ rw₄ : ⁅H, H⁆ = ⁅H, H⁆
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆

Tactic:
rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]

Premises used: MonoidHom.range_eq_map, Subgroup.range_subtype, commutator_def, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ⁅H, H⁆ ≤ H

Tactic:
H.map_subtype_commutator.symm.trans_le (map_subtype_le _)

Premises used: Eq.trans_le, Subgroup.map_subtype_le, Eq.symm, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : _root_.commutator G ≤ H
⊢ H.Normal

Tactic:
commutator_top_left_le_iff.mp <| commutator_mono le_top le_top |>.trans h

Premises used: Subgroup.commutator_mono, Subgroup.commutator_top_left_le_iff, le_top, Iff.mp, LE.le.trans
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (commutator G) ⊥ ↔ Eq (α := Subgroup G) (center G) ⊤

Tactic:
simp [commutator, Subgroup.commutator_eq_bot_iff_le_centralizer]

Premises used: Subgroup.commutator_eq_bot_iff_le_centralizer, commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
rw : Eq (α := Subgroup G) (center G) ⊤ ↔ IsMulCommutative G
rw₁ rw₂ : IsMulCommutative G ↔ IsMulCommutative G
⊢ Eq (α := Subgroup G) (commutator G) ⊥ ↔ IsMulCommutative G

Tactic:
rw [commutator_eq_bot_iff_center_eq_top, center_eq_top_iff]

Premises used: Subgroup.center_eq_top_iff, commutator_eq_bot_iff_center_eq_top
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
hG : IsMulCommutative G
⊢ Eq (α := Subgroup G) (commutator G) ⊥

Tactic:
(commutator_eq_bot_iff G).mpr hG

Premises used: Iff.mpr, commutator_eq_bot_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
rw :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G))
        (centralizer (↑(commutator G) : Set G)))
      ⊤)
    ⊥
⊢ LE.le (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G)) (centralizer (↑(commutator G) : Set G)))
    (center G)

Tactic:
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
    Subgroup.commutator_eq_bot_iff_le_centralizer]

Premises used: Subgroup.centralizer_univ, Subgroup.coe_top, Subgroup.commutator_eq_bot_iff_le_centralizer
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
this :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G))
        (centralizer (↑(commutator G) : Set G)))
      ⊤)
    ⊥

Tactic:
Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this

Premises used: Subgroup.commutator_commutator_eq_bot_of_rotate
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
this :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥
refine :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G)) ⊤)
      (centralizer (↑(commutator G) : Set G)))
    ⊥
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G))
        (centralizer (↑(commutator G) : Set G)))
      ⊤)
    ⊥

Tactic:
refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this

Premises used: Subgroup.commutator_commutator_eq_bot_of_rotate
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
this rwa rwa₁ rwa₂ rwa₃ :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G)) ⊤)
      (centralizer (↑(commutator G) : Set G)))
    ⊥

Tactic:
rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]

Premises used: Subgroup.centralizer, Subgroup.commutator_comm, commutator, SetLike.coe
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
suffices :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G))
        (centralizer (↑(commutator G) : Set G)))
      ⊤)
    ⊥

Tactic:
suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
    refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
rw :
  LE.le (α := Subgroup G) (centralizer (↑(commutator G) : Set G))
    (centralizer (↑(Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G))) : Set G))
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥

Tactic:
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]

Premises used: Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ LE.le (α := Subgroup G) (centralizer (↑(commutator G) : Set G))
    (centralizer (↑(Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G))) : Set G))

Tactic:
Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)

Premises used: Subgroup.commutator_mono, Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset, le_top
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ LE.le (α := Subgroup G) (centralizer (↑(commutator G) : Set G))
    (centralizer (↑(Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G))) : Set G))

Tactic:
exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)

Premises used: Subgroup.commutator_mono, Set.centralizer_subset, le_top
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
hg : IsConj g (HPow.hPow (β := ℕ) g 2)
obtain : ∀ (h : Gˣ) (hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)), g ∈ commutatorSet G
⊢ g ∈ commutatorSet G

Tactic:
obtain ⟨h, hg⟩ := hg
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)
h₁ : ⁅(↑h : G), g⁆ = g
⊢ g ∈ commutatorSet G

Tactic:
use h, g
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)
h₁ : HPow.hPow (β := ℕ) g 2 * (↑h : G) * (↑h : G)⁻¹ * g⁻¹ = g
⊢ ⁅(↑h : G), g⁆ = g

Tactic:
rw [commutatorElement_def, hg]

Premises used: commutatorElement_def
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)
⊢ HPow.hPow (β := ℕ) g 2 * (↑h : G) * (↑h : G)⁻¹ * g⁻¹ = g

Tactic:
simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]

Premises used: pow_two, IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
rw : ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆
⊢ map f (commutator G) = ⁅f.range, f.range⁆

Tactic:
rw [_root_.commutator_def, Subgroup.map_commutator]

Premises used: commutator_def, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hx hy : map f ⊤ = f.range
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆

Tactic:
apply congr_arg₂

Premises used: congr_arg₂
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hx : Codisjoint ⊤ f.ker
⊢ map f ⊤ = f.range

Tactic:
rw [Subgroup.map_eq_range_iff]

Premises used: Subgroup.map_eq_range_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hx : ⊤ ⊔ f.ker = ⊤
hx₁ hx₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
⊢ Codisjoint ⊤ f.ker

Tactic:
rw [codisjoint_iff, top_sup_eq]

Premises used: codisjoint_iff, top_sup_eq
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hy : Codisjoint ⊤ f.ker
⊢ map f ⊤ = f.range

Tactic:
rw [Subgroup.map_eq_range_iff]

Premises used: Subgroup.map_eq_range_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hy : ⊤ ⊔ f.ker = ⊤
hy₁ hy₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
⊢ Codisjoint ⊤ f.ker

Tactic:
rw [codisjoint_iff, top_sup_eq]

Premises used: codisjoint_iff, top_sup_eq
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
h₁ :
  Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G)) ⊆
    commutatorSet G
h₂ :
  commutatorSet G ⊆
    Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G))
⊢ Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G)) =
    commutatorSet G

Tactic:
apply Set.Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : ↥(closureCommutatorRepresentatives G)
⊢ Membership.mem (α := G) (commutatorSet G)
    ((Subgroup.subtype (closureCommutatorRepresentatives G) : (a : ↥(closureCommutatorRepresentatives G)) → G)
        ⁅g₁, g₂⁆ :
      G)

Tactic:
⟨g₁, g₂, rfl⟩

Premises used: commutatorSet, Set.Mem, setOf, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : ↥(closureCommutatorRepresentatives G)
⊢ Membership.mem (α := G) (commutatorSet G)
    ((Subgroup.subtype (closureCommutatorRepresentatives G) : (a : ↥(closureCommutatorRepresentatives G)) → G)
        ⁅g₁, g₂⁆ :
      G)

Tactic:
exact ⟨g₁, g₂, rfl⟩
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ commutatorSet G ⊆
    Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G))

Tactic:
fun g hg ↦
      ⟨_, ⟨⟨_, subset_closure <| .inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩,
          ⟨_, subset_closure <| .inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩, rfl⟩,
        hg.choose_spec.choose_spec⟩

Premises used: Exists.choose_spec, Set.Mem, Bracket.bracket, setOf, Prod.mk, Set.Subset, Prod.fst, Subtype.mk, Subgroup.subset_closure, commutatorRepresentatives._proof_2, commutatorRepresentatives._proof_1, And.intro, Exists.intro, Set.image, Exists.choose, Or.inl, Prod.snd, Or.inr, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ commutatorSet G ⊆
    Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G))

Tactic:
exact fun g hg ↦
      ⟨_, ⟨⟨_, subset_closure <| .inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩,
          ⟨_, subset_closure <| .inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩, rfl⟩,
        hg.choose_spec.choose_spec⟩
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
⊢ IsMulCommutative.{u_1} (G ⧸ N) ↔ _root_.commutator G ≤ N

Tactic:
⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩

Premises used: Iff.intro, IsMulCommutative.mk, Std.Commutative.mk
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
refine_1 : ∀ (hcomm : IsMulCommutative.{u_1} (G ⧸ N)), _root_.commutator G ≤ N
refine_2 : ∀ (hGN : _root_.commutator G ≤ N) (x' y' : G ⧸ N), x' * y' = y' * x'
⊢ IsMulCommutative.{u_1} (G ⧸ N) ↔ _root_.commutator G ≤ N

Tactic:
refine ⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
refine_1 : commutatorSet G ⊆ (↑N : Set G)
⊢ _root_.commutator G ≤ N

Tactic:
rw [commutator_eq_normalClosure, ← Subgroup.normalClosure_subset_iff]

Premises used: commutator_eq_normalClosure, Subgroup.normalClosure_subset_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
refine_1 : Eq (α := G ⧸ N) (↑(p * q * p⁻¹ * q⁻¹) : G ⧸ N) 1
⊢ ⁅p, q⁆ ∈ (↑N : Set G)

Tactic:
rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]

Premises used: commutatorElement_def, SetLike.mem_coe, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
refine_1 : HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) * (↑p : G ⧸ N)⁻¹ * (↑q : G ⧸ N)⁻¹ = 1
⊢ Eq (α := G ⧸ N) (↑(p * q * p⁻¹ * q⁻¹) : G ⧸ N) 1

Tactic:
simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]

Premises used: QuotientGroup.mk_inv, QuotientGroup.mk_mul
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
refine_1 : Eq (α := G ⧸ N) (Bracket.bracket (L := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N)) 1
refine_1₁ : HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) = HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N)
refine_1₂ refine_1₃ :
  HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N) = HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N)
⊢ HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) * (↑p : G ⧸ N)⁻¹ * (↑q : G ⧸ N)⁻¹ = 1

Tactic:
rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']

Premises used: commutatorElement_def, mul_comm', commutatorElement_eq_one_iff_mul_comm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
refine_2 :
  ∀ (x : G),
    HMul.hMul (α := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N) y' =
      HMul.hMul (β := G ⧸ N) y' ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
⊢ x' * y' = y' * x'

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'

Premises used: QuotientGroup.mk'_surjective, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
y' : G ⧸ N
x : G
refine_2 :
  ∀ (y : G),
    HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
        ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N) =
      HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N)
        ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
⊢ HMul.hMul (α := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N) y' =
    HMul.hMul (β := G ⧸ N) y' ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)

Tactic:
obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'

Premises used: QuotientGroup.mk'_surjective, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
refine_2 : ⁅x, y⁆ ∈ N
⊢ HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
      ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N) =
    HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N)
      ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)

Tactic:
rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
      QuotientGroup.eq_one_iff]

Premises used: QuotientGroup.mk'_apply, commutatorElement_eq_one_iff_mul_comm, QuotientGroup.eq_one_iff, map_commutatorElement
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
refine_2 : Membership.mem (γ := Subgroup G) (_root_.commutator G) ⁅x, y⁆
⊢ ⁅x, y⁆ ∈ N

Tactic:
apply hGN
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
refine_2 : Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) ⁅x, y⁆
⊢ Membership.mem (γ := Subgroup G) (_root_.commutator G) ⁅x, y⁆

Tactic:
rw [commutator_eq_closure]

Premises used: commutator_eq_closure
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) ⁅x, y⁆

Tactic:
Subgroup.subset_closure (commutator_mem_commutatorSet x y)

Premises used: commutator_mem_commutatorSet, Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) ⁅x, y⁆

Tactic:
exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

Premises used: commutator_mem_commutatorSet, Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
apply : IsMulCommutative.{u_1} (G ⧸ N)
⊢ _root_.commutator G ≤ N

Tactic:
apply quotient_commutative_iff_commutator_le.mp

Premises used: Subgroup.Normal.quotient_commutative_iff_commutator_le, Iff.mp
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
apply : Function.Surjective (α := ↥H) (β := G ⧸ N) (⇑φ : (a : ↥H) → G ⧸ N)
⊢ IsMulCommutative.{u_1} (G ⧸ N)

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

Premises used: Function.Surjective.mul_comm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
rw : Function.Surjective (α := G) (β := G ⧸ N) (⇑(QuotientGroup.mk' N) : (a : G) → G ⧸ N)
⊢ Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤

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

Premises used: MonoidHom.range_eq_map, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
⊢ Function.Surjective (α := G) (β := G ⧸ N) (⇑(QuotientGroup.mk' N) : (a : G) → G ⧸ N)

Tactic:
QuotientGroup.mk'_surjective N

Premises used: QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
⊢ Function.Surjective (α := G) (β := G ⧸ N) (⇑(QuotientGroup.mk' N) : (a : G) → G ⧸ N)

Tactic:
exact QuotientGroup.mk'_surjective N

Premises used: QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
⊢ Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤

Tactic:
have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ := by
    rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
    exact QuotientGroup.mk'_surjective N
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
this : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤
rw : N ⊔ H.subtype.range = N ⊔ H ⊔ N
⊢ Function.Surjective (α := ↥H) (β := G ⧸ N) (⇑φ : (a : ↥H) → G ⧸ N)

Tactic:
rw [MulHom.coe_coe, ← MonoidHom.range_eq_top, MonoidHom.range_eq_map, ← Subgroup.map_map, ← this,
    Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN, ← MonoidHom.range_eq_map]

Premises used: Subgroup.map_eq_map_iff, MonoidHom.range_eq_map, MulHom.coe_coe, MonoidHom.range_eq_top, sup_comm, QuotientGroup.ker_mk', Subgroup.map_map
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
this : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤
⊢ N ⊔ H.subtype.range = N ⊔ H ⊔ N

Tactic:
simp
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
apply : (pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆) ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆

Tactic:
apply le_antisymm (commutator_pi_pi_le H K)

Premises used: Subgroup.commutator_pi_pi_le, le_antisymm
-- Module: Mathlib.GroupTheory.Commutator.Finite
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
rw : ∀ (i : η), map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
⊢ (pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆) ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆

Tactic:
rw [pi_le_iff]

Premises used: Subgroup.pi_le_iff