awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_2
inst : Group G
inst_1 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_2)
inst_2 : Fintype G
inst_3 : Fintype ↥(Subgroup.center G)
inst_4 : Fintype (↑(noncenter G) : Type u_2)
h : Fintype.card.{u_2} ↥(Subgroup.center G) = Nat.card.{u_2} ↥(Subgroup.center G)
h₁ :
  Eq (α := ℕ) (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
    (∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
      Nat.card.{u_2} (↑x.carrier : Type u_2))
h₂ : Fintype.card G = Nat.card G
⊢ Fintype.card.{u_2} ↥(Subgroup.center G) + ∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card = Fintype.card G

Tactic:
convert! Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2

Premises used: Group.nat_card_center_add_sum_card_noncenter_eq_card
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_2
inst : Group G
inst_1 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_2)
inst_2 : Fintype G
inst_3 : Fintype ↥(Subgroup.center G)
inst_4 : Fintype (↑(noncenter G) : Type u_2)
⊢ Fintype.card.{u_2} ↥(Subgroup.center G) = Nat.card.{u_2} ↥(Subgroup.center G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_2
inst : Group G
inst_1 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_2)
inst_2 : Fintype G
inst_3 : Fintype ↥(Subgroup.center G)
inst_4 : Fintype (↑(noncenter G) : Type u_2)
h :
  Eq (α := ℕ) (∑ i : (↑(noncenter G) : Type u_2), (↑i : ConjClasses G).carrier.toFinset.card)
    (∑ i : (↑(noncenter G) : Type u_2), Nat.card.{u_2} (↑(↑i : ConjClasses G).carrier : Type u_2))
⊢ Eq (α := ℕ) (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
    (∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
      Nat.card.{u_2} (↑x.carrier : Type u_2))

Tactic:
rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype,
      ← Finset.sum_set_coe]

Premises used: finsum_set_coe_eq_finsum_mem, finsum_eq_sum_of_fintype, Finset.sum_set_coe, ConjClasses.noncenter
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_2
inst : Group G
inst_1 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_2)
inst_2 : Fintype G
inst_3 : Fintype ↥(Subgroup.center G)
inst_4 : Fintype (↑(noncenter G) : Type u_2)
⊢ Eq (α := ℕ) (∑ i : (↑(noncenter G) : Type u_2), (↑i : ConjClasses G).carrier.toFinset.card)
    (∑ i : (↑(noncenter G) : Type u_2), Nat.card.{u_2} (↑(↑i : ConjClasses G).carrier : Type u_2))

Tactic:
simp
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_2
inst : Group G
inst_1 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_2)
inst_2 : Fintype G
inst_3 : Fintype ↥(Subgroup.center G)
inst_4 : Fintype (↑(noncenter G) : Type u_2)
⊢ Fintype.card G = Nat.card G

Tactic:
simp
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
rw : (↑(a⁻¹ * b) : G) ∈ H ↔ g • (↑(a⁻¹ * b) : G) ∈ g • H
⊢ (QuotientGroup.leftRel (H.subgroupOf K) : ↥K → ↥K → Prop) a b ↔
    (QuotientGroup.leftRel ((g • H).subgroupOf (g • K)) : ↥(g • K) → ↥(g • K) → Prop)
      ((equivSMul g K : (a : ↥K) → ↥(g • K)) a : ↥(g • K)) ((equivSMul g K : (a : ↥K) → ↥(g • K)) b : ↥(g • K))

Tactic:
rw [← Quotient.eq'', ← Quotient.eq'', QuotientGroup.eq, QuotientGroup.eq,
      mem_subgroupOf, mem_subgroupOf, ← map_inv, ← map_mul, equivSMul_apply_coe]

Premises used: Subgroup.equivSMul_apply_coe, map_inv, Quotient.eq'', QuotientGroup.eq, map_mul, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ (↑(a⁻¹ * b) : G) ∈ H ↔ g • (↑(a⁻¹ * b) : G) ∈ g • H

Tactic:
smul_mem_pointwise_smul_iff.symm

Premises used: Set.Mem, Iff.symm, Subgroup.smul_mem_pointwise_smul_iff
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ (↑(a⁻¹ * b) : G) ∈ H ↔ g • (↑(a⁻¹ * b) : G) ∈ g • H

Tactic:
exact smul_mem_pointwise_smul_iff.symm

Premises used: Iff.symm, Subgroup.smul_mem_pointwise_smul_iff
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Commensurable H

Tactic:
simp [Commensurable]

Premises used: Subgroup.Commensurable
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.Commensurable K ↔ K.Commensurable H

Tactic:
and_comm

Premises used: and_comm, Subgroup.Commensurable
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.Commensurable K → K.Commensurable H

