no goals
ι : Type ?u.434314
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ k in range (n + 1 + 1), f k = (∏ k in range (n + 1), f (k + 1)) * f 0
rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]