exact subset_iUnion₂ s Subset.rfl ⟨hx, h⟩
case neg
𝕜 : 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
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∉ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
no goals