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

State before:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = (push N).prod (cons a f)
Tactic:
rw [push]
State after:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = (insert 0 (Finset.image (fun n => n + 1) N)).prod (cons a f)

State before:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = (insert 0 (Finset.image (fun n => n + 1) N)).prod (cons a f)
Tactic:
simp
State after:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = cons a f 0 * N.prod fun x => cons a f (x + 1)

State before:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = cons a f 0 * N.prod fun x => cons a f (x + 1)
Tactic:
rfl
State after:
no goals