[GOAL]
M : Type u_1
S T : Set M
inst✝ : MulOneClass M
⊢ 1 ∈ centralizer S
[PROOFSTEP]
simp [mem_centralizer_iff]
[GOAL]
M : Type u_1
S T : Set M
inst✝ : MulZeroClass M
⊢ 0 ∈ centralizer S
[PROOFSTEP]
simp [mem_centralizer_iff]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Semigroup M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
g : M
hg : g ∈ S
⊢ g * (a * b) = a * b * g
[PROOFSTEP]
rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Group M
ha : a ∈ centralizer S
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g
[PROOFSTEP]
rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
c : M
hc : c ∈ S
⊢ c * (a + b) = (a + b) * c
[PROOFSTEP]
rw [add_mul, mul_add, ha c hc, hb c hc]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ centralizer S
c : M
hc : c ∈ S
⊢ c * -a = -a * c
[PROOFSTEP]
rw [mul_neg, ha c hc, neg_mul]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ a⁻¹ ∈ centralizer S
[PROOFSTEP]
rw [h, inv_zero]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ 0 ∈ centralizer S
[PROOFSTEP]
exact zero_mem_centralizer S
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
ha0 : a ≠ 0
c : M
hc : c ∈ S
⊢ c * a⁻¹ = a⁻¹ * c
[PROOFSTEP]
rw [mul_inv_eq_iff_eq_mul₀ ha0, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha0, ha c hc]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Group M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a / b ∈ centralizer S
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Group M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a * b⁻¹ ∈ centralizer S
[PROOFSTEP]
exact mul_mem_centralizer ha (inv_mem_centralizer hb)
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a / b ∈ centralizer S
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a * b⁻¹ ∈ centralizer S
[PROOFSTEP]
exact mul_mem_centralizer ha (inv_mem_centralizer₀ hb)
