no goals
R : Type u_2
A : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : StarSemigroup R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑(↑(selfAdjointPart R) x) = x
rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]