refine'
  Set.Subset.antisymm _
    (convexHull_min (subset_closure_combiInterior hs) (convex_combiInterior hs).closure)
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) = (convexHull ℝ) ↑s
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑s