awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      Nat.card G
intro₁ :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
        (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
intro₂ :
  ∀ (val : Fintype G),
    Fintype.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Fintype.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
        (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
intro₃ :
  ∀ (val : Fintype G),
    Fintype.card.{u_1} ↥(Subgroup.center G) =
      ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro₄ : ∀ (val : Fintype G),
  Eq (α := ℕ)
    (∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
      Fintype.card.{u_1} (↑x.carrier : Type u_1))
    (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
Tactic: classical
  cases nonempty_fintype G
  rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
  simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
  congr 1
  swap
  · convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]
  calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
  rw [Finset.card_eq_sum_ones]
  refine Finset.sum_congr rfl ?_
  rintro ⟨g⟩ hg
  simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
  rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
  exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
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) + ∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card = Fintype.card G
have h : Fintype.card.{u_2} ↥(Subgroup.center G) = Nat.card.{u_2} ↥(Subgroup.center G)
Tactic: convert! Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
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)
⊢ Fintype.card.{u_2} ↥(Subgroup.center G) + ∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card = Fintype.card G
have 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))
Tactic: convert! Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
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))
⊢ Fintype.card.{u_2} ↥(Subgroup.center G) + ∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card = Fintype.card G
have h₂ : Fintype.card G = Nat.card G
Tactic: convert! Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
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 (α := ℕ) (∑ 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))
have 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))
Tactic: rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype,
      ← Finset.sum_set_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ (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))
have rw : (↑(a⁻¹ * b) : G) ∈ H ↔ g • (↑(a⁻¹ * b) : G) ∈ g • H
Tactic: rw [← Quotient.eq'', ← Quotient.eq'', QuotientGroup.eq, QuotientGroup.eq,
      mem_subgroupOf, mem_subgroupOf, ← map_inv, ← map_mul, equivSMul_apply_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : ConjAct G
⊢ (g • H).Commensurable H ↔ H.Commensurable (g⁻¹ • H)
have rw : (g⁻¹ • g • H).Commensurable (g⁻¹ • H) ↔ H.Commensurable (g⁻¹ • H)
Tactic: rw [commensurable_conj, inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
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
⊢ (g • H).Commensurable H ↔ H.Commensurable (g⁻¹ • H)
have rw₂ : H.Commensurable (g⁻¹ • H) ↔ H.Commensurable (g⁻¹ • H)
Tactic: rw [commensurable_conj, inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
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
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} (a * b)
have rw : (a • b • H).Commensurable H
Tactic: rw [Set.mem_setOf_eq, mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} 1
have rw : (HSMul.hSMul (α := ConjAct G) 1 H).Commensurable H
Tactic: rw [Set.mem_setOf_eq, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (HSMul.hSMul (α := ConjAct G) 1 H).Commensurable H
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} 1
have rw₁ : H.Commensurable H
Tactic: rw [Set.mem_setOf_eq, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
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
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} x⁻¹
have rwa : (x⁻¹ • H).Commensurable H
Tactic: rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
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
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} x⁻¹
have rwa₁ : H.Commensurable (x⁻¹ • H)
Tactic: rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Commensurable (goal)
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)
⊢ Membership.mem (γ := Set (ConjAct G)) {g : ConjAct G | (g • H).Commensurable H} x⁻¹
have rwa₂ : (x • H).Commensurable H
Tactic: rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
have rw : g₁ * g₂ * g₁⁻¹ * g₂⁻¹ = 1 ↔ g₁ * g₂ = g₂ * g₁
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
rw : g₁ * g₂ * g₁⁻¹ * g₂⁻¹ = 1 ↔ g₁ * g₂ = g₂ * g₁
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
have rw₁ : g₁ * g₂ * g₁⁻¹ = g₂ ↔ g₁ * g₂ = g₂ * g₁
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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₁
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
have rw₂ : g₁ * g₂ = g₂ * g₁ ↔ g₁ * g₂ = g₂ * g₁
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
have simp_rw : (g₁ * g₂ * g₁⁻¹ * g₂⁻¹)⁻¹ = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
Tactic: simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
simp_rw : (g₁ * g₂ * g₁⁻¹ * g₂⁻¹)⁻¹ = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
have simp_rw₁ : g₂⁻¹⁻¹ * (g₁⁻¹⁻¹ * (g₂⁻¹ * g₁⁻¹)) = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
Tactic: simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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₁⁻¹
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
have simp_rw₂ : g₂ * (g₁ * (g₂⁻¹ * g₁⁻¹)) = g₂ * g₁ * g₂⁻¹ * g₁⁻¹
Tactic: simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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
⊢ 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')
have 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')
Tactic: simp_rw [commutatorElement_def, map_mul f, map_inv f]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: simp_rw [commutatorElement_def, map_mul f, map_inv f]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer (↑H₂ : Set G)
have rw : (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆) ↔ H₁ ≤ centralizer (↑H₂ : Set G)
Tactic: rw [eq_bot_iff, commutator_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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)
have refine : ∀ (p : G) (_hp : p ∈ H₁) (q : G) (hq : q ∈ H₂), Membership.mem (γ := Subgroup G) ⊥ ⁅p, q⁆ ↔ q * p = p * q
Tactic: refine forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ Membership.mem (γ := Subgroup G) ⊥ ⁅p, q⁆ ↔ q * p = p * q
have rw : ⁅p, q⁆ = 1 ↔ q * p = p * q
Tactic: rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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
⊢ Membership.mem (γ := Subgroup G) ⊥ ⁅p, q⁆ ↔ q * p = p * q
have rw₁ : p * q = q * p ↔ q * p = p * q
Tactic: rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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
⊢ Membership.mem (γ := Subgroup G) ⊥ ⁅p, q⁆ ↔ q * p = p * q
have rw₂ : q * p = p * q ↔ q * p = p * q
Tactic: rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
have 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
Tactic: simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
    mem_centralizer_iff_commutator_eq_one] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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⁆⁆ = 1
