/-
Copyright (c) 2021 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser, Jireh Loreaux

! This file was ported from Lean 3 source module group_theory.subsemigroup.center
! leanprover-community/mathlib commit a437a2499163d85d670479f69f625f461cc5fef9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Ring.Defs
import Mathlib.GroupTheory.Subsemigroup.Operations

/-!
# Centers of magmas and semigroups

## Main definitions

* `Set.center`: the center of a magma
* `Subsemigroup.center`: the center of a semigroup
* `Set.addCenter`: the center of an additive magma
* `AddSubsemigroup.center`: the center of an additive semigroup

We provide `Submonoid.center`, `AddSubmonoid.center`, `Subgroup.center`, `AddSubgroup.center`,
`Subsemiring.center`, and `Subring.center` in other files.
-/


variable {M: Type ?u.9827
M : Type _: Type (?u.16689+1)
Type _}

namespace Set

variable (M: ?m.8
M)

/-- The center of a magma. -/
@[to_additive addCenter: (M : Type u_1) → [inst : Add M] → Set M
addCenter " The center of an additive magma. "]
def center: (M : Type u_1) → [inst : Mul M] → Set M
center [Mul: Type ?u.14 → Type ?u.14
Mul M: Type ?u.11
M] : Set: Type ?u.17 → Type ?u.17
Set M: Type ?u.11
M :=
  { z: ?m.26
z | ∀ m: ?m.29
m, m: ?m.29
m * z: ?m.26
z = z: ?m.26
z * m: ?m.29
m }
#align set.center Set.center: (M : Type u_1) → [inst : Mul M] → Set M
Set.center
#align set.add_center Set.addCenter: (M : Type u_1) → [inst : Add M] → Set M
Set.addCenter

