refine' extremePoints_convexHull_subset.antisymm fun x hxs => ⟨subset_convexHull 𝕜 _ hxs, _⟩
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ (convexHull 𝕜) s → ∀ ⦃x₂ : E⦄, x₂ ∈ (convexHull 𝕜) s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x