no goals
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a✝ b : α
s : Set α
inst✝ : NoMaxOrder α
a : α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ ∃ b, b > a ∧ p b
simpa only [exists_prop, gt_iff_lt, and_comm] using
  ((h.filter_mono (@nhdsWithin_le_nhds _ _ a (Ioi a))).and self_mem_nhdsWithin).exists