awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
have refine_1 : ∀ (H : Subgroup G) (hH : Subgroup.IsComplement' (commutator G) H),
  ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
Tactic: obtain ⟨H, hH⟩ := Subgroup.exists_right_complement'_of_coprime hG.coprime_commutator_index
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
have refine_1 : ∀ (h1 : Abelianization G ≃* ↥H),
  ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
Tactic: have h1 : Abelianization G ≃* H := hH.symm.QuotientMulEquiv
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
h1 : Abelianization G ≃* ↥H
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
have refine_1 : (Nat.card.{u_1} ↥(commutator G)).Coprime (Nat.card.{u_1} ↥H)
Tactic: refine ⟨commutator G, H, _, (SemidirectProduct.mulEquivSubgroup hH).symm,
      isCyclic_of_surjective _ h1.surjective, hG.isCyclic_commutator, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic.{u_1} ↥H
hN : IsCyclic.{u_1} ↥N
hHN : (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
⊢ IsZGroup G
have this : IsZGroup.{u_1} (↥N ⋊[φ] ↥H)
Tactic: have : IsZGroup (N ⋊[φ] H) :=
      isZGroup_of_coprime SemidirectProduct.range_inl_eq_ker_rightHom.ge hHN
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_1
inst : Group G
z : G
⊢ Membership.mem (γ := Subgroup G) (center G) z ↔ ∀ (g : G), g * z = z * g
have rw : Membership.mem (γ := Subgroup G) (center G) z ↔ z ∈ Set.center G
Tactic: rw [← Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Characteristic (center G)
have refine : ∀ (ϕ : G ≃* G) (g : G) (hg : g ∈ comap ϕ.toMonoidHom (center G)), Membership.mem (γ := Subgroup G) (center G) g
Tactic: refine characteristic_iff_comap_le.mpr fun ϕ g hg => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_1
inst : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
⊢ Membership.mem (γ := Subgroup G) (center G) g
have rw : ∀ (g_1 : G), g_1 * g = g * g_1
Tactic: rw [mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_1
inst : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : G
⊢ h * g = g * h
have rw : HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) h : G) ((ϕ : (a : G) → G) g : G) =
  HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) g : G) ((ϕ : (a : G) → G) h : G)
Tactic: rw [← ϕ.injective.eq_iff, map_mul, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : CommGroup G
⊢ Eq (α := Subgroup G) (center G) ⊤
have rw : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
Tactic: rw [eq_top_iff']
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : CommGroup G
x : G
⊢ Membership.mem (γ := Subgroup G) (center G) x
have rw : ∀ (g : G), g * x = x * g
Tactic: rw [Subgroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (hypothesis)
Goal:
G : Type u_1
inst : Group G
h : Eq (α := Subgroup G) (center G) ⊤
⊢ ∀ (a b : G), a * b = b * a
have h₁ : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
Tactic: rw [eq_top_iff'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_1
inst : Group G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
__src : Group G := inst
x y : G
⊢ x * y = y * x
have apply : Membership.mem (γ := Subgroup G) (center G) y
Tactic: apply Subgroup.mem_center_iff.mp _ x
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
M : Type u_2
inst : Monoid M
g h : M
H : IsConj g h
Hg : g ∈ Set.center M
⊢ g = h
have rcases : ∀ (u : Mˣ) (hu : SemiconjBy (↑u : M) g h), g = h
Tactic: rcases H with ⟨u, hu⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
M : Type u_2
inst : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u : M) g h
⊢ g = h
have rwa : g * (↑u : M) = h * (↑u : M)
Tactic: rwa [← u.mul_left_inj, Hg.comm u]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
M : Type u_2
inst : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u : M) g h
rwa : g * (↑u : M) = h * (↑u : M)
⊢ g = h
have rwa₁ : (↑u : M) * g = h * (↑u : M)
Tactic: rwa [← u.mul_left_inj, Hg.comm u]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
⊢ Set.BijOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ
have refine_1 : ∀ (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G)),
  Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (ConjClasses.mk g)
Tactic: refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
refine_1 :
  ∀ (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G)),
    Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (ConjClasses.mk g)
⊢ Set.BijOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ
have refine_2 : ∀ (x : G) (hx : x ∈ (↑(Subgroup.center G) : Set G)),
  ∀ y ∈ (↑(Subgroup.center G) : Set G), ∀ (H : Eq (α := ConjClasses G) (ConjClasses.mk x) (ConjClasses.mk y)), x = y
