no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.899657
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
x y : E
inst✝ : CompleteSpace E
hK : Dense ↑K
h : ∀ (v : { x // x ∈ K }), inner x ↑v = 0
v : { x // x ∈ K }
⊢ inner x ↑v = inner 0 ↑v
rw [inner_zero_left, h v]