Theorem: push_sum (Ray/Misc/Finset.lean)

State before:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = (push N).sum (cons a f)
Tactic:
rw [push]
State after:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = (insert 0 (Finset.image (fun n => n + 1) N)).sum (cons a f)

State before:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = (insert 0 (Finset.image (fun n => n + 1) N)).sum (cons a f)
Tactic:
simp
State after:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = cons a f 0 + N.sum fun x => cons a f (x + 1)

State before:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = cons a f 0 + N.sum fun x => cons a f (x + 1)
Tactic:
rfl
State after:
no goals