no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.979345
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
u : { x // x ∈ K }
v : E
⊢ inner u (↑(orthogonalProjection K) v) = inner (↑u) v
rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]