Theorem: tsum_eq_partial_add_tail (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
⊢ ∑' (n : ℕ), f n = ∑ n ∈ Finset.range N, f n + ∑' (n : ℕ), f (n + N)
Tactic:
rw [← sum_add_tsum_nat_add (f := f) (h := hf) (k := N)]
State after:
no goals