obtain ⟨t, hst, hts, hxt⟩ := (mem_exposed_set_iff_mem_frontier hs₁ hs₂).2 h
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t✝ C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
t : Set E
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
hxt : x ∈ t
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t