exact (convex_convexHull 𝕜 _).convexIndependent_extremePoints
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
h : extremePoints 𝕜 ((convexHull 𝕜) s) = s
⊢ ConvexIndependent 𝕜 fun p => ↑p
no goals