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✝ : { x // x ∈ skewAdjoint.submodule R A }
x : A
hx : star x = -x
⊢ ↑(↑(LinearMap.comp (selfAdjointPart R) (Submodule.subtype (skewAdjoint.submodule R A)))
        { val := x, property := hx }) =
    ↑(↑0 { val := x, property := hx })
simp [hx]