no goals
𝕜 : Type u_3
E✝ : Type ?u.715379
F : Type ?u.715382
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'
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E'
⊢ ↑(reflection (Submodule.map (↑f.toLinearEquiv) K)) x = ↑f (↑(reflection K) (↑(LinearIsometryEquiv.symm f) x))
simp [two_smul, reflection_apply, orthogonalProjection_map_apply f K x]