awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
F : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : FunLike F G G'
inst_3 : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : ∃ a_1 ∈ base, ∃ (c : G), c * a_1 * c⁻¹ = a
rcases : ∀ (c : G) (hc : c ∈ H₁) (e : G) (he : e ∈ H₂) (d : G), d * ⁅c, e⁆ * d⁻¹ ∈ base
⊢ a ∈ base

Tactic:
rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
F : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : FunLike F G G'
inst_3 : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
c : G
hc : c ∈ H₁
e : G
he : e ∈ H₂
d : G
⊢ d * ⁅c, e⁆ * d⁻¹ ∈ base

Tactic:
⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Eq.symm, conjugate_commutatorElement, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
F : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : FunLike F G G'
inst_3 : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
c : G
hc : c ∈ H₁
e : G
he : e ∈ H₂
d : G
⊢ d * ⁅c, e⁆ * d⁻¹ ∈ base

Tactic:
exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
inst_1 : H₁.Normal
inst_2 : H₂.Normal
⊢ ⁅H₁, H₂⁆ = normalClosure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}

Tactic:
le_antisymm closure_le_normalClosure (normalClosure_le_normal subset_closure)

Premises used: Subgroup.subset_closure, le_antisymm, Subgroup.normalClosure_le_normal, Subgroup.closure_le_normalClosure
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : H₂.Normal
⊢ ⁅H₁, H₂⁆ ≤ H₂

Tactic:
commutator_le.mpr fun g₁ _h₁ g₂ h₂ => H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂)

Premises used: Iff.mpr, Subgroup.commutator_le, Subgroup.inv_mem, Subgroup.mul_mem, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
inst_1 : H₁.Normal
⊢ ⁅H₁, H₂⁆ ≤ H₁

Tactic:
commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁

Premises used: Subgroup.commutator_le_right, Eq.rec, Subgroup.commutator_comm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Bracket.bracket (L := Subgroup G) ⊤ H ≤ H ↔ H.Normal

Tactic:
⟨fun hle ↦ ⟨fun h hh g ↦ ?_⟩, fun h ↦ commutator_le_right ⊤ H⟩

Premises used: Subgroup.commutator_le_right, Subgroup.Normal.mk, Iff.intro, Top.top
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine : ∀ (hle : Bracket.bracket (L := Subgroup G) ⊤ H ≤ H) (h : G) (hh : h ∈ H) (g : G), g * h * g⁻¹ ∈ H
⊢ Bracket.bracket (L := Subgroup G) ⊤ H ≤ H ↔ H.Normal

Tactic:
refine ⟨fun hle ↦ ⟨fun h hh g ↦ ?_⟩, fun h ↦ commutator_le_right ⊤ H⟩
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hle : Bracket.bracket (L := Subgroup G) ⊤ H ≤ H
h : G
hh : h ∈ H
g : G
⊢ g * h * g⁻¹ ∈ H

Tactic:
(H.mul_mem_cancel_right <| H.inv_mem hh).mp <| commutator_le.mp hle g trivial h hh

Premises used: trivial, Subgroup.commutator_le, Subgroup.mul_mem_cancel_right, Subgroup.inv_mem, Iff.mp
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hle : Bracket.bracket (L := Subgroup G) ⊤ H ≤ H
h : G
hh : h ∈ H
g : G
⊢ g * h * g⁻¹ ∈ H

Tactic:
exact (H.mul_mem_cancel_right <| H.inv_mem hh).mp <| commutator_le.mp hle g trivial h hh

Premises used: trivial, Subgroup.commutator_le, Subgroup.mul_mem_cancel_right, Subgroup.inv_mem, Iff.mp
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ⁅H, ⊤⁆ ≤ H ↔ H.Normal

Tactic:
commutator_comm H ⊤ ▸ commutator_top_left_le_iff

Premises used: Eq.rec, Subgroup.commutator_comm, Subgroup.commutator_top_left_le_iff, Top.top, Eq.symm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ normalizer (↑K : Set G) ↔ ⁅H, K⁆ ≤ K

Tactic:
le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩

Premises used: Iff.intro, Iff.trans, Subgroup.le_normalizer_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
refine_1 : ∀ (hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K), ⁅H, K⁆ ≤ K
refine_2 : ∀ (hH : ⁅H, K⁆ ≤ K) (h : G) (hh : h ∈ H) (k : G) (hk : k ∈ K), h * k * h⁻¹ ∈ K
⊢ H ≤ normalizer (↑K : Set G) ↔ ⁅H, K⁆ ≤ K

