case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.748584
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x✝ : E
⊢ ↑(reflection ⊥) x✝ = ↑(LinearIsometryEquiv.neg 𝕜) x✝
𝕜 : Type u_2
E : Type u_1
F : Type ?u.748584
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
⊢ reflection ⊥ = LinearIsometryEquiv.neg 𝕜
ext
no goals
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.748584
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x✝ : E
⊢ ↑(reflection ⊥) x✝ = ↑(LinearIsometryEquiv.neg 𝕜) x✝
simp [reflection_apply]