[GOAL]
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
a : R
s : Set R
ha : a ∈ center R
⊢ star a ∈ center R
[PROOFSTEP]
simpa only [star_mul, star_star] using fun g => congr_arg star ((Set.mem_center_iff R).mp ha <| star g).symm
[GOAL]
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
a : R
s : Set R
h : ∀ (a : R), a ∈ s → star a ∈ s
ha : a ∈ centralizer s
y : R
hy : y ∈ s
⊢ y * star a = star a * y
[PROOFSTEP]
simpa using congr_arg star (ha _ (h _ hy)).symm