Tactic:
And.symm

Premises used: Subgroup.Commensurable, And.symm
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hhk : H.Commensurable K
hkl : K.Commensurable L
⊢ H.Commensurable L

Tactic:
⟨Subgroup.relIndex_ne_zero_trans hhk.1 hkl.1, Subgroup.relIndex_ne_zero_trans hkl.2 hhk.2⟩

Premises used: And.right, And.left, And.intro, Subgroup.Commensurable, Subgroup.relIndex_ne_zero_trans
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
⊢ Equivalence.{u_1 + 1} (α := Subgroup G) Commensurable

Tactic:
⟨Commensurable.refl, fun h => Commensurable.symm h, fun h₁ h₂ => Commensurable.trans h₁ h₂⟩

Premises used: Subgroup.Commensurable.trans, Subgroup.Commensurable.symm, Subgroup.Commensurable.refl, Equivalence.mk
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : ConjAct G
⊢ H.Commensurable K ↔ (g • H).Commensurable (g • K)

Tactic:
and_congr (not_iff_not.mpr (Eq.congr_left (Nat.card_congr (quotConjEquiv H K g))))
    (not_iff_not.mpr (Eq.congr_left (Nat.card_congr (quotConjEquiv K H g))))

Premises used: not_iff_not, Iff.mpr, Subgroup.quotConjEquiv, Eq.congr_left, Nat.card_congr, Subgroup.Commensurable, and_congr
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.Commensurable K
g : ConjAct G
⊢ (g • H).Commensurable (g • K)

Tactic:
(commensurable_conj g).mp h

Premises used: Subgroup.Commensurable.commensurable_conj, Iff.mp
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : ConjAct G
rw : (g⁻¹ • g • H).Commensurable (g⁻¹ • H) ↔ H.Commensurable (g⁻¹ • H)
rw₁ : ConjAct G
rw₂ rw₃ : H.Commensurable (g⁻¹ • H) ↔ H.Commensurable (g⁻¹ • H)
⊢ (g • H).Commensurable H ↔ H.Commensurable (g⁻¹ • H)

Tactic:
rw [commensurable_conj, inv_smul_smul]

Premises used: Subgroup.Commensurable.commensurable_conj, inv_smul_smul
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : ConjAct G
ha : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} a
hb : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} b
rw : (a • b • H).Commensurable H
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} (a * b)

Tactic:
rw [Set.mem_setOf_eq, mul_smul]

Premises used: Set.mem_setOf_eq, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : ConjAct G
ha : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} a
hb : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} b
⊢ (a • b • H).Commensurable H

Tactic:
trans ((commensurable_conj _).mp hb) ha

Premises used: Subgroup.Commensurable.commensurable_conj, Subgroup.Commensurable.trans, Iff.mp
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : ConjAct G
ha : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} a
hb : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} b
⊢ (a • b • H).Commensurable H

Tactic:
exact trans ((commensurable_conj _).mp hb) ha

Premises used: Subgroup.Commensurable.commensurable_conj, Subgroup.Commensurable.trans, Iff.mp
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (HSMul.hSMul (α := ConjAct G) 1 H).Commensurable H
rw₁ rw₂ : H.Commensurable H
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} 1

Tactic:
rw [Set.mem_setOf_eq, one_smul]

Premises used: Set.mem_setOf_eq, one_smul
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : ConjAct G
h : Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} x
rwa : (x⁻¹ • H).Commensurable H
rwa₁ : H.Commensurable (x⁻¹ • H)
rwa₂ rwa₃ rwa₄ rwa₅ : (x • H).Commensurable H
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} x⁻¹

Tactic:
rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]

Premises used: Subgroup.Commensurable.comm, Set.mem_setOf_eq, Subgroup.Commensurable.commensurable_inv
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : ConjAct G
⊢ g ∈ commensurator' H ↔ (g • H).Commensurable H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Subgroup.Commensurable
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ g ∈ commensurator H ↔
    (HSMul.hSMul (α := ConjAct G) ((ConjAct.toConjAct : (a : G) → ConjAct G) g : ConjAct G) H).Commensurable H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Subgroup.Commensurable
-- Module: Mathlib.GroupTheory.Commensurable
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hk : H.Commensurable K
⊢ commensurator H = commensurator K

Tactic:
Subgroup.ext fun x =>
    let hx := (commensurable_conj x).1 hk
    ⟨fun h => hx.symm.trans (h.trans hk), fun h => hx.trans (h.trans hk.symm)⟩

