case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.512356
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : { x // x ∈ K }
⊢ ↑(↑(orthogonalProjection K) ↑v) = ↑v
𝕜 : Type u_2
E : Type u_1
F : Type ?u.512356
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : { x // x ∈ K }
⊢ ↑(orthogonalProjection K) ↑v = v
ext
no goals
case a
𝕜 : Type u_2
E : Type u_1
F : Type ?u.512356
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : { x // x ∈ K }
⊢ ↑(↑(orthogonalProjection K) ↑v) = ↑v
apply eq_orthogonalProjection_of_mem_of_inner_eq_zero <;> simp