no goals
𝕜 : Type ?u.9011
E : Type ?u.9014
F : Type ?u.9017
G : Type ?u.9020
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : H
x✝ : x ∈ s
⊢ 0 ≤ inner x 0
rw [inner_zero_right]