no goals
𝕜 : Type u_3
E✝ : Type ?u.545265
F : Type ?u.545268
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace 𝕜 E✝
inst✝⁶ : InnerProductSpace ℝ F
K : Submodule 𝕜 E✝
inst✝⁵ : CompleteSpace { x // x ∈ K }
E : Type u_1
E' : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ p }
x : E'
⊢ ↑(↑(orthogonalProjection (Submodule.map (↑f.toLinearEquiv) p)) x) =
    ↑f ↑(↑(orthogonalProjection p) (↑(LinearIsometryEquiv.symm f) x))
simpa only [f.coe_toLinearIsometry, f.apply_symm_apply] using
  (f.toLinearIsometry.map_orthogonalProjection p (f.symm x)).symm