have trans : ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
Tactic: trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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⁻¹
⊢ ⁅z, ⁅x, y⁆⁆ = 1
have trans₁ : x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
Tactic: trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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 * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
have rw : x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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₁, H₂⁆.Normal
have change : Normal (closure base)
Tactic: change (closure base).Normal
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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 base)
have rw : Normal (closure (Group.conjugatesOfSet base))
Tactic: rw [h_base]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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}
⊢ Normal (closure base)
have suffices : base = Group.conjugatesOfSet base
Tactic: suffices h_base : base = Group.conjugatesOfSet base by
    rw [h_base]
    exact Subgroup.normalClosure_normal
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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
have refine : ∀ (a : G) (h : a ∈ Group.conjugatesOfSet base), a ∈ base
Tactic: refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (hypothesis)
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 ∈ base
have h₃ : ∃ a_1 ∈ base, ∃ (c : G), c * a_1 * c⁻¹ = a
Tactic: simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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
⊢ a ∈ base
have rcases : ∀ (c : G) (hc : c ∈ H₁) (e : G) (he : e ∈ H₂) (d : G), d * ⁅c, e⁆ * d⁻¹ ∈ base
Tactic: rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Bracket.bracket (L := Subgroup G) ⊤ H ≤ H ↔ H.Normal
have refine : ∀ (hle : Bracket.bracket (L := Subgroup G) ⊤ H ≤ H) (h : G) (hh : h ∈ H) (g : G), g * h * g⁻¹ ∈ H
Tactic: refine ⟨fun hle ↦ ⟨fun h hh g ↦ ?_⟩, fun h ↦ commutator_le_right ⊤ H⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ normalizer (↑K : Set G) ↔ ⁅H, K⁆ ≤ K
have refine_1 : ∀ (hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K), ⁅H, K⁆ ≤ K
Tactic: refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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
⊢ H ≤ normalizer (↑K : Set G) ↔ ⁅H, K⁆ ≤ K
have refine_2 : ∀ (hH : ⁅H, K⁆ ≤ K) (h : G) (hh : h ∈ H) (k : G) (hk : k ∈ K), h * k * h⁻¹ ∈ K
Tactic: refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ≤ normalizer (↑⁅H₁, H₂⁆ : Set G)
have 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⁻¹)
Tactic: apply le_normalizer_closure_iff.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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₂
⊢ Membership.mem (γ := Subgroup G) (closure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}) (g * ⁅g₁, g₂⁆ * g⁻¹)
have apply : g * ⁅g₁, g₂⁆ * g⁻¹ * ⁅g, g₂⁆ ∈ ⁅H₁, H₂⁆
Tactic: apply (mul_mem_cancel_right <| commutator_mem_commutator hg hg₂).mp
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
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₂⁆ * g⁻¹ * ⁅g, g₂⁆ ∈ ⁅H₁, H₂⁆
have rw : ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
Tactic: rw [← commutatorElement_mul_left_eq_conj_mul g g₁ g₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer (↑⁅H₁, H₂⁆ : Set G)
have rw : H₂ ≤ normalizer (↑⁅H₂, H₁⁆ : Set G)
Tactic: rw [commutator_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
have 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₂⁆
Tactic: simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ (∀ 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₂⁆
have 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')
Tactic: constructor