no goals
α✝ : Type ?u.12287
inst✝ : TopologicalSpace α✝
α : Type u_1
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Ioi ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
simp only [true_implies, mem_Ioi]