Inequality from eventually

Stream: Is there code for X?

[Vincent Beffara]

Is something like this in Mathlib? Presumably with a more elegant proof?

lemma le_of_eventually_nhdsWithin {a b : ℝ} (h : ∀ᶠ c in 𝓝[>] b, a ≤ c) : a ≤ b := by
  apply le_of_forall_lt' ; intro d hd
  have key : ∀ᶠ c in 𝓝[>] b, c < d := by
    apply eventually_of_mem (U := Iio d) ?_ (fun x hx => hx)
    rw [mem_nhdsWithin]
    refine ⟨Iio d, isOpen_Iio, hd, inter_subset_left _ _⟩
  obtain ⟨x, h1, h2⟩ := (h.and key).exists
  linarith

[Anatole Dedecker]

It’s probably not the easiest way, but in general all of those things can be obtained from docs#le_of_tendsto_of_tendsto