Theorem: late_series_sum' (Ray/Misc/Bounds.lean)

State before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ ∃ M, N.sum f = M.sum fun n => f (n + m)
Tactic:
exists Finset.image (fun n ↦ n - m) N
State after:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ N.sum f = (Finset.image (fun n => n - m) N).sum fun n => f (n + m)

State before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ N.sum f = (Finset.image (fun n => n - m) N).sum fun n => f (n + m)
Tactic:
exact late_series_sum h f
State after:
no goals