no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.841108
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace ℝ F
K U V : Submodule 𝕜 E
inst✝¹ : CompleteSpace { x // x ∈ U }
inst✝ : CompleteSpace { x // x ∈ V }
h : U ≤ V
x : E
⊢ ↑(orthogonalProjection U) x = ↑(orthogonalProjection U) ↑(↑(orthogonalProjection V) x)
simpa only [sub_eq_zero, map_sub] using
  orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
    (Submodule.orthogonal_le h (sub_orthogonalProjection_mem_orthogonal x))