no goals
α : Type u_1
β : Type ?u.39319
γ : Type ?u.39322
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
m : α → ℝ≥0∞
f : Filter α
⊢ Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]