rw [Finset.sum_Ico_eq_sub]
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ ∑ i ∈ Finset.range M, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N M, f n
case h.h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ N ≤ M