Tactic:
refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩

Premises used: Iff.intro, Iff.trans, Subgroup.le_normalizer_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
⊢ ⁅H, K⁆ ≤ K

Tactic:
commutator_le.mpr fun h hh k hk ↦ mul_mem (hH h hh k hk) (inv_mem hk)

Premises used: Iff.mpr, Subgroup.commutator_le, InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
⊢ ⁅H, K⁆ ≤ K

Tactic:
exact commutator_le.mpr fun h hh k hk ↦ mul_mem (hH h hh k hk) (inv_mem hk)

Premises used: Iff.mpr, Subgroup.commutator_le, InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
(mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk

Premises used: Subgroup.commutator_mem_commutator, InvMemClass.inv_mem, Iff.mp, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
exact (mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk

Premises used: Subgroup.commutator_mem_commutator, InvMemClass.inv_mem, Iff.mp, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ normalizer (↑K : Set G) ↔ ⁅K, H⁆ ≤ K

Tactic:
commutator_comm H K ▸ le_normalizer_iff_commutator_le_right

Premises used: Eq.rec, Subgroup.commutator_comm, Subgroup.le_normalizer_iff_commutator_le_right
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ : Subgroup G
⊢ Bracket.bracket (L := Subgroup G) ⊥ H₁ = ⊥

Tactic:
le_bot_iff.mp (commutator_le_left ⊥ H₁)

Premises used: le_bot_iff, Bot.bot, Iff.mp, Subgroup.commutator_le_left
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ : Subgroup G
⊢ Eq (α := Subgroup G) ⁅H₁, ⊥⁆ ⊥

Tactic:
le_bot_iff.mp (commutator_le_right H₁ ⊥)

Premises used: le_bot_iff, Subgroup.commutator_le_right, Bot.bot, Iff.mp
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
inst_1 : H₁.Normal
inst_2 : H₂.Normal
⊢ ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂

Tactic:
le_inf (commutator_le_left H₁ H₂) (commutator_le_right H₁ H₂)

Premises used: Subgroup.commutator_le_right, Set.Mem, le_inf, Subgroup.commutator_le_left
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₁ ⊔ H₂

Tactic:
grind [mul_assoc, mul_mem, mul_mem_sup, inv_mem]

Premises used: mul_assoc, InvMemClass.inv_mem, Subgroup.mul_mem_sup, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
apply :
  ∀ h ∈ H₁,
    ∀ (g : G),
      Membership.mem (γ := Set G) {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g} g →
        Membership.mem (γ := Subgroup G) (closure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}) (h * g * h⁻¹)
⊢ H₁ ≤ normalizer (↑⁅H₁, H₂⁆ : Set G)

Tactic:
apply le_normalizer_closure_iff.mpr

Premises used: Iff.mpr, Subgroup.le_normalizer_closure_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
apply : g * ⁅g₁, g₂⁆ * g⁻¹ * ⁅g, g₂⁆ ∈ ⁅H₁, H₂⁆
⊢ Membership.mem (γ := Subgroup G) (closure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}) (g * ⁅g₁, g₂⁆ * g⁻¹)

Tactic:
apply (mul_mem_cancel_right <| commutator_mem_commutator hg hg₂).mp

Premises used: Subgroup.commutator_mem_commutator, Iff.mp, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
rw : ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
⊢ g * ⁅g₁, g₂⁆ * g⁻¹ * ⁅g, g₂⁆ ∈ ⁅H₁, H₂⁆

Tactic:
rw [← commutatorElement_mul_left_eq_conj_mul g g₁ g₂]

Premises used: commutatorElement_mul_left_eq_conj_mul
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆

Tactic:
commutator_mem_commutator (mul_mem hg hg₁) hg₂

Premises used: Subgroup.commutator_mem_commutator, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆

Tactic:
exact commutator_mem_commutator (mul_mem hg hg₁) hg₂

Premises used: Subgroup.commutator_mem_commutator, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
rw : H₂ ≤ normalizer (↑⁅H₂, H₁⁆ : Set G)
⊢ H₂ ≤ normalizer (↑⁅H₁, H₂⁆ : Set G)

