no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.878200
G : Type ?u.878203
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ↑adjoint (orthogonalProjection U) = Submodule.subtypeL U
rw [← U.adjoint_subtypeL, adjoint_adjoint]