Premises used: Subgroup.Commensurable.commensurable_conj, Subgroup.Commensurable.trans, Iff.intro, Iff.mp, Subgroup.Commensurable.symm, Subgroup.ext
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
rw : g₁ * g₂ * g₁⁻¹ * g₂⁻¹ = 1 ↔ g₁ * g₂ = g₂ * g₁
rw₁ : g₁ * g₂ * g₁⁻¹ = g₂ ↔ g₁ * g₂ = g₂ * g₁
rw₂ rw₃ : g₁ * g₂ = g₂ * g₁ ↔ g₁ * g₂ = g₂ * g₁
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

Tactic:
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]

Premises used: commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂

Tactic:
commutatorElement_eq_one_iff_mul_comm

Premises used: SemiconjBy, Commute, commutatorElement_eq_one_iff_mul_comm
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
h : Commute g₁ g₂
⊢ ⁅g₁, g₂⁆ = 1

Tactic:
commutatorElement_eq_one_iff_commute.mpr h

Premises used: Iff.mpr, commutatorElement_eq_one_iff_commute
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Eq (α := G) ⁅g, 1⁆ 1

Tactic:
(Commute.one_right g).commutator_eq

Premises used: Commute.one_right, Commute.commutator_eq
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Bracket.bracket (L := G) 1 g = 1

Tactic:
(Commute.one_left g).commutator_eq

Premises used: Commute.commutator_eq, Commute.one_left
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ ⁅g, g⁆ = 1

Tactic:
(Commute.refl g).commutator_eq

Premises used: Commute.refl, Commute.commutator_eq
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
simp_rw : (g₁ * g₂ * g₁⁻¹ * g₂⁻¹)⁻¹ = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
simp_rw₁ : g₂⁻¹⁻¹ * (g₁⁻¹⁻¹ * (g₂⁻¹ * g₁⁻¹)) = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
simp_rw₂ : g₂ * (g₁ * (g₂⁻¹ * g₁⁻¹)) = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]

