convert
  (inter_frontier_self_inter_convexHull_extreme :
    IsExtreme 𝕜 (closure s) (closure s ∩ frontier (convexHull 𝕜 s))) using 1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ IsExtreme 𝕜 s (frontier s)
case h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ s = closure s

case h.e'_7
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ frontier s = closure s ∩ frontier ((convexHull 𝕜) s)