no goals
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : OrderTopology α
inst✝² : OrderTopology β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)
simpa only [dual_Ioo]
  using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)