Premises used: commutatorElement_def, mul_assoc, inv_inv, mul_inv_rev
-- 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
simp_rw :
  (f : (a : G) → G') (g₁ * g₂ * g₁⁻¹ * g₂⁻¹) =
    HMul.hMul (β := G')
      (HMul.hMul (β := G') (HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂ : G'))
        (((f : (a : G) → G') g₁)⁻¹ : G'))
      (((f : (a : G) → G') g₂)⁻¹ : G')
simp_rw₁ :
  HMul.hMul (β := G')
      (HMul.hMul (β := G') (HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂ : G'))
        ((f : (a : G) → G') g₁⁻¹ : G'))
      ((f : (a : G) → G') g₂⁻¹ : G') =
    HMul.hMul (β := G')
      (HMul.hMul (β := G') (HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂ : G'))
        (((f : (a : G) → G') g₁)⁻¹ : G'))
      (((f : (a : G) → G') g₂)⁻¹ : G')
⊢ Eq.{u_2 + 1} (α := G') ((f : (a : G) → G') ⁅g₁, g₂⁆ : G')
    (Bracket.bracket (L := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂) : G')

Tactic:
simp_rw [commutatorElement_def, map_mul f, map_inv f]

Premises used: commutatorElement_def, map_inv, map_mul
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
g₁ g₂ g₃ : G
⊢ g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆

Tactic:
simp [mul_assoc, commutatorElement_def]

Premises used: commutatorElement_def, mul_assoc
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
a b c : G
⊢ ⁅a * b, c⁆ = a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆

Tactic:
simp [mul_assoc, commutatorElement_def]

Premises used: commutatorElement_def, mul_assoc
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
a b c : G
⊢ ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹

Tactic:
simp [mul_assoc, commutatorElement_def]

Premises used: commutatorElement_def, mul_assoc
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = closure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}

Tactic:
rfl

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

Tactic:
subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩

Premises used: Set.Mem, Subgroup.subset_closure, And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
⊢ ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃

Tactic:
H₃.closure_le.trans
    ⟨fun h a b c d => h ⟨a, b, c, d, rfl⟩, fun h _g ⟨a, b, c, d, h_eq⟩ => h_eq ▸ h a b c d⟩

Premises used: Set.Mem, Subgroup.closure_le, Membership.mem, Eq.rec, _private.0.Subgroup.commutator_le.match_1, SetLike.coe, And.intro, Iff.intro, Exists.intro, Iff.trans, rfl
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ K₁ K₂ : Subgroup G
h₁ : H₁ ≤ K₁
h₂ : H₂ ≤ K₂
⊢ ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆

Tactic:
commutator_le.mpr fun _g₁ hg₁ _g₂ hg₂ => commutator_mem_commutator (h₁ hg₁) (h₂ hg₂)

Premises used: Iff.mpr, Subgroup.commutator_le, Subgroup.commutator_mem_commutator
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
rw : (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆) ↔ H₁ ≤ centralizer (↑H₂ : Set G)
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer (↑H₂ : Set G)

Tactic:
rw [eq_bot_iff, commutator_le]

Premises used: Subgroup.commutator_le, eq_bot_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆) ↔ H₁ ≤ centralizer (↑H₂ : Set G)

Tactic:
forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
refine : ∀ (p : G) (_hp : p ∈ H₁) (q : G) (hq : q ∈ H₂), Membership.mem (γ := Subgroup G) ⊥ ⁅p, q⁆ ↔ q * p = p * q
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆) ↔ H₁ ≤ centralizer (↑H₂ : Set G)

Tactic:
refine forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
rw : ⁅p, q⁆ = 1 ↔ q * p = p * q
rw₁ : p * q = q * p ↔ q * p = p * q
rw₂ rw₃ : q * p = p * q ↔ q * p = p * q
⊢ Membership.mem (γ := Subgroup G) ⊥ ⁅p, q⁆ ↔ q * p = p * q

Tactic:
rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]

Premises used: eq_comm, commutatorElement_eq_one_iff_mul_comm, Subgroup.mem_bot
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
simp_rw :
  ∀ (h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ (↑H₁ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1)
    (h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ (↑H₂ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1),
    ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ∀ h ∈ (↑H₃ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

Tactic:
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
    mem_centralizer_iff_commutator_eq_one] at h1 h2 ⊢

Premises used: Subgroup.mem_centralizer_iff_commutator_eq_one, Subgroup.commutator_le, Subgroup.commutator_eq_bot_iff_le_centralizer
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ (↑H₁ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ (↑H₂ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ (↑H₃ : Set G)
trans : ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
trans₁ : x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
⊢ ⁅z, ⁅x, y⁆⁆ = 1

Tactic:
trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ (↑H₁ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ (↑H₂ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ (↑H₃ : Set G)
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹

Tactic:
simp [commutatorElement_def, mul_assoc]

Premises used: commutatorElement_def, mul_assoc
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ (↑H₁ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ (↑H₂ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ (↑H₃ : Set G)
rw : x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]

Premises used: Subgroup.inv_mem
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ (↑H₁ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ (↑H₂ : Set G), ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ (↑H₃ : Set G)
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆

Tactic:
commutator_le.mpr fun g₁ h₁ g₂ h₂ =>
    commutatorElement_inv g₂ g₁ ▸ ⁅H₂, H₁⁆.inv_mem_iff.mpr (commutator_mem_commutator h₂ h₁)

Premises used: Iff.mpr, Bracket.bracket, Subgroup.commutator_le, Eq.rec, commutatorElement_inv, Subgroup.commutator_mem_commutator, Subgroup.inv_mem_iff
-- Module: Mathlib.GroupTheory.Commutator.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆

Tactic:
le_antisymm (commutator_comm_le H₁ H₂) (commutator_comm_le H₂ H₁)

Premises used: le_antisymm, Subgroup.commutator_comm_le
-- 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}
change : Normal (closure base)
⊢ ⁅H₁, H₂⁆.Normal

Tactic:
change (closure base).Normal

Premises used: Subgroup.closure, Subgroup.Normal
-- 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}
h_base : base = Group.conjugatesOfSet base
rw : Normal (closure (Group.conjugatesOfSet base))
⊢ Normal (closure base)

Tactic:
rw [h_base]
-- 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}
h_base : base = Group.conjugatesOfSet base
⊢ Normal (closure (Group.conjugatesOfSet base))

Tactic:
Subgroup.normalClosure_normal

Premises used: Subgroup.normalClosure, Subgroup.normalClosure_normal
-- 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}
h_base : base = Group.conjugatesOfSet base
⊢ Normal (closure (Group.conjugatesOfSet base))

Tactic:
exact Subgroup.normalClosure_normal

Premises used: Subgroup.normalClosure_normal
-- 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}
suffices : base = Group.conjugatesOfSet base
⊢ Normal (closure base)

Tactic:
suffices h_base : base = Group.conjugatesOfSet base by
    rw [h_base]
    exact Subgroup.normalClosure_normal
-- 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}
⊢ base = Group.conjugatesOfSet base

Tactic:
Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_

Premises used: Set.Subset.antisymm, Group.subset_conjugatesOfSet
-- 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}
refine : ∀ (a : G) (h : a ∈ Group.conjugatesOfSet base), a ∈ base
⊢ base = Group.conjugatesOfSet base

Tactic:
refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_

Premises used: Set.Subset.antisymm, Group.subset_conjugatesOfSet
-- 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 ∈ Group.conjugatesOfSet base
⊢ ∃ a_1 ∈ base, ∃ (c : G), c * a_1 * c⁻¹ = a

Tactic:
simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h

Premises used: isConj_iff, Group.mem_conjugatesOfSet_iff