case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.968584
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w : E
⊢ ↑(ContinuousLinearMap.id 𝕜 E) w =
    ↑(ContinuousLinearMap.comp (Submodule.subtypeL K) (orthogonalProjection K) +
          ContinuousLinearMap.comp (Submodule.subtypeL Kᗮ) (orthogonalProjection Kᗮ))
      w
𝕜 : Type u_2
E : Type u_1
F : Type ?u.968584
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
⊢ ContinuousLinearMap.id 𝕜 E =
    ContinuousLinearMap.comp (Submodule.subtypeL K) (orthogonalProjection K) +
      ContinuousLinearMap.comp (Submodule.subtypeL Kᗮ) (orthogonalProjection Kᗮ)
ext w
no goals
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.968584
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace { x // x ∈ K }
w : E
⊢ ↑(ContinuousLinearMap.id 𝕜 E) w =
    ↑(ContinuousLinearMap.comp (Submodule.subtypeL K) (orthogonalProjection K) +
          ContinuousLinearMap.comp (Submodule.subtypeL Kᗮ) (orthogonalProjection Kᗮ))
      w
exact eq_sum_orthogonalProjection_self_orthogonalComplement K w