no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.973385
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 ↑(↑(orthogonalProjection K) v) ↑u =
    inner ↑(↑(orthogonalProjection K) v) ↑u + inner (v - ↑(↑(orthogonalProjection K) v)) ↑u
rw [orthogonalProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_zero]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.973385
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 ↑(↑(orthogonalProjection K) v) ↑u + inner (v - ↑(↑(orthogonalProjection K) v)) ↑u = inner v ↑u
rw [← inner_add_left, add_sub_cancel'_right]