no goals
α : Type u_1
β : Type ?u.74500
γ : Type ?u.74503
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto u f (𝓝 a) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal]