rintro ⟨hxA, hxfA⟩
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
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
case mpr.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
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t