no goals
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
rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]