theorem int_tendsto_nat {f : ℤ → ℂ} {x : ℂ} (hf : Filter.Tendsto f Filter.atTop (nhds x)) : Filter.Tendsto (fun (n : ℕ) => f ↑n) Filter.atTop (nhds x)

theorem pnat_tendsto_nat (f : ℕ → ℂ) (x : ℂ) (hf : Filter.Tendsto (fun (n : ℕ+) => f ↑n) Filter.atTop (nhds x)) : Filter.Tendsto f Filter.atTop (nhds x)

theorem nat_tendsto_pnat (f : ℕ → ℂ) (x : ℂ) (hf : Filter.Tendsto f Filter.atTop (nhds x)) : Filter.Tendsto (fun (n : ℕ+) => f ↑n) Filter.atTop (nhds x)

theorem rest (f g : ℕ → ℂ) (x : ℂ) (hf : Filter.Tendsto f Filter.atTop (nhds x)) (hfg : Filter.Tendsto (g - f) Filter.atTop (nhds 0)) : Filter.Tendsto g Filter.atTop (nhds x)

theorem aux47 (r : ℂ) (hr : ‖r‖ < 1) : Filter.Tendsto (fun (n : ℕ) => 1 - r ^ n) Filter.atTop (nhds 1)