awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.normalizerMonoidHom.ker = subgroupOf (centralizer (↑H : Set G)) (normalizer (↑H : Set G))

Tactic:
simp [Subgroup.ext_iff, DFunLike.ext_iff, Subtype.ext_iff,
    mem_subgroupOf, mem_centralizer_iff, eq_mul_inv_iff_mul_eq, eq_comm]

Premises used: Subgroup.mem_centralizer_iff, Subgroup.ext_iff, DFunLike.ext_iff, eq_comm, eq_mul_inv_iff_mul_eq, Subtype.ext_iff, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Monoid G
H : Submonoid G
⊢ H.PowSaturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

Tactic:
Iff.rfl

Premises used: Iff.rfl, Submonoid.PowSaturated
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H.toSubmonoid
⊢ HPow.hPow (β := ℤ) g (↑n : ℤ) ∈ H

Tactic:
simpa using hgn
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H.toSubmonoid
⊢ n = 0 ∨ g ∈ H.toSubmonoid

Tactic:
simpa using h n g (by simpa using hgn)

Premises used: Nat.cast
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine : ∀ (h : H.PowSaturated) (n : ℤ) (g : G) (hgn : g ^ n ∈ H), n = 0 ∨ g ∈ H
⊢ H.PowSaturated ↔ ∀ (n : ℤ) (g : G), 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)⟩
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
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
inr : ∀ (n : ℕ) (hgn : HPow.hPow (β := ℤ) g (-(↑n : ℤ)) ∈ H), Eq (α := ℤ) (-(↑n : ℤ)) 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : HPow.hPow (β := ℤ) g (↑n : ℤ) ∈ H
⊢ g ^ n ∈ H.toSubmonoid

Tactic:
simpa using hgn
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : HPow.hPow (β := ℤ) g (↑n : ℤ) ∈ H
⊢ Eq (α := ℤ) (↑n : ℤ) 0 ∨ g ∈ H

Tactic:
simpa using h (by simpa using hgn)
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : HPow.hPow (β := ℤ) g (-(↑n : ℤ)) ∈ H
⊢ g ^ n ∈ H.toSubmonoid

Tactic:
simpa using hgn
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : HPow.hPow (β := ℤ) g (-(↑n : ℤ)) ∈ H
⊢ Eq (α := ℤ) (-(↑n : ℤ)) 0 ∨ g ∈ H

Tactic:
simpa using h (by simpa using hgn)
-- Module: Mathlib.GroupTheory.Subgroup.Saturated
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : AddGroup A₁
inst_1 : AddMonoid A₂
inst_2 : IsAddTorsionFree A₂
f : A₁ →+ A₂
⊢ f.ker.NSMulSaturated

Tactic:
simp [NSMulSaturated, or_comm]

Premises used: AddSubmonoid.NSMulSaturated, or_comm
-- Module: Mathlib.GroupTheory.Subgroup.Simple
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
H : Subgroup G
Hn : H.Normal
⊢ H = ⊥ ∨ H = ⊤

Tactic:
IsSimpleGroup.eq_bot_or_eq_top_of_normal H Hn

Premises used: IsSimpleGroup.eq_bot_or_eq_top_of_normal
-- Module: Mathlib.GroupTheory.Subgroup.Simple
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw :
  (H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H'.subgroupOf H = ⊥ ∨ H'.subgroupOf H = ⊤) ↔
    H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H
⊢ IsSimpleGroup.{u_1} ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H

Tactic:
rw [isSimpleGroup_iff, H.nontrivial_iff_ne_bot, Subgroup.forall]

Premises used: Subgroup.forall, isSimpleGroup_iff, Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.GroupTheory.Subgroup.Simple
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H'.subgroupOf H = ⊥ ∨ H'.subgroupOf H = ⊤) ↔
    H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H

Tactic:
simp +contextual [disjoint_of_le_iff_left_eq_bot, LE.le.ge_iff_eq]

