𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (x : H), x ∈ innerDualCone univ → x = 0
𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ innerDualCone univ = 0
suffices ∀ x : H, x ∈ (univ : Set H).innerDualCone → x = 0 by
  apply SetLike.coe_injective
  exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
no goals
𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (x : H), x ∈ innerDualCone univ → x = 0
exact fun x hx => by simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)
case a
𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ ↑(innerDualCone univ) = ↑0
𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ innerDualCone univ = 0
apply SetLike.coe_injective
no goals
case a
𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ ↑(innerDualCone univ) = ↑0
exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
no goals
𝕜 : Type ?u.5561
E : Type ?u.5564
F : Type ?u.5567
G : Type ?u.5570
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : H
hx : x ∈ innerDualCone univ
⊢ x = 0
simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)