Tactic:
rw [commutator_comm]

Premises used: Subgroup.commutator_comm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer (↑⁅H₂, H₁⁆ : Set G)

Tactic:
apply normalizer_commutator_ge_left

Premises used: Subgroup.normalizer_commutator_ge_left
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
F : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : FunLike F G G'
inst_3 : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
⊢ Normal (G := ↥(H₁ ⊔ H₂)) (⁅H₁, H₂⁆.subgroupOf (H₁ ⊔ H₂))

Tactic:
normal_subgroupOf_of_le_normalizer <| sup_le
    (normalizer_commutator_ge_left H₁ H₂) (normalizer_commutator_ge_right H₁ H₂)

Premises used: Subgroup.normalizer_commutator_ge_right, Subgroup.normalizer_commutator_ge_left, Subgroup.normal_subgroupOf_of_le_normalizer, sup_le
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
simp_rw :
  (∀ g₁ ∈ H₁,
      ∀ g₂ ∈ H₂,
        Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
          (Bracket.bracket (L := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂) : G')) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

Tactic:
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]

Premises used: Subgroup.commutator_le, Subgroup.mem_comap, le_antisymm_iff, Subgroup.map_le_iff_le_comap, map_commutatorElement
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
left :
  ∀ g₁ ∈ H₁,
    ∀ g₂ ∈ H₂,
      Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
        (Bracket.bracket (L := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂) : G')
right : ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
⊢ (∀ g₁ ∈ H₁,
      ∀ g₂ ∈ H₂,
        Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
          (Bracket.bracket (L := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂) : G')) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
    (Bracket.bracket (L := G') ((f : (a : G) → G') p : G') ((f : (a : G) → G') q) : G')

Tactic:
commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)

Premises used: Subgroup.mem_map_of_mem, Subgroup.commutator_mem_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
    (Bracket.bracket (L := G') ((f : (a : G) → G') p : G') ((f : (a : G) → G') q) : G')

Tactic:
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)

Premises used: Subgroup.mem_map_of_mem, Subgroup.commutator_mem_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ (↑H₁ : Set G)
q : G
hq : q ∈ (↑H₂ : Set G)
right : Membership.mem (α := G') (map f ⁅H₁, H₂⁆) ((f : (a : G) → G') ⁅p, q⁆ : G')
⊢ Membership.mem (α := G') (map f ⁅H₁, H₂⁆)
    (Bracket.bracket (L := G') ((f : (a : G) → G') p : G') ((f : (a : G) → G') q) : G')

Tactic:
rw [← map_commutatorElement]

Premises used: map_commutatorElement
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ (↑H₁ : Set G)
q : G
hq : q ∈ (↑H₂ : Set G)
⊢ Membership.mem (α := G') (map f ⁅H₁, H₂⁆) ((f : (a : G) → G') ⁅p, q⁆ : G')

Tactic:
mem_map_of_mem _ (commutator_mem_commutator hp hq)

Premises used: Set.Mem, Subgroup.mem_map_of_mem, Subgroup.commutator_mem_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ (↑H₁ : Set G)
q : G
hq : q ∈ (↑H₂ : Set G)
⊢ Membership.mem (α := G') (map f ⁅H₁, H₂⁆) ((f : (a : G) → G') ⁅p, q⁆ : G')

Tactic:
exact mem_map_of_mem _ (commutator_mem_commutator hp hq)

Premises used: Subgroup.mem_map_of_mem, Subgroup.commutator_mem_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
K₁ K₂ : Subgroup G'
h₁ : K₁ ≤ map f H₁
h₂ : K₂ ≤ map f H₂
⊢ ⁅K₁, K₂⁆ ≤ map f ⁅H₁, H₂⁆

Tactic:
(commutator_mono h₁ h₂).trans (ge_of_eq (map_commutator H₁ H₂ f))

Premises used: Subgroup.commutator_mono, ge_of_eq, LE.le.trans, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
F : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : FunLike F G G'
inst_3 : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Characteristic
h₂ : H₂.Characteristic
⊢ ⁅H₁, H₂⁆.Characteristic

Tactic:
characteristic_iff_le_map.mpr fun ϕ =>
    commutator_le_map_commutator (characteristic_iff_le_map.mp h₁ ϕ)
      (characteristic_iff_le_map.mp h₂ ϕ)

