no goals
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ t ∈ {t | ↑t ⊆ s ∧ x ∈ ↑(convexHull 𝕜).toOrderHom ↑t}
exact ⟨ht₁, ht₂⟩