no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1812323
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ∀ (v : E), inner v x = inner v y
⊢ x = y
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]