rw [closure_convexHull_extremePoints hscomp hsconv, convexHull_extremePoints hscomp hsconv]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s B : Set E
hscomp : IsCompact s
hsconv : Convex ℝ s
⊢ closure ((convexHull ℝ) (extremePoints ℝ s)) = (convexHull ℝ) (extremePoints ℝ s)
no goals