no goals
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n : ℕ
⊢ prod (map f (range (succ n))) = prod (map f (range n)) * f n
rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]