-- porting note: The `to_additive` version used to be `mem_addCenter` without the iff
@[to_additive mem_addCenter_iff: ∀ (M : Type u_1) [inst : Add M] {z : M}, z ∈ addCenter M ↔ ∀ (g : M), g + z = z + g
mem_addCenter_iff]
theorem mem_center_iff: ∀ (M : Type u_1) [inst : Mul M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff [Mul: Type ?u.145 → Type ?u.145
Mul M: Type ?u.142
M] {z: M
z : M: Type ?u.142
M} : z: M
z ∈ center: (M : Type ?u.155) → [inst : Mul M] → Set M
center M: Type ?u.142
M ↔ ∀ g: ?m.180
g, g: ?m.180
g * z: M
z = z: M
z * g: ?m.180
g :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align set.mem_center_iff Set.mem_center_iff: ∀ (M : Type u_1) [inst : Mul M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
Set.mem_center_iff
#align set.mem_add_center Set.mem_addCenter_iff: ∀ (M : Type u_1) [inst : Add M] {z : M}, z ∈ addCenter M ↔ ∀ (g : M), g + z = z + g
Set.mem_addCenter_iff

instance decidableMemCenter: [inst : Mul M] → [inst_1 : (a : M) → Decidable (∀ (b : M), b * a = a * b)] → DecidablePred fun x => x ∈ center M
decidableMemCenter [Mul: Type ?u.286 → Type ?u.286
Mul M: Type ?u.283
M] [∀ a: M
a : M: Type ?u.283
M, Decidable: Prop → Type
Decidable <| ∀ b: M
b : M: Type ?u.283
M, b: M
b * a: M
a = a: M
a * b: M
b] :
    DecidablePred: {α : Sort ?u.375} → (α → Prop) → Sort (max1?u.375)
DecidablePred (· ∈ center: (M : Type ?u.385) → [inst : Mul M] → Set M
center M: Type ?u.283
M) := fun _: ?m.419
_ => decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' _: Prop
_ (mem_center_iff: ∀ (M : Type ?u.425) [inst : Mul M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff M: Type ?u.283
M)
#align set.decidable_mem_center Set.decidableMemCenter: (M : Type u_1) →
  [inst : Mul M] → [inst_1 : (a : M) → Decidable (∀ (b : M), b * a = a * b)] → DecidablePred fun x => x ∈ center M
Set.decidableMemCenter

@[to_additive (attr := simp) zero_mem_addCenter: ∀ (M : Type u_1) [inst : AddZeroClass M], 0 ∈ addCenter M
zero_mem_addCenter]
theorem one_mem_center: ∀ [inst : MulOneClass M], 1 ∈ center M
one_mem_center [MulOneClass: Type ?u.541 → Type ?u.541
MulOneClass M: Type ?u.538
M] : (1: ?m.563
1 : M: Type ?u.538
M) ∈ Set.center: (M : Type ?u.832) → [inst : Mul M] → Set M
Set.center M: Type ?u.538
M := by
Goals accomplished! 🐙 M: Type u_1

inst✝: MulOneClass M

1 ∈ center Msimp [mem_center_iff: ∀ (M : Type ?u.1013) [inst : Mul M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff]
Goals accomplished! 🐙
#align set.one_mem_center Set.one_mem_center: ∀ (M : Type u_1) [inst : MulOneClass M], 1 ∈ center M
Set.one_mem_center
#align set.zero_mem_add_center Set.zero_mem_addCenter: ∀ (M : Type u_1) [inst : AddZeroClass M], 0 ∈ addCenter M
Set.zero_mem_addCenter

@[simp]
theorem zero_mem_center: ∀ (M : Type u_1) [inst : MulZeroClass M], 0 ∈ center M
zero_mem_center [MulZeroClass: Type ?u.2064 → Type ?u.2064
MulZeroClass M: Type ?u.2061
M] : (0: ?m.2086
0 : M: Type ?u.2061
M) ∈ Set.center: (M : Type ?u.2251) → [inst : Mul M] → Set M
Set.center M: Type ?u.2061
M := by
Goals accomplished! 🐙 M: Type u_1

inst✝: MulZeroClass M

0 ∈ center Msimp [mem_center_iff: ∀ (M : Type ?u.2363) [inst : Mul M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff]
Goals accomplished! 🐙
#align set.zero_mem_center Set.zero_mem_center: ∀ (M : Type u_1) [inst : MulZeroClass M], 0 ∈ center M
Set.zero_mem_center

variable {M: ?m.3415
M}

@[to_additive (attr := simp) add_mem_addCenter: ∀ {M : Type u_1} [inst : AddSemigroup M] {a b : M}, a ∈ addCenter M → b ∈ addCenter M → a + b ∈ addCenter M
add_mem_addCenter]
theorem mul_mem_center: ∀ {M : Type u_1} [inst : Semigroup M] {a b : M}, a ∈ center M → b ∈ center M → a * b ∈ center M
mul_mem_center [Semigroup: Type ?u.3421 → Type ?u.3421
Semigroup M: Type ?u.3418
M] {a: M
a b: M
b : M: Type ?u.3418
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.3445) → [inst : Mul M] → Set M
Set.center M: Type ?u.3418
M) (hb: b ∈ center M
hb : b: M
b ∈ Set.center: (M : Type ?u.3782) → [inst : Mul M] → Set M
Set.center M: Type ?u.3418
M) :
    a: M
a * b: M
b ∈ Set.center: (M : Type ?u.4302) → [inst : Mul M] → Set M
Set.center M: Type ?u.3418
M := fun g: ?m.4317
g => by
Goals accomplished! 🐙 M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * b * grw [M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * b * gmul_assoc: ∀ {G : Type ?u.4323} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * (b * g) M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * b * g← hb: b ∈ center M
hb g: M
g,M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * (g * b) M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * b * g← mul_assoc: ∀ {G : Type ?u.4395} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * a * b = a * (g * b) M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * b * gha: a ∈ center M
ha g: M
g,M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

a * g * b = a * (g * b) M: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

g * (a * b) = a * b * gmul_assoc: ∀ {G : Type ?u.4441} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assocM: Type u_1

inst✝: Semigroup M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

g: M

a * (g * b) = a * (g * b)]
Goals accomplished! 🐙
#align set.mul_mem_center Set.mul_mem_center: ∀ {M : Type u_1} [inst : Semigroup M] {a b : M}, a ∈ center M → b ∈ center M → a * b ∈ center M
Set.mul_mem_center
#align set.add_mem_add_center Set.add_mem_addCenter: ∀ {M : Type u_1} [inst : AddSemigroup M] {a b : M}, a ∈ addCenter M → b ∈ addCenter M → a + b ∈ addCenter M
Set.add_mem_addCenter

@[to_additive (attr := simp) neg_mem_addCenter: ∀ {M : Type u_1} [inst : AddGroup M] {a : M}, a ∈ addCenter M → -a ∈ addCenter M
neg_mem_addCenter]
theorem inv_mem_center: ∀ [inst : Group M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
inv_mem_center [Group: Type ?u.4604 → Type ?u.4604
Group M: Type ?u.4601
M] {a: M
a : M: Type ?u.4601
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.4626) → [inst : Mul M] → Set M
Set.center M: Type ?u.4601
M) :
    a: M
a⁻¹ ∈ Set.center: (M : Type ?u.4945) → [inst : Mul M] → Set M
Set.center M: Type ?u.4601
M := fun g: ?m.4956
g => by
Goals accomplished! 🐙
  M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * grw [M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * g← inv_inj: ∀ {G : Type ?u.4962} [inst : InvolutiveInv G] {a b : G}, a⁻¹ = b⁻¹ ↔ a = b
inv_inj,M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

(g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹ M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * gmul_inv_rev: ∀ {G : Type ?u.5033} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev,M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

a⁻¹⁻¹ * g⁻¹ = (a⁻¹ * g)⁻¹ M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * ginv_inv: ∀ {G : Type ?u.5113} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_inv,M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

a * g⁻¹ = (a⁻¹ * g)⁻¹ M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * g← ha: a ∈ center M
ha,M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g⁻¹ * a = (a⁻¹ * g)⁻¹ M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * gmul_inv_rev: ∀ {G : Type ?u.5161} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev,M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g⁻¹ * a = g⁻¹ * a⁻¹⁻¹ M: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g * a⁻¹ = a⁻¹ * ginv_inv: ∀ {G : Type ?u.5238} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_invM: Type u_1

inst✝: Group M

a: M

ha: a ∈ center M

g: M

g⁻¹ * a = g⁻¹ * a]
Goals accomplished! 🐙
#align set.inv_mem_center Set.inv_mem_center: ∀ {M : Type u_1} [inst : Group M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
Set.inv_mem_center
#align set.neg_mem_add_center Set.neg_mem_addCenter: ∀ {M : Type u_1} [inst : AddGroup M] {a : M}, a ∈ addCenter M → -a ∈ addCenter M
Set.neg_mem_addCenter

@[simp]
theorem add_mem_center: ∀ {M : Type u_1} [inst : Distrib M] {a b : M}, a ∈ center M → b ∈ center M → a + b ∈ center M
add_mem_center [Distrib: Type ?u.5423 → Type ?u.5423
Distrib M: Type ?u.5420
M] {a: M
a b: M
b : M: Type ?u.5420
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.5447) → [inst : Mul M] → Set M
Set.center M: Type ?u.5420
M) (hb: b ∈ center M
hb : b: M
b ∈ Set.center: (M : Type ?u.5585) → [inst : Mul M] → Set M
Set.center M: Type ?u.5420
M) :
    a: M
a + b: M
b ∈ Set.center: (M : Type ?u.5653) → [inst : Mul M] → Set M
Set.center M: Type ?u.5420
M := fun c: ?m.5668
c => by
Goals accomplished! 🐙 M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * (a + b) = (a + b) * crw [M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * (a + b) = (a + b) * cadd_mul: ∀ {R : Type ?u.5674} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
  (a + b) * c = a * c + b * c
add_mul,M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * (a + b) = a * c + b * c M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * (a + b) = (a + b) * cmul_add: ∀ {R : Type ?u.6000} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
  a * (b + c) = a * b + a * c
mul_add,M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * a + c * b = a * c + b * c M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * (a + b) = (a + b) * cha: a ∈ center M
ha c: M
c,M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

a * c + c * b = a * c + b * c M: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

c * (a + b) = (a + b) * chb: b ∈ center M
hb c: M
cM: Type u_1

inst✝: Distrib M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

c: M

a * c + b * c = a * c + b * c]
Goals accomplished! 🐙
#align set.add_mem_center Set.add_mem_center: ∀ {M : Type u_1} [inst : Distrib M] {a b : M}, a ∈ center M → b ∈ center M → a + b ∈ center M
Set.add_mem_center

@[simp]
theorem neg_mem_center: ∀ {M : Type u_1} [inst : Ring M] {a : M}, a ∈ center M → -a ∈ center M
neg_mem_center [Ring: Type ?u.6236 → Type ?u.6236
Ring M: Type ?u.6233
M] {a: M
a : M: Type ?u.6233
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.6258) → [inst : Mul M] → Set M
Set.center M: Type ?u.6233
M) : -a: M
a ∈ Set.center: (M : Type ?u.6332) → [inst : Mul M] → Set M
Set.center M: Type ?u.6233
M := fun c: ?m.6343
c => by
Goals accomplished! 🐙
  M: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

c * -a = -a * crw [M: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

c * -a = -a * c← neg_mul_comm: ∀ {α : Type ?u.6349} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * b = a * -b
neg_mul_comm,M: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

-c * a = -a * c M: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

c * -a = -a * cha: a ∈ center M
ha (-c: M
c),M: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

a * -c = -a * c M: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

c * -a = -a * cneg_mul_comm: ∀ {α : Type ?u.6563} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * b = a * -b
neg_mul_commM: Type u_1

inst✝: Ring M

a: M

ha: a ∈ center M

c: M

a * -c = a * -c]
Goals accomplished! 🐙
#align set.neg_mem_center Set.neg_mem_center: ∀ {M : Type u_1} [inst : Ring M] {a : M}, a ∈ center M → -a ∈ center M
Set.neg_mem_center

@[to_additive subset_addCenter_add_units: ∀ {M : Type u_1} [inst : AddMonoid M], AddUnits.val ⁻¹' addCenter M ⊆ addCenter (AddUnits M)
subset_addCenter_add_units]
theorem subset_center_units: ∀ {M : Type u_1} [inst : Monoid M], Units.val ⁻¹' center M ⊆ center Mˣ
subset_center_units [Monoid: Type ?u.6830 → Type ?u.6830
Monoid M: Type ?u.6827
M] : ((↑): Mˣ → M
(↑) : M: Type ?u.6827
Mˣ → M: Type ?u.6827
M) ⁻¹' center: (M : Type ?u.7729) → [inst : Mul M] → Set M
center M: Type ?u.6827
M ⊆ Set.center: (M : Type ?u.7926) → [inst : Mul M] → Set M
Set.center M: Type ?u.6827
Mˣ :=
  fun _: ?m.8083
_ ha: ?m.8086
ha _: ?m.8089
_ => Units.ext: ∀ {α : Type ?u.8091} [inst : Monoid α], Function.Injective Units.val
Units.ext <| ha: ?m.8086
ha _: M
_
#align set.subset_center_units Set.subset_center_units: ∀ {M : Type u_1} [inst : Monoid M], Units.val ⁻¹' center M ⊆ center Mˣ
Set.subset_center_units
#align set.subset_add_center_add_units Set.subset_addCenter_add_units: ∀ {M : Type u_1} [inst : AddMonoid M], AddUnits.val ⁻¹' addCenter M ⊆ addCenter (AddUnits M)
Set.subset_addCenter_add_units

theorem center_units_subset: ∀ [inst : GroupWithZero M], center Mˣ ⊆ Units.val ⁻¹' center M
center_units_subset [GroupWithZero: Type ?u.8163 → Type ?u.8163
GroupWithZero M: Type ?u.8160
M] : Set.center: (M : Type ?u.8174) → [inst : Mul M] → Set M
Set.center M: Type ?u.8160
Mˣ ⊆ ((↑): Mˣ → M
(↑) : M: Type ?u.8160
Mˣ → M: Type ?u.8160
M) ⁻¹' center: (M : Type ?u.9280) → [inst : Mul M] → Set M
center M: Type ?u.8160
M :=
  fun a: ?m.9397
a ha: ?m.9400
ha b: ?m.9403
b => by
Goals accomplished! 🐙
  M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

b * ↑a = ↑a * bobtain rfl: b = 0
rflrfl | hb: b = 0 ∨ b ≠ 0
 | hb: b ≠ 0
hb := eq_or_ne: ∀ {α : Sort ?u.9413} (x y : α), x = y ∨ x ≠ y
eq_or_ne b: M
b 0: ?m.9416
0M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 * ↑a = ↑a * 0
M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

hb: b ≠ 0

inrb * ↑a = ↑a * b
  M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

b * ↑a = ↑a * b·M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 * ↑a = ↑a * 0 M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 * ↑a = ↑a * 0
M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

hb: b ≠ 0

inrb * ↑a = ↑a * brw [M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 * ↑a = ↑a * 0zero_mul: ∀ {M₀ : Type ?u.9537} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul,M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 = ↑a * 0 M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 * ↑a = ↑a * 0mul_zero: ∀ {M₀ : Type ?u.9688} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zeroM: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

inl0 = 0]
Goals accomplished! 🐙
  M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

b * ↑a = ↑a * b·M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

hb: b ≠ 0

inrb * ↑a = ↑a * b M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: a ∈ center Mˣ

b: M

hb: b ≠ 0

inrb * ↑a = ↑a * bexact Units.ext_iff: ∀ {α : Type ?u.9725} [inst : Monoid α] {a b : αˣ}, a = b ↔ ↑a = ↑b
Units.ext_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (ha: a ∈ center Mˣ
ha (Units.mk0: {G₀ : Type ?u.9755} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣ
Units.mk0 _: ?m.9756
_ hb: b ≠ 0
hb))
Goals accomplished! 🐙
#align set.center_units_subset Set.center_units_subset: ∀ {M : Type u_1} [inst : GroupWithZero M], center Mˣ ⊆ Units.val ⁻¹' center M
Set.center_units_subset

/-- In a group with zero, the center of the units is the preimage of the center. -/
theorem center_units_eq: ∀ [inst : GroupWithZero M], center Mˣ = Units.val ⁻¹' center M
center_units_eq [GroupWithZero: Type ?u.9830 → Type ?u.9830
GroupWithZero M: Type ?u.9827
M] : Set.center: (M : Type ?u.9834) → [inst : Mul M] → Set M
Set.center M: Type ?u.9827
Mˣ = ((↑): Mˣ → M
(↑) : M: Type ?u.9827
Mˣ → M: Type ?u.9827
M) ⁻¹' center: (M : Type ?u.10938) → [inst : Mul M] → Set M
center M: Type ?u.9827
M :=
  Subset.antisymm: ∀ {α : Type ?u.11049} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Subset.antisymm center_units_subset: ∀ {M : Type ?u.11057} [inst : GroupWithZero M], center Mˣ ⊆ Units.val ⁻¹' center M
center_units_subset subset_center_units: ∀ {M : Type ?u.11085} [inst : Monoid M], Units.val ⁻¹' center M ⊆ center Mˣ
subset_center_units
#align set.center_units_eq Set.center_units_eq: ∀ {M : Type u_1} [inst : GroupWithZero M], center Mˣ = Units.val ⁻¹' center M
Set.center_units_eq

@[simp]
theorem inv_mem_center₀: ∀ {M : Type u_1} [inst : GroupWithZero M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
inv_mem_center₀ [GroupWithZero: Type ?u.11163 → Type ?u.11163
GroupWithZero M: Type ?u.11160
M] {a: M
a : M: Type ?u.11160
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.11185) → [inst : Mul M] → Set M
Set.center M: Type ?u.11160
M) : a: M
a⁻¹ ∈ Set.center: (M : Type ?u.11396) → [inst : Mul M] → Set M
Set.center M: Type ?u.11160
M := by
Goals accomplished! 🐙
  M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

a⁻¹ ∈ center Mobtain rfl: a = 0
rflrfl | ha0: a = 0 ∨ a ≠ 0
 | ha0: a ≠ 0
ha0 := eq_or_ne: ∀ {α : Sort ?u.11408} (x y : α), x = y ∨ x ≠ y
eq_or_ne a: M
a 0: ?m.11411
0M: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0⁻¹ ∈ center M
M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

ha0: a ≠ 0

inra⁻¹ ∈ center M
  M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

a⁻¹ ∈ center M·M: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0⁻¹ ∈ center M M: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0⁻¹ ∈ center M
M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

ha0: a ≠ 0

inra⁻¹ ∈ center Mrw [M: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0⁻¹ ∈ center Minv_zero: ∀ {G₀ : Type ?u.11536} [self : GroupWithZero G₀], 0⁻¹ = 0
inv_zeroM: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0 ∈ center M]M: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0 ∈ center M
    M: Type u_1

inst✝: GroupWithZero M

ha: 0 ∈ center M

inl0⁻¹ ∈ center Mexact zero_mem_center: ∀ (M : Type ?u.11567) [inst : MulZeroClass M], 0 ∈ center M
zero_mem_center M: Type u_1
M
Goals accomplished! 🐙
  M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

a⁻¹ ∈ center Mrcases IsUnit.mk0: ∀ {G₀ : Type ?u.11680} [inst : GroupWithZero G₀] (x : G₀), x ≠ 0 → IsUnit x
IsUnit.mk0 _: ?m.11681
_ ha0: a ≠ 0
ha0 with ⟨a, rfl⟩: IsUnit a
⟨a: Mˣ
a⟨a, rfl⟩: IsUnit a
, rfl: ↑a = a✝
rfl⟨a, rfl⟩: IsUnit a
⟩M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: ↑a ∈ center M

ha0: ↑a ≠ 0

inr.intro(↑a)⁻¹ ∈ center M
  M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

a⁻¹ ∈ center Mrw [M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: ↑a ∈ center M

ha0: ↑a ≠ 0

inr.intro(↑a)⁻¹ ∈ center M← Units.val_inv_eq_inv_val: ∀ {M : Type ?u.11737} [inst : DivisionMonoid M] (u : Mˣ), ↑u⁻¹ = (↑u)⁻¹
Units.val_inv_eq_inv_valM: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: ↑a ∈ center M

ha0: ↑a ≠ 0

inr.intro↑a⁻¹ ∈ center M]M: Type u_1

inst✝: GroupWithZero M

a: Mˣ

ha: ↑a ∈ center M

ha0: ↑a ≠ 0

inr.intro↑a⁻¹ ∈ center M
  M: Type u_1

inst✝: GroupWithZero M

a: M

ha: a ∈ center M

a⁻¹ ∈ center Mexact center_units_subset: ∀ {M : Type ?u.11807} [inst : GroupWithZero M], center Mˣ ⊆ Units.val ⁻¹' center M
center_units_subset (inv_mem_center: ∀ {M : Type ?u.11850} [inst : Group M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
inv_mem_center (subset_center_units: ∀ {M : Type ?u.11890} [inst : Monoid M], Units.val ⁻¹' center M ⊆ center Mˣ
subset_center_units ha: ↑a ∈ center M
ha))
Goals accomplished! 🐙
#align set.inv_mem_center₀ Set.inv_mem_center₀: ∀ {M : Type u_1} [inst : GroupWithZero M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
Set.inv_mem_center₀

@[to_additive (attr := simp) sub_mem_addCenter: ∀ {M : Type u_1} [inst : AddGroup M] {a b : M}, a ∈ addCenter M → b ∈ addCenter M → a - b ∈ addCenter M
sub_mem_addCenter]
theorem div_mem_center: ∀ {M : Type u_1} [inst : Group M] {a b : M}, a ∈ center M → b ∈ center M → a / b ∈ center M
div_mem_center [Group: Type ?u.12015 → Type ?u.12015
Group M: Type ?u.12012
M] {a: M
a b: M
b : M: Type ?u.12012
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.12039) → [inst : Mul M] → Set M
Set.center M: Type ?u.12012
M) (hb: b ∈ center M
hb : b: M
b ∈ Set.center: (M : Type ?u.12285) → [inst : Mul M] → Set M
Set.center M: Type ?u.12012
M) :
    a: M
a / b: M
b ∈ Set.center: (M : Type ?u.12383) → [inst : Mul M] → Set M
Set.center M: Type ?u.12012
M := by
Goals accomplished! 🐙
  M: Type u_1

inst✝: Group M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a / b ∈ center Mrw [M: Type u_1

inst✝: Group M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a / b ∈ center Mdiv_eq_mul_inv: ∀ {G : Type ?u.12399} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_invM: Type u_1

inst✝: Group M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a * b⁻¹ ∈ center M]M: Type u_1

inst✝: Group M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a * b⁻¹ ∈ center M
  M: Type u_1

inst✝: Group M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a / b ∈ center Mexact mul_mem_center: ∀ {M : Type ?u.12472} [inst : Semigroup M] {a b : M}, a ∈ center M → b ∈ center M → a * b ∈ center M
mul_mem_center ha: a ∈ center M
ha (inv_mem_center: ∀ {M : Type ?u.12654} [inst : Group M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
inv_mem_center hb: b ∈ center M
hb)
Goals accomplished! 🐙
#align set.div_mem_center Set.div_mem_center: ∀ {M : Type u_1} [inst : Group M] {a b : M}, a ∈ center M → b ∈ center M → a / b ∈ center M
Set.div_mem_center
#align set.sub_mem_add_center Set.sub_mem_addCenter: ∀ {M : Type u_1} [inst : AddGroup M] {a b : M}, a ∈ addCenter M → b ∈ addCenter M → a - b ∈ addCenter M
Set.sub_mem_addCenter

@[simp]
theorem div_mem_center₀: ∀ {M : Type u_1} [inst : GroupWithZero M] {a b : M}, a ∈ center M → b ∈ center M → a / b ∈ center M
div_mem_center₀ [GroupWithZero: Type ?u.12799 → Type ?u.12799
GroupWithZero M: Type ?u.12796
M] {a: M
a b: M
b : M: Type ?u.12796
M} (ha: a ∈ center M
ha : a: M
a ∈ Set.center: (M : Type ?u.12823) → [inst : Mul M] → Set M
Set.center M: Type ?u.12796
M)
    (hb: b ∈ center M
hb : b: M
b ∈ Set.center: (M : Type ?u.12995) → [inst : Mul M] → Set M
Set.center M: Type ?u.12796
M) : a: M
a / b: M
b ∈ Set.center: (M : Type ?u.13067) → [inst : Mul M] → Set M
Set.center M: Type ?u.12796
M := by
Goals accomplished! 🐙
  M: Type u_1

inst✝: GroupWithZero M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a / b ∈ center Mrw [M: Type u_1

inst✝: GroupWithZero M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a / b ∈ center Mdiv_eq_mul_inv: ∀ {G : Type ?u.13083} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_invM: Type u_1

inst✝: GroupWithZero M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a * b⁻¹ ∈ center M]M: Type u_1

inst✝: GroupWithZero M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a * b⁻¹ ∈ center M
  M: Type u_1

inst✝: GroupWithZero M

a, b: M

ha: a ∈ center M

hb: b ∈ center M

a / b ∈ center Mexact mul_mem_center: ∀ {M : Type ?u.13149} [inst : Semigroup M] {a b : M}, a ∈ center M → b ∈ center M → a * b ∈ center M
mul_mem_center ha: a ∈ center M
ha (inv_mem_center₀: ∀ {M : Type ?u.13278} [inst : GroupWithZero M] {a : M}, a ∈ center M → a⁻¹ ∈ center M
inv_mem_center₀ hb: b ∈ center M
hb)
Goals accomplished! 🐙
#align set.div_mem_center₀ Set.div_mem_center₀: ∀ {M : Type u_1} [inst : GroupWithZero M] {a b : M}, a ∈ center M → b ∈ center M → a / b ∈ center M
Set.div_mem_center₀

variable (M: ?m.13346
M)

@[to_additive (attr := simp) addCenter_eq_univ: ∀ (M : Type u_1) [inst : AddCommSemigroup M], addCenter M = univ
addCenter_eq_univ]
theorem center_eq_univ: ∀ (M : Type u_1) [inst : CommSemigroup M], center M = univ
center_eq_univ [CommSemigroup: Type ?u.13352 → Type ?u.13352
CommSemigroup M: Type ?u.13349
M] : center: (M : Type ?u.13356) → [inst : Mul M] → Set M
center M: Type ?u.13349
M = Set.univ: {α : Type ?u.13687} → Set α
Set.univ :=
  (Subset.antisymm: ∀ {α : Type ?u.13722} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Subset.antisymm (subset_univ: ∀ {α : Type ?u.13726} (s : Set α), s ⊆ univ
subset_univ _: Set ?m.13727
_)) fun x: ?m.13747
x _: ?m.13750
_ y: ?m.13753
y => mul_comm: ∀ {G : Type ?u.13755} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm y: ?m.13753
y x: ?m.13747
x
#align set.center_eq_univ Set.center_eq_univ: ∀ (M : Type u_1) [inst : CommSemigroup M], center M = univ
Set.center_eq_univ
#align set.add_center_eq_univ Set.addCenter_eq_univ: ∀ (M : Type u_1) [inst : AddCommSemigroup M], addCenter M = univ
Set.addCenter_eq_univ

end Set

namespace Subsemigroup

section

variable (M: ?m.13800
M) [Semigroup: Type ?u.14284 → Type ?u.14284
Semigroup M: Type ?u.14272
M]

/-- The center of a semigroup `M` is the set of elements that commute with everything in `M` -/
@[to_additive: (M : Type u_1) → [inst : AddSemigroup M] → AddSubsemigroup M
to_additive
      "The center of a semigroup `M` is the set of elements that commute with everything in `M`"]
def center: (M : Type u_1) → [inst : Semigroup M] → Subsemigroup M
center : Subsemigroup: (M : Type ?u.13812) → [inst : Mul M] → Type ?u.13812
Subsemigroup M: Type ?u.13806
M where
  carrier := Set.center: (M : Type ?u.14123) → [inst : Mul M] → Set M
Set.center M: Type ?u.13806
M
  mul_mem':= Set.mul_mem_center: ∀ {M : Type ?u.14129} [inst : Semigroup M] {a b : M}, a ∈ Set.center M → b ∈ Set.center M → a * b ∈ Set.center M
Set.mul_mem_center
#align subsemigroup.center Subsemigroup.center: (M : Type u_1) → [inst : Semigroup M] → Subsemigroup M
Subsemigroup.center
#align add_subsemigroup.center AddSubsemigroup.center: (M : Type u_1) → [inst : AddSemigroup M] → AddSubsemigroup M
AddSubsemigroup.center

-- porting note: `coe_center` is now redundant
#noalign subsemigroup.coe_center
#noalign add_subsemigroup.coe_center

variable {M: ?m.14278
M}

@[to_additive: ∀ {M : Type u_1} [inst : AddSemigroup M] {z : M}, z ∈ AddSubsemigroup.center M ↔ ∀ (g : M), g + z = z + g
to_additive]
theorem mem_center_iff: ∀ {M : Type u_1} [inst : Semigroup M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff {z: M
z : M: Type ?u.14281
M} : z: M
z ∈ center: (M : Type ?u.14294) → [inst : Semigroup M] → Subsemigroup M
center M: Type ?u.14281
M ↔ ∀ g: ?m.14329
g, g: ?m.14329
g * z: M
z = z: M
z * g: ?m.14329
g :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align subsemigroup.mem_center_iff Subsemigroup.mem_center_iff: ∀ {M : Type u_1} [inst : Semigroup M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
Subsemigroup.mem_center_iff
#align add_subsemigroup.mem_center_iff AddSubsemigroup.mem_center_iff: ∀ {M : Type u_1} [inst : AddSemigroup M] {z : M}, z ∈ AddSubsemigroup.center M ↔ ∀ (g : M), g + z = z + g
AddSubsemigroup.mem_center_iff

@[to_additive: {M : Type u_1} →
  [inst : AddSemigroup M] →
    (a : M) → [inst_1 : Decidable (∀ (b : M), b + a = a + b)] → Decidable (a ∈ AddSubsemigroup.center M)
to_additive]
instance decidableMemCenter: {M : Type u_1} →
  [inst : Semigroup M] → (a : M) → [inst_1 : Decidable (∀ (b : M), b * a = a * b)] → Decidable (a ∈ center M)
decidableMemCenter (a: M
a) [Decidable: Prop → Type
Decidable <| ∀ b: M
b : M: Type ?u.15176
M, b: M
b * a: ?m.15182
a = a: ?m.15182
a * b: M
b] : Decidable: Prop → Type
Decidable (a: ?m.15182
a ∈ center: (M : Type ?u.16019) → [inst : Semigroup M] → Subsemigroup M
center M: Type ?u.15176
M) :=
  decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' _: Prop
_ mem_center_iff: ∀ {M : Type ?u.16055} [inst : Semigroup M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff
#align subsemigroup.decidable_mem_center Subsemigroup.decidableMemCenter: {M : Type u_1} →
  [inst : Semigroup M] → (a : M) → [inst_1 : Decidable (∀ (b : M), b * a = a * b)] → Decidable (a ∈ center M)
Subsemigroup.decidableMemCenter
#align add_subsemigroup.decidable_mem_center AddSubsemigroup.decidableMemCenter: {M : Type u_1} →
  [inst : AddSemigroup M] →
    (a : M) → [inst_1 : Decidable (∀ (b : M), b + a = a + b)] → Decidable (a ∈ AddSubsemigroup.center M)
AddSubsemigroup.decidableMemCenter

/-- The center of a semigroup is commutative. -/
@[to_additive: {M : Type u_1} → [inst : AddSemigroup M] → AddCommSemigroup { x // x ∈ AddSubsemigroup.center M }
to_additive "The center of an additive semigroup is commutative."]
instance center.commSemigroup: {M : Type u_1} → [inst : Semigroup M] → CommSemigroup { x // x ∈ center M }
center.commSemigroup : CommSemigroup: Type ?u.16261 → Type ?u.16261
CommSemigroup (center: (M : Type ?u.16262) → [inst : Semigroup M] → Subsemigroup M
center M: Type ?u.16255
M) :=
  { MulMemClass.toSemigroup: {M : Type ?u.16418} →
  [inst : Semigroup M] →
    {A : Type ?u.16417} → [inst_1 : SetLike A M] → [inst : MulMemClass A M] → (S : A) → Semigroup { x // x ∈ S }
MulMemClass.toSemigroup (center: (M : Type ?u.16424) → [inst : Semigroup M] → Subsemigroup M
center M: Type ?u.16255
M) with mul_comm := fun _: ?m.16490
_ b: ?m.16493
b => Subtype.ext: ∀ {α : Sort ?u.16495} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext <| b: ?m.16493
b.2: ∀ {α : Sort ?u.16506} {p : α → Prop} (self : Subtype p), p ↑self
2 _: M
_ }
#align subsemigroup.center.comm_semigroup Subsemigroup.center.commSemigroup: {M : Type u_1} → [inst : Semigroup M] → CommSemigroup { x // x ∈ center M }
Subsemigroup.center.commSemigroup
#align add_subsemigroup.center.add_comm_semigroup AddSubsemigroup.center.addCommSemigroup: {M : Type u_1} → [inst : AddSemigroup M] → AddCommSemigroup { x // x ∈ AddSubsemigroup.center M }
AddSubsemigroup.center.addCommSemigroup

end

section

variable (M: ?m.16683
M) [CommSemigroup: Type ?u.16692 → Type ?u.16692
CommSemigroup M: ?m.16683
M]

@[to_additive: ∀ (M : Type u_1) [inst : AddCommSemigroup M], AddSubsemigroup.center M = ⊤
to_additive (attr := simp)]
theorem center_eq_top: ∀ (M : Type u_1) [inst : CommSemigroup M], center M = ⊤
center_eq_top : center: (M : Type ?u.16696) → [inst : Semigroup M] → Subsemigroup M
center M: Type ?u.16689
M = ⊤: ?m.16943
⊤ :=
  SetLike.coe_injective: ∀ {A : Type ?u.16992} {B : Type ?u.16993} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective (Set.center_eq_univ: ∀ (M : Type ?u.17010) [inst : CommSemigroup M], Set.center M = Set.univ
Set.center_eq_univ M: Type ?u.16689
M)
#align subsemigroup.center_eq_top Subsemigroup.center_eq_top: ∀ (M : Type u_1) [inst : CommSemigroup M], center M = ⊤
Subsemigroup.center_eq_top
#align add_subsemigroup.center_eq_top AddSubsemigroup.center_eq_top: ∀ (M : Type u_1) [inst : AddCommSemigroup M], AddSubsemigroup.center M = ⊤
AddSubsemigroup.center_eq_top

end

end Subsemigroup

-- Guard against import creep
assert_not_exists Finset