rintro _ ⟨w, hw, rfl⟩
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 '' interior s ⊆ Iio (l x)
case mpr.intro.intro.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
w : E
hw : w ∈ interior s
⊢ l w ∈ Iio (l x)