refine'
  ⟨{x ∈ s | ∀ y ∈ s, l y ≤ l x}, fun _ => ⟨l, rfl⟩, fun h =>
    not_le.2 (hl y hyA) ((h (interior_subset hyA)).2 x hxA), hxA, fun z hzA => _⟩
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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
⊢ ∃ t, IsExposed ℝ 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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ l z ≤ l x