Tactic: refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
refine_1 :
  ∀ (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G)),
    Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (ConjClasses.mk g)
refine_2 :
  ∀ (x : G) (hx : x ∈ (↑(Subgroup.center G) : Set G)),
    ∀ y ∈ (↑(Subgroup.center G) : Set G), ∀ (H : Eq (α := ConjClasses G) (ConjClasses.mk x) (ConjClasses.mk y)), x = y
⊢ Set.BijOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ
have refine_3 : Set.SurjOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ
Tactic: refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
⊢ Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (ConjClasses.mk g)
have refine_1 : (carrier (ConjClasses.mk g)).Subsingleton
Tactic: simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (hypothesis)
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x : G
hx : x ∈ carrier (ConjClasses.mk g)
y : G
hy : y ∈ carrier (ConjClasses.mk g)
⊢ x = y
have hx₁ : IsConj x g
Tactic: simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (hypothesis)
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x : G
hx : x ∈ carrier (ConjClasses.mk g)
y : G
hy : y ∈ carrier (ConjClasses.mk g)
hx₁ : IsConj x g
⊢ x = y
have hy₁ : IsConj y g
Tactic: simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ x = y
have refine_1 : g = y
Tactic: rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x y : G
hx : IsConj x g
hy : IsConj y g
refine_1 : g = y
⊢ x = y
have refine_1₁ : g = g
Tactic: rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (hypothesis)
Goal:
G : Type u_2
inst : Group G
x : G
hx : x ∈ (↑(Subgroup.center G) : Set G)
y : G
h : y ∈ (↑(Subgroup.center G) : Set G)
H : Eq (α := ConjClasses G) (ConjClasses.mk x) (ConjClasses.mk y)
⊢ x = y
have H₁ : IsConj x y
Tactic: rw [mk_eq_mk_iff_isConj] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ Membership.mem (γ := Set (ConjClasses G)) (ConjClasses.mk '' (↑(Subgroup.center G) : Set G))
    (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
have refine_3 : g ∈ (↑(Subgroup.center G) : Set G)
Tactic: refine ⟨g, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (hypothesis)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ g ∈ (↑(Subgroup.center G) : Set G)
have hg₁ : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
Tactic: simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
⊢ g ∈ (↑(Subgroup.center G) : Set G)
have refine_3 : ∀ (g_1 : G), g_1 * g = g * g_1
Tactic: rw [SetLike.mem_coe, Subgroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ h * g = g * h
have refine_3 : h * g * h⁻¹ = g
Tactic: rw [← mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ = g
have refine_3 : h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
Tactic: refine hg ?_ mem_carrier_mk
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
have refine_3 : Eq (α := ConjClasses G) (ConjClasses.mk (h * g * h⁻¹)) (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
Tactic: rw [mem_carrier_iff_mk_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ Eq (α := ConjClasses G) (ConjClasses.mk (h * g * h⁻¹)) (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
have refine_3 : IsConj (h * g * h⁻¹) g
Tactic: apply mk_eq_mk_iff_isConj.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Center (goal)
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ IsConj (h * g * h⁻¹) g
have refine_3 : ∃ (c : G), c * g * c⁻¹ = h * g * h⁻¹
Tactic: rw [isConj_comm, isConj_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
⊢ Membership.mem (γ := Subgroup G) (centralizer s) g ↔ ∀ h ∈ s, ⁅g, h⁆ = 1
have refine : ∀ x ∈ s, x * g = g * x ↔ ⁅g, x⁆ = 1
Tactic: refine forall₂_congr fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
x : G
h : x ∈ s
⊢ x * g = g * x ↔ ⁅g, x⁆ = 1
have rw : x * g = g * x ↔ g * x * g⁻¹ * x⁻¹ = 1
Tactic: rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
x : G
h : x ∈ s
rw : x * g = g * x ↔ g * x * g⁻¹ * x⁻¹ = 1
⊢ x * g = g * x ↔ ⁅g, x⁆ = 1
have rw₁ : x * g = g * x ↔ g * x * g⁻¹ = 1 * x
Tactic: rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
x : G
h : x ∈ s
rw : x * g = g * x ↔ g * x * g⁻¹ * x⁻¹ = 1
rw₁ : x * g = g * x ↔ g * x * g⁻¹ = 1 * x
⊢ x * g = g * x ↔ ⁅g, x⁆ = 1
have rw₂ : x * g = g * x ↔ g * x = 1 * x * g
Tactic: rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
x : G
h : x ∈ s
rw : x * g = g * x ↔ g * x * g⁻¹ * x⁻¹ = 1
rw₁ : x * g = g * x ↔ g * x * g⁻¹ = 1 * x
rw₂ : x * g = g * x ↔ g * x = 1 * x * g
⊢ x * g = g * x ↔ ⁅g, x⁆ = 1
have rw₃ : x * g = g * x ↔ g * x = x * g
Tactic: rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
x : G
h : x ∈ s
rw : x * g = g * x ↔ g * x * g⁻¹ * x⁻¹ = 1
rw₁ : x * g = g * x ↔ g * x * g⁻¹ = 1 * x
rw₂ : x * g = g * x ↔ g * x = 1 * x * g
rw₃ : x * g = g * x ↔ g * x = x * g
⊢ x * g = g * x ↔ ⁅g, x⁆ = 1
have rw₄ : g * x = x * g ↔ g * x = x * g
Tactic: rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g k : G
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) k ↔ k * g = g * k
have simp : g * k = k * g ↔ k * g = g * k
Tactic: simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ (↑(centralizer s) : Set G)
h : G
hh : h ∈ s
⊢ HMul.hMul (α := G') (β := G') ((f : (a : G) → G') h : G') ((f : (a : G) → G') g : G') =
    HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
have rw : (f : (a : G) → G') (h * g) = HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
Tactic: rw [← map_mul, ← map_mul, hg h hh]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ (↑(centralizer s) : Set G)
h : G
hh : h ∈ s
rw : (f : (a : G) → G') (h * g) = HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
⊢ HMul.hMul (α := G') (β := G') ((f : (a : G) → G') h : G') ((f : (a : G) → G') g : G') =
    HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
have rw₁ : Eq.{u_2 + 1} (α := G') ((f : (a : G) → G') (h * g) : G') ((f : (a : G) → G') (g * h) : G')
Tactic: rw [← map_mul, ← map_mul, hg h hh]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ (↑(centralizer s) : Set G)
h : G
hh : h ∈ s
rw : (f : (a : G) → G') (h * g) = HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
rw₁ : Eq.{u_2 + 1} (α := G') ((f : (a : G) → G') (h * g) : G') ((f : (a : G) → G') (g * h) : G')
⊢ HMul.hMul (α := G') (β := G') ((f : (a : G) → G') h : G') ((f : (a : G) → G') g : G') =
    HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
have rw₂ : Eq.{u_2 + 1} (α := G') ((f : (a : G) → G') (g * h) : G') ((f : (a : G) → G') (g * h) : G')
Tactic: rw [← map_mul, ← map_mul, hg h hh]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
⊢ Characteristic (centralizer (↑H : Set G))
have refine : ∀ (ϕ : G ≃* G) (g : G) (hg : g ∈ comap ϕ.toMonoidHom (centralizer (↑H : Set G))) (h : G) (hh : h ∈ (↑H : Set G)),
  Eq (α := G) ((ϕ : (a : G) → G) (h * g) : G) ((ϕ : (a : G) → G) (g * h) : G)
Tactic: refine Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer (↑H : Set G))
h : G
hh : h ∈ (↑H : Set G)
⊢ Eq (α := G) ((ϕ : (a : G) → G) (h * g) : G) ((ϕ : (a : G) → G) (g * h) : G)
have rw : HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) h : G) ((ϕ : (a : G) → G) g : G) =
  HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) g : G) ((ϕ : (a : G) → G) h : G)
Tactic: rw [map_mul, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
⊢ Eq (α := Subgroup G) (center G) (⨅ g ∈ s, centralizer {g})
have rw : Eq.{u_1 + 1} (α := Subgroup G) (centralizer Set.univ) (⨅ g ∈ s, centralizer {g})
Tactic: rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (centralizer Set.univ) (⨅ g ∈ s, centralizer {g})
⊢ Eq (α := Subgroup G) (center G) (⨅ g ∈ s, centralizer {g})
have rw₁ : Eq (α := Subgroup G) (centralizer (↑⊤ : Set G)) (⨅ g ∈ s, centralizer {g})
Tactic: rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (centralizer Set.univ) (⨅ g ∈ s, centralizer {g})
rw₁ : Eq (α := Subgroup G) (centralizer (↑⊤ : Set G)) (⨅ g ∈ s, centralizer {g})
⊢ Eq (α := Subgroup G) (center G) (⨅ g ∈ s, centralizer {g})
have rw₂ : Eq (α := Subgroup G) (centralizer (↑(closure s) : Set G)) (⨅ g ∈ s, centralizer {g})
Tactic: rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (centralizer Set.univ) (⨅ g ∈ s, centralizer {g})
rw₁ : Eq (α := Subgroup G) (centralizer (↑⊤ : Set G)) (⨅ g ∈ s, centralizer {g})
rw₂ : Eq (α := Subgroup G) (centralizer (↑(closure s) : Set G)) (⨅ g ∈ s, centralizer {g})
⊢ Eq (α := Subgroup G) (center G) (⨅ g ∈ s, centralizer {g})
have rw₃ : Eq (α := Subgroup G) (centralizer s) (⨅ g ∈ s, centralizer {g})
Tactic: rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (centralizer Set.univ) (⨅ g ∈ s, centralizer {g})
rw₁ : Eq (α := Subgroup G) (centralizer (↑⊤ : Set G)) (⨅ g ∈ s, centralizer {g})
rw₂ : Eq (α := Subgroup G) (centralizer (↑(closure s) : Set G)) (⨅ g ∈ s, centralizer {g})
rw₃ : Eq (α := Subgroup G) (centralizer s) (⨅ g ∈ s, centralizer {g})
⊢ Eq (α := Subgroup G) (center G) (⨅ g ∈ s, centralizer {g})
have rw₄ : Eq.{u_1 + 1} (α := Subgroup G) (⨅ g ∈ s, centralizer {g}) (⨅ g ∈ s, centralizer {g})
Tactic: rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
⊢ Eq (α := Subgroup G) (center G) (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
have rw : Eq.{u_1 + 1} (α := Subgroup G) (⨅ g ∈ s, centralizer {g}) (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
Tactic: rw [center_eq_iInf hs, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (⨅ g ∈ s, centralizer {g}) (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
⊢ Eq (α := Subgroup G) (center G) (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
have rw₁ : Eq.{u_1 + 1} (α := Subgroup G) (⨅ (i : (↑s : Type u_1)), centralizer {(↑i : G)})
  (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
Tactic: rw [center_eq_iInf hs, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ LE.le (α := Subgroup G) (centralizer s) (normalizer s)
have refine_1 : ∀ (g : G) (hg : Membership.mem (γ := Subgroup G) (centralizer s) g) (h : G) (hh : h ∈ s), g * h * g⁻¹ ∈ s
Tactic: refine fun g hg h ↦ ⟨fun hh ↦ ?_, fun hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
refine_1 : ∀ (g : G) (hg : Membership.mem (γ := Subgroup G) (centralizer s) g) (h : G) (hh : h ∈ s), g * h * g⁻¹ ∈ s
⊢ LE.le (α := Subgroup G) (centralizer s) (normalizer s)
have refine_2 : ∀ (g : G) (hg : Membership.mem (γ := Subgroup G) (centralizer s) g) (h : G) (hh : g * h * g⁻¹ ∈ s), h ∈ s
Tactic: refine fun g hg h ↦ ⟨fun hh ↦ ?_, fun hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (centralizer s) g
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s
have h₁ : h = g * h * g⁻¹
Tactic: convert! hh
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
⊢ Normal (G := ↥(normalizer s)) (subgroupOf (centralizer s) (normalizer s))
have refine : ∀ (c n : G) (hc : Membership.mem (γ := Subgroup G) (centralizer s) c)
  (hn : Membership.mem (γ := Subgroup G) (normalizer s) n),
  Membership.mem (γ := Subgroup G) (centralizer s) (n * c * n⁻¹)
Tactic: refine (Subgroup.normal_subgroupOf_iff <| centralizer_le_normalizer s).mpr fun c n hc hn ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : Membership.mem (γ := Subgroup G) (centralizer s) c
hn : Membership.mem (γ := Subgroup G) (normalizer s) n
⊢ Membership.mem (γ := Subgroup G) (centralizer s) (n * c * n⁻¹)
have refine : ∀ (g : G) (hg : g ∈ s), ⁅n * c * n⁻¹, g⁆ = 1
Tactic: refine mem_centralizer_iff_commutator_eq_one'.mpr fun g hg ↦ ?_