no goals
F : Type ?u.378119
R : Type ?u.378122
A : Type u_1
B : Type ?u.378128
C : Type ?u.378131
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S : StarSubalgebra R A
a : A
s : Set A
h : ∀ (a : A), a ∈ s → star a ∈ s
ha : a ∈ Set.centralizer s
y : A
hy : y ∈ s
⊢ y * star a = star a * y
simpa using congr_arg star (ha _ (h _ hy)).symm