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
⊢ ↑(↑(selfAdjointPart R) x) + ↑(↑(skewAdjointPart R) x) = x
simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe,
  add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul]