awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : G
hg : g ∈ s
⊢ ⁅n * c * n⁻¹, g⁆ = 1
have suffices : n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1
Tactic: suffices n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1 by simpa [commutatorElement_def, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Eq (α := Subgroup G) (normalizer {g}) (centralizer {g})
have refine_1 : ∀ (h : G), Membership.mem (γ := Subgroup G) (normalizer {g}) h → Membership.mem (γ := Subgroup G) (centralizer {g}) h
Tactic: refine ext fun h ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g : G
refine_1 :
  ∀ (h : G), Membership.mem (γ := Subgroup G) (normalizer {g}) h → Membership.mem (γ := Subgroup G) (centralizer {g}) h
⊢ Eq (α := Subgroup G) (normalizer {g}) (centralizer {g})
have refine_2 : ∀ (h : G), Membership.mem (γ := Subgroup G) (centralizer {g}) h → Membership.mem (γ := Subgroup G) (normalizer {g}) h
Tactic: refine ext fun h ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g h : G
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) h → Membership.mem (γ := Subgroup G) (normalizer {g}) h
have refine_2 : ∀ (hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h) (g_1 : G),
  Membership.mem (γ := Set G) {g} g_1 → Membership.mem (γ := Set G) {g} (h * g_1 * h⁻¹)
Tactic: refine fun hh g ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Centralizer (goal)
Goal:
G : Type u_1
inst : Group G
g h : G
refine_2 :
  ∀ (hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h) (g_1 : G),
    Membership.mem (γ := Set G) {g} g_1 → Membership.mem (γ := Set G) {g} (h * g_1 * h⁻¹)
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) h → Membership.mem (γ := Subgroup G) (normalizer {g}) h
have refine_2₁ : ∀ (hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h) (g_1 : G),
  Membership.mem (γ := Set G) {g} (h * g_1 * h⁻¹) → Membership.mem (γ := Set G) {g} g_1
