rintro x hx
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
⊢ s ⊆ t
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
⊢ x ∈ t