no goals
ι : Type ?u.431878
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ x in range (n + 1), f x = f n * ∏ x in range n, f x
rw [range_succ, prod_insert not_mem_range_self]