no goals
ι : Type ?u.345463
ι' : Type ?u.345466
α : Type u_1
β : Type ?u.345472
γ : Type ?u.345475
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l
rw [← tendsto_map'_iff, map_add_atTop_eq_nat]