no goals
α✝ : Type ?u.24919
β : Type ?u.24922
γ : Type ?u.24925
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
α : Type u_1
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ some) (𝓝 x) l
rw [nhds_coe, tendsto_map'_iff]