no goals
R : Type u_1
A : Type ?u.21732
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]