Tactic: refine fun hh g ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Saturated (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.PowSaturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
have refine : ∀ (h : H.PowSaturated) (n : ℤ) (g : G) (hgn : g ^ n ∈ H), n = 0 ∨ g ∈ H
Tactic: refine ⟨fun h n g hgn ↦ ?_, fun h n g hgn ↦ by simpa using h n g (by simpa using hgn)⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Saturated (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.PowSaturated
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
have inl : ∀ (n : ℕ) (hgn : HPow.hPow (β := ℤ) g (↑n : ℤ) ∈ H), Eq (α := ℤ) (↑n : ℤ) 0 ∨ g ∈ H
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hgn
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Saturated (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.PowSaturated
n : ℤ
g : G
hgn : g ^ n ∈ H
inl : ∀ (n : ℕ) (hgn : HPow.hPow (β := ℤ) g (↑n : ℤ) ∈ H), Eq (α := ℤ) (↑n : ℤ) 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
have inr : ∀ (n : ℕ) (hgn : HPow.hPow (β := ℤ) g (-(↑n : ℤ)) ∈ H), Eq (α := ℤ) (-(↑n : ℤ)) 0 ∨ g ∈ H
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hgn
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsSimpleGroup.{u_1} ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H
have rw : (H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H'.subgroupOf H = ⊥ ∨ H'.subgroupOf H = ⊤) ↔
  H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H
Tactic: rw [isSimpleGroup_iff, H.nontrivial_iff_ne_bot, Subgroup.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Type u_3
inst_1 : Group H_1
inst_2 : IsSimpleGroup G
inst_3 : Nontrivial H_1
f : G →* H_1
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H_1) (⇑f : (a : G) → H_1)
H : Subgroup H_1
iH : H.Normal
⊢ H = ⊥ ∨ H = ⊤
have refine_1 : ∀ (h : comap f H = ⊥), H = ⊥
Tactic: refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Type u_3
inst_1 : Group H_1
inst_2 : IsSimpleGroup G
inst_3 : Nontrivial H_1
f : G →* H_1
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H_1) (⇑f : (a : G) → H_1)
H : Subgroup H_1
iH : H.Normal
refine_1 : ∀ (h : comap f H = ⊥), H = ⊥
⊢ H = ⊥ ∨ H = ⊤
have refine_2 : ∀ (h : comap f H = ⊤), H = ⊤
Tactic: refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Type u_3
inst_1 : Group H_1
inst_2 : IsSimpleGroup G
inst_3 : Nontrivial H_1
f : G →* H_1
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H_1) (⇑f : (a : G) → H_1)
H : Subgroup H_1
iH : H.Normal
h : comap f H = ⊥
⊢ H = ⊥
have refine_1 : H = map f ⊥
Tactic: rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Type u_3
inst_1 : Group H_1
inst_2 : IsSimpleGroup G
inst_3 : Nontrivial H_1
f : G →* H_1
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H_1) (⇑f : (a : G) → H_1)
H : Subgroup H_1
iH : H.Normal
h : comap f H = ⊥
refine_1 : H = map f ⊥
⊢ H = ⊥
have refine_1₁ : H = map f (comap f H)
Tactic: rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Type u_3
inst_1 : Group H_1
inst_2 : IsSimpleGroup G
inst_3 : Nontrivial H_1
f : G →* H_1
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H_1) (⇑f : (a : G) → H_1)
H : Subgroup H_1
iH : H.Normal
h : comap f H = ⊥
refine_1 : H = map f ⊥
refine_1₁ : H = map f (comap f H)
⊢ H = ⊥
have refine_1₂ : H = H
Tactic: rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Subgroup.Simple (hypothesis)
Goal:
G : Type u_1
inst : Group G
H_1 : Type u_3
inst_1 : Group H_1
inst_2 : IsSimpleGroup G
inst_3 : Nontrivial H_1
f : G →* H_1
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H_1) (⇑f : (a : G) → H_1)
H : Subgroup H_1
iH : H.Normal
h : comap f H = ⊤
⊢ H = ⊤
have h₁ : comap f H = comap f ⊤
Tactic: rw [← comap_top f] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (hypothesis)
Goal:
M_1 : Type u_1
inst : MulOneClass M_1
M : Type u_2
α : Type u_3
inst_1 : Monoid M
inst_2 : MulAction M α
c : ↥(center M)
r : M
v : α
⊢ c • r • v = r • c • v
have this : ∀ (g : M), g * (↑c : M) = (↑c : M) * g
Tactic: have := Semigroup.mem_center_iff.1 c.2
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M_1 : Type u_1
inst : MulOneClass M_1
M : Type u_2
α : Type u_3
inst_1 : Monoid M
inst_2 : MulAction M α
c : ↥(center M)
r : M
v : α
this : ∀ (g : M), g * (↑c : M) = (↑c : M) * g
⊢ c • r • v = r • c • v
have simp_rw : (↑c : M) • r • v = r • (↑c : M) • v
Tactic: simp_rw [Submonoid.smul_def, smul_smul, this]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M_1 : Type u_1
inst : MulOneClass M_1
M : Type u_2
α : Type u_3
inst_1 : Monoid M
inst_2 : MulAction M α
c : ↥(center M)
r : M
v : α
this : ∀ (g : M), g * (↑c : M) = (↑c : M) * g
simp_rw : (↑c : M) • r • v = r • (↑c : M) • v
⊢ c • r • v = r • c • v
have simp_rw₁ : ((↑c : M) * r) • v = (r * (↑c : M)) • v
Tactic: simp_rw [Submonoid.smul_def, smul_smul, this]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
z : M
⊢ Membership.mem (γ := Submonoid M) (center M) z ↔ ∀ (g : M), g * z = z * g
have rw : Membership.mem (γ := Submonoid M) (center M) z ↔ z ∈ Set.center M
Tactic: rw [← Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw : (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
  (↑(HMul.hMul (α := Mˣ)
        ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
    M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
rw :
  (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw₁ : HMul.hMul (β := M) (↑r : M)
    ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M) =
  (↑(HMul.hMul (α := Mˣ)
        ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
    M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
rw :
  (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₁ :
  HMul.hMul (β := M) (↑r : M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw₂ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
  (↑(HMul.hMul (α := Mˣ)
        ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
    M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
rw :
  (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₁ :
  HMul.hMul (β := M) (↑r : M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₂ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw₃ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
  (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) * (↑r : M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
rw :
  (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₁ :
  HMul.hMul (β := M) (↑r : M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₂ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₃ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) * (↑r : M)
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw₄ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
  HMul.hMul (α := M)
    ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M)
    (↑r : M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
rw :
  (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₁ :
  HMul.hMul (β := M) (↑r : M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₂ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₃ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) * (↑r : M)
rw₄ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    HMul.hMul (α := M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M)
      (↑r : M)
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw₅ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) = (↑(↑u : ↥(Submonoid.center M)) : M) * (↑r : M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
rw :
  (↑r : M) * (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₁ :
  HMul.hMul (β := M) (↑r : M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₂ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
rw₃ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    (↑((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u) : M) * (↑r : M)
rw₄ :
  (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) =
    HMul.hMul (α := M)
      ((Submonoid.subtype (Submonoid.center M) : (a : ↥(Submonoid.center M)) → M) (↑u : ↥(Submonoid.center M)) : M)
      (↑r : M)
rw₅ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) = (↑(↑u : ↥(Submonoid.center M)) : M) * (↑r : M)
⊢ (↑(HMul.hMul (β := Mˣ) r
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ)) :
      M) =
    (↑(HMul.hMul (α := Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.center M)) : (a : (↥(Submonoid.center M))ˣ) → Mˣ) u : Mˣ) r) :
      M)
have rw₆ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) = (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M)
Tactic: rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
⊢ Membership.mem (α := N) (Set.center N) ((e_1 : (a : M) → N) x : N)
have change : Membership.mem (α := N) (Set.center N) ((e : (a : M) → N) x : N)
Tactic: change e x ∈ Set.center N
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
⊢ Membership.mem (α := N) (Set.center N) ((e : (a : M) → N) x : N)
have comm : ∀ (a : N), Commute ((e : (a : M) → N) x) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
comm : ∀ (a : N), Commute ((e : (a : M) → N) x) a
⊢ Membership.mem (α := N) (Set.center N) ((e : (a : M) → N) x : N)
have left_assoc : ∀ (b c : N), HMul.hMul (α := N) ((e : (a : M) → N) x : N) (b * c) = HMul.hMul (α := N) ((e : (a : M) → N) x : N) b * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
comm : ∀ (a : N), Commute ((e : (a : M) → N) x) a
left_assoc :
  ∀ (b c : N), HMul.hMul (α := N) ((e : (a : M) → N) x : N) (b * c) = HMul.hMul (α := N) ((e : (a : M) → N) x : N) b * c
⊢ Membership.mem (α := N) (Set.center N) ((e : (a : M) → N) x : N)
have right_assoc : ∀ (a b : N), HMul.hMul (β := N) (a * b) ((e : (a : M) → N) x : N) = a * HMul.hMul (β := N) b ((e : (a : M) → N) x : N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
a : N
⊢ Commute ((e : (a : M) → N) x) a
have comm : Eq.{u_3 + 1} (α := M) ((e.symm : (a : N) → M) (HMul.hMul (α := N) ((e : (a : M) → N) x : N) a) : M)
  ((e.symm : (a : N) → M) (HMul.hMul (β := N) a ((e : (a : M) → N) x : N)) : M)
Tactic: apply e.symm.injective
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
b c : N
⊢ HMul.hMul (α := N) ((e : (a : M) → N) x : N) (b * c) = HMul.hMul (α := N) ((e : (a : M) → N) x : N) b * c
have left_assoc : Eq.{u_3 + 1} (α := M) ((e.symm : (a : N) → M) (HMul.hMul (α := N) ((e : (a : M) → N) x : N) (b * c)) : M)
  ((e.symm : (a : N) → M) (HMul.hMul (α := N) ((e : (a : M) → N) x : N) b * c) : M)
Tactic: apply e.symm.injective
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_3
N : Type u_1
F : Type u_2
inst : EquivLike F M N
inst_1 : Mul M
inst_2 : Mul N
inst_3 : MulEquivClass F M N
e_1 : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := (↑e_1 : M ≃* N)
a b : N
⊢ HMul.hMul (β := N) (a * b) ((e : (a : M) → N) x : N) = a * HMul.hMul (β := N) b ((e : (a : M) → N) x : N)
have right_assoc : Eq.{u_3 + 1} (α := M) ((e.symm : (a : N) → M) (HMul.hMul (β := N) (a * b) ((e : (a : M) → N) x : N)) : M)
  ((e.symm : (a : N) → M) (a * HMul.hMul (β := N) b ((e : (a : M) → N) x : N)) : M)
Tactic: apply e.symm.injective
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Center (goal)
Goal:
M : Type u_2
inst : Mul M
x : M
⊢ Membership.mem (γ := Set Mᵐᵒᵖ) (Set.center Mᵐᵒᵖ) (op x) ↔ x ∈ Set.center M
have simp_rw : ((∀ (a : M), Commute (op x) (op a)) ∧
    (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
  (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)
Tactic: simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Centralizer (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ Eq (α := Submonoid M) (centralizer s.centralizer.centralizer) (centralizer s)
have a : (↑(centralizer s.centralizer.centralizer) : Set M) = (↑(centralizer s) : Set M)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * (↑z : M) = 1
h₂ : x * y = 1
⊢ x ∈ S
have h : x = (↑z : M)
Tactic: convert! z.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * (↑z : M) = 1
h₂ : x * y = 1
⊢ x = (↑z : M)
have h : x * 1 = (↑z : M)
Tactic: rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Submonoid.Inverses (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * (↑z : M) = 1
h₂ : x * y = 1
h : x * 1 = (↑z : M)
⊢ x = (↑z : M)
have h₃ : x * (y * (↑z : M)) = (↑z : M)
Tactic: rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]