exact ⟨_, Zt.trans st.1, hZ⟩
case pos.intro.intro.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✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
Z : Finset E
Zt : Z ⊆ t
hZ : x ∈ combiInterior 𝕜 Z
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
no goals