Premises used: disjoint_of_le_iff_left_eq_bot, LE.le.ge_iff_eq
-- Module: Mathlib.GroupTheory.Subgroup.Simple
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
C : Type u_3
inst_2 : CommGroup C
inst_3 : IsSimpleGroup C
⊢ IsSimpleOrder.{u_3} (Subgroup C)

Tactic:
⟨fun H => H.normal_of_isMulCommutative.eq_bot_or_eq_top⟩

Premises used: IsSimpleOrder.mk, Subgroup.normal_of_isMulCommutative, Subgroup.Normal.eq_bot_or_eq_top
-- Module: Mathlib.GroupTheory.Subgroup.Simple
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 = ⊤

Tactic:
(iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_

Premises used: Or.imp, Subgroup.Normal.eq_bot_or_eq_top, Subgroup.Normal.comap
-- Module: Mathlib.GroupTheory.Subgroup.Simple
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 = ⊥
refine_2 : ∀ (h : comap f H = ⊤), H = ⊤
⊢ H = ⊥ ∨ H = ⊤

Tactic:
refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_

Premises used: Or.imp, Subgroup.Normal.eq_bot_or_eq_top, Subgroup.Normal.comap
-- Module: Mathlib.GroupTheory.Subgroup.Simple
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)
refine_1₂ refine_1₃ : H = H
⊢ H = ⊥

Tactic:
rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]

Premises used: Subgroup.map_bot, Subgroup.map_comap_eq_self_of_surjective
-- Module: Mathlib.GroupTheory.Subgroup.Simple
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 = ⊤
⊢ comap f H = comap f ⊤

Tactic:
rw [← comap_top f] at h

Premises used: Subgroup.comap_top
-- Module: Mathlib.GroupTheory.Subgroup.Simple
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 = comap f ⊤
⊢ H = ⊤

Tactic:
comap_injective hf h

Premises used: Subgroup.comap_injective
-- Module: Mathlib.GroupTheory.Subgroup.Simple
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 = comap f ⊤
⊢ H = ⊤

Tactic:
exact comap_injective hf h

Premises used: Subgroup.comap_injective
-- Module: Mathlib.GroupTheory.Subgroup.Simple
Goal:
G : Type u_1
inst : Group G
H : Type u_3
inst_1 : Group H
inst_2 : IsSimpleGroup H
e : G ≃* H
⊢ IsSimpleGroup G

Tactic:
haveI : Nontrivial G := e.toEquiv.nontrivial
  isSimpleGroup_of_surjective e.symm.toMonoidHom e.symm.surjective

Premises used: MulEquiv.surjective, MulEquiv.toMonoidHom, IsSimpleGroup.isSimpleGroup_of_surjective, MulEquiv.symm
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : MulOneClass M
⊢ (↑(center M) : Set M) = Set.center M

Tactic:
rfl

Premises used: setOf, Set.center, rfl
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq (α := Subsemigroup M) (toSubsemigroup (center M)) (Subsemigroup.center M)

Tactic:
rfl

Premises used: Subsemigroup.center, rfl
-- Module: Mathlib.GroupTheory.Submonoid.Center
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 : α
⊢ ∀ (g : M), g * (↑c : M) = (↑c : M) * g

Tactic:
have := Semigroup.mem_center_iff.1 c.2
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
simp_rw₁ : ((↑c : M) * r) • v = (r * (↑c : M)) • v
⊢ c • r • v = r • c • v

Tactic:
simp_rw [Submonoid.smul_def, smul_smul, this]

Premises used: smul_smul, Submonoid.smul_def
-- Module: Mathlib.GroupTheory.Submonoid.Center
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 α
⊢ SMulCommClass M (↥(center M)) α

Tactic:
SMulCommClass.symm (Submonoid.center M) M α

