simp at hys
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑∅
⊢ y ∈ ∅
no goals