no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162171
G : Type ?u.162174
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y, y ∈ s ∧ c • y = x
simp only [toCone, ConvexCone.mem_mk, mem_iUnion, mem_smul_set, eq_comm, exists_prop]