Premises used: Membership.mem, Subtype, SMulCommClass.symm, Submonoid.center
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq (α := Monoid ↥(center M)) CommMonoid.toMonoid (toMonoid (center M))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq (α := Monoid ↥(center M)) CommMonoid.toMonoid (toMonoid (center M))

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
z : M
rw : Membership.mem (γ := Submonoid M) (center M) z ↔ z ∈ Set.center M
⊢ Membership.mem (γ := Submonoid M) (center M) z ↔ ∀ (g : M), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
z : M
⊢ Membership.mem (γ := Submonoid M) (center M) z ↔ z ∈ Set.center M

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.center
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
z : M
⊢ Membership.mem (γ := Submonoid M) (center M) z ↔ z ∈ Set.center M

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
⊢ SMulCommClass M (↥(center M)) M

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
⊢ SMulCommClass (↥(center M)) (↥(center M)) M

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : CommMonoid M
⊢ Eq (α := Submonoid M) (center M) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ M)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.GroupTheory.Submonoid.Center
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)
rw₆ rw₇ : (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : M) = (↑r : M) * (↑(↑u : ↥(Submonoid.center M)) : 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)

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]

Premises used: Units.val, Units.coe_map, IsMulCentral.comm, Submonoid.coe_subtype, Subtype.prop, Units.val_mul
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_1
inst : Monoid M
⊢ Function.Injective (α := (↥(Submonoid.center M))ˣ) (β := ↥(Submonoid.center Mˣ))
    (⇑(unitsCenterToCenterUnits M) : (a : (↥(Submonoid.center M))ˣ) → ↥(Submonoid.center Mˣ))

Tactic:
fun _a _b h => Units.ext <| Subtype.ext <| congr_arg (Units.val ∘ Subtype.val) h

Premises used: Units.val, Function.comp, Units.ext, congr_arg, Function.Injective, Subtype.val, Subtype.ext
-- Module: Mathlib.GroupTheory.Submonoid.Center
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)
change : Membership.mem (α := N) (Set.center N) ((e : (a : M) → N) x : N)
⊢ Membership.mem (α := N) (Set.center N) ((e_1 : (a : M) → N) x : N)

Tactic:
change e x ∈ Set.center N

Premises used: Set.center, DFunLike.coe
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
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)
⊢ Membership.mem (α := N) (Set.center N) ((e : (a : M) → N) x : N)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
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)
⊢ Commute ((e : (a : M) → N) x) a

Tactic:
apply e.symm.injective

Premises used: MulEquiv.symm, MulEquiv.injective
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
⊢ 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:
simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Premises used: IsMulCentral.comm, isMulCentral_iff, map_mul, Iff.mp, IsMulCentral.right_comm, Commute.eq, MulEquiv.symm_apply_apply
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
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)
⊢ HMul.hMul (α := N) ((e : (a : M) → N) x : N) (b * c) = HMul.hMul (α := N) ((e : (a : M) → N) x : N) b * c

Tactic:
apply e.symm.injective

Premises used: MulEquiv.symm, MulEquiv.injective
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
⊢ 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:
simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Premises used: IsMulCentral.comm, isMulCentral_iff, map_mul, Iff.mp, IsMulCentral.right_comm, Commute.eq, MulEquiv.symm_apply_apply
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
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)
⊢ HMul.hMul (β := N) (a * b) ((e : (a : M) → N) x : N) = a * HMul.hMul (β := N) b ((e : (a : M) → N) x : N)

Tactic:
apply e.symm.injective

Premises used: MulEquiv.symm, MulEquiv.injective
-- Module: Mathlib.GroupTheory.Submonoid.Center
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
⊢ 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:
simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Premises used: IsMulCentral.comm, isMulCentral_iff, map_mul, Iff.mp, IsMulCentral.right_comm, Commute.eq, MulEquiv.symm_apply_apply
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_2
inst : Mul M
x : M
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)
⊢ Membership.mem (γ := Set Mᵐᵒᵖ) (Set.center Mᵐᵒᵖ) (op x) ↔ x ∈ Set.center M

Tactic:
simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]

