use z
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
z : ℕ → E := fun n => (1 + 1 / ↑n.succ) • x - (1 / ↑n.succ) • y
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ sᶜ) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
z : ℕ → E := fun n => (1 + 1 / ↑n.succ) • x - (1 / ↑n.succ) • y
⊢ (∀ (n : ℕ), z n ∈ sᶜ) ∧ Filter.Tendsto z Filter.atTop (nhds x)