Premises used: Iff.mpr, Subgroup.commutator_le_map_commutator, Iff.mp, Subgroup.characteristic_iff_le_map
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
a₁ : ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : ∀ g₁ ∈ H₁.prod K₁, ∀ g₂ ∈ H₂.prod K₂, ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
rw [commutator_le]

Premises used: Subgroup.commutator_le
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).1 ∈ (↑H₁.toSubmonoid : Set G)
hp₂ : (p₁, p₂).2 ∈ (↑K₁.toSubmonoid : Set G')
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).1 ∈ (↑H₂.toSubmonoid : Set G)
hq₂ : (q₁, q₂).2 ∈ (↑K₂.toSubmonoid : Set G')
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩

Premises used: Set.Mem, setOf, Set.prod, Subgroup.commutator_mem_commutator, And.intro
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).1 ∈ (↑H₁.toSubmonoid : Set G)
hp₂ : (p₁, p₂).2 ∈ (↑K₁.toSubmonoid : Set G')
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).1 ∈ (↑H₂.toSubmonoid : Set G)
hq₂ : (q₁, q₂).2 ∈ (↑K₂.toSubmonoid : Set G')
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a :
  map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
rw [prod_le_iff]

Premises used: Subgroup.prod_le_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
a₁ : map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a :
  Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inl G G') H₁) (map (MonoidHom.inl G G') H₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
rw [map_commutator]

Premises used: Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁
a₁ : map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂
⊢ Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inl G G') H₁) (map (MonoidHom.inl G G') H₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
apply commutator_mono

Premises used: Subgroup.commutator_mono
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

Premises used: MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr, MonoidHom.fst_comp_inl, Subgroup.le_prod_iff, MonoidHom.snd_comp_inl, Subgroup.map_map
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

Premises used: MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr, MonoidHom.fst_comp_inl, Subgroup.le_prod_iff, MonoidHom.snd_comp_inl, Subgroup.map_map
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a :
  Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inr G G') K₁) (map (MonoidHom.inr G G') K₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
rw [map_commutator]

Premises used: Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁
a₁ : map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂
⊢ Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inr G G') K₁) (map (MonoidHom.inr G G') K₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
apply commutator_mono

Premises used: Subgroup.commutator_mono
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

Premises used: MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr, MonoidHom.fst_comp_inl, Subgroup.le_prod_iff, MonoidHom.snd_comp_inl, Subgroup.map_map
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

Premises used: MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr, MonoidHom.fst_comp_inl, Subgroup.le_prod_iff, MonoidHom.snd_comp_inl, Subgroup.map_map
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
η : Type u_4
Gs : η → Type u_5
inst : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ ≤ pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆

Tactic:
commutator_le.mpr fun _p hp _q hq i hi => commutator_mem_commutator (hp i hi) (hq i hi)

Premises used: Iff.mpr, Set.Mem, Subgroup.commutator_le, Subgroup.commutator_mem_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ commutatorSet G = {g : G | ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g}

Tactic:
rfl

Premises used: commutatorSet, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ 1 ∈ commutatorSet G

Tactic:
⟨1, 1, commutatorElement_self 1⟩

Premises used: commutatorSet, Set.Mem, setOf, commutatorElement_self, Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
G' : Type u_2
F : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : FunLike F G G'
inst_3 : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ Nonempty.{u_1 + 1} (↑(commutatorSet G) : Type u_1)

Tactic:
⟨⟨1, one_mem_commutatorSet G⟩⟩

Premises used: one_mem_commutatorSet, Nonempty.intro, Subtype.mk, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ g ∈ commutatorSet G ↔ ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g

Tactic:
Iff.rfl

Premises used: commutatorSet, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ ∈ commutatorSet G

Tactic:
⟨g₁, g₂, rfl⟩

Premises used: commutatorSet, Set.Mem, setOf, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (commutator G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤)

Tactic:
rfl

Premises used: commutator, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (commutator G) (closure (commutatorSet G))

Tactic:
simp [commutator, Subgroup.commutator_def, commutatorSet]

Premises used: commutatorSet, commutator, Subgroup.commutator_def
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (commutator G) (normalClosure (commutatorSet G))

Tactic:
simp [commutator, Subgroup.commutator_def', commutatorSet]

Premises used: commutatorSet, Subgroup.commutator_def', commutator