Premises used: MulOpposite.forall, isMulCentral_iff, Set.mem_center_iff, MulOpposite.op_inj, MulOpposite.op_mul
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_2
inst : Mul M
x : M
⊢ ((∀ (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:
aesop
-- Module: Mathlib.GroupTheory.Submonoid.Center
Goal:
M : Type u_2
inst : Mul M
x : Mᵐᵒᵖ
⊢ unop x ∈ Set.center M ↔ Membership.mem (γ := Set Mᵐᵒᵖ) (Set.center Mᵐᵒᵖ) x

Tactic:
op_mem_center_iff.symm

Premises used: Set.Mem, MulOpposite.op_mem_center_iff, MulOpposite, MulOpposite.unop, Iff.symm, MulOpposite.op
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
S : Set M
inst : Monoid M
⊢ (↑(centralizer S) : Set M) = S.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
S : Set M
inst : Monoid M
⊢ Eq (α := Subsemigroup M) (toSubsemigroup (centralizer S)) (Subsemigroup.centralizer S)

Tactic:
rfl

Premises used: Subsemigroup.centralizer, rfl
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
S : Set M
inst : Monoid M
z : M
⊢ Membership.mem (γ := Submonoid M) (centralizer S) z ↔ ∀ g ∈ S, g * z = z * g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ LE.le (α := Submonoid M) (center M) (centralizer s)

Tactic:
s.center_subset_centralizer

Premises used: Set.Mem, setOf, Set.center, Set.centralizer, Set.Subset, Set.center_subset_centralizer
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
S T : Set M
inst : Monoid M
h : S ⊆ T
⊢ LE.le (α := Submonoid M) (centralizer T) (centralizer S)

Tactic:
Set.centralizer_subset h

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ Eq (α := Submonoid M) (centralizer s) ⊤ ↔ s ⊆ (↑(center M) : Set M)

Tactic:
SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Premises used: Set.centralizer_eq_top_iff_subset, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq (α := Submonoid M) (centralizer Set.univ) (center M)

Tactic:
SetLike.ext' (Set.centralizer_univ M)

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Submonoid M
⊢ s ≤ centralizer (↑(centralizer (↑s : Set M)) : Set M)

Tactic:
Set.subset_centralizer_centralizer

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.subset_centralizer_centralizer
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Set M
a : (↑(centralizer s.centralizer.centralizer) : Set M) = (↑(centralizer s) : Set M)
⊢ Eq (α := Submonoid M) (centralizer s.centralizer.centralizer) (centralizer s)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ (↑(centralizer s.centralizer.centralizer) : Set M) = (↑(centralizer s) : Set M)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Premises used: Set.centralizer_centralizer_centralizer, Submonoid.coe_centralizer
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ LE.le (α := Submonoid M) (closure s) (centralizer (↑(centralizer s) : Set M))

Tactic:
closure_le.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Set.subset_centralizer_centralizer, Submonoid.closure_le
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
inst : Monoid M
s : Set M
hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a
⊢ IsMulCommutative.{u_1} ↥(closure s)

Tactic:
have := closure_le_centralizer_centralizer s
  .of_setLike_mul_comm fun _ h₁ _ h₂ ↦
    Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂)

Premises used: IsMulCommutative.of_setLike_mul_comm, Set.centralizer_centralizer_comm_of_comm, Submonoid.closure_le_centralizer_centralizer
-- Module: Mathlib.GroupTheory.Submonoid.Centralizer
Goal:
M : Type u_1
S_1 T : Set M
inst : Monoid M
S : Type u_2
inst_1 : SetLike S M
inst_2 : MulMemClass S M
s : S
inst_3 : IsMulCommutative.{u_1} ↥s
⊢ IsMulCommutative.{u_1} ↥(closure (↑s : Set M))

Tactic:
isMulCommutative_closure _ fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂

Premises used: setLike_mul_comm, Submonoid.isMulCommutative_closure
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
a b : ↥(IsUnit.submonoid M)
⊢ a * b = b * a

Tactic:
mul_comm a b

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.Submonoid.Inverses
Goal:
M : Type u_1
inst : CommMonoid M
a b : ↥(IsUnit.submonoid M)
⊢ a * b = b * a

Tactic:
convert! mul_comm a b

Premises used: mul_comm