no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∏ x in range (n + 1), (x + 1) = (n + 1)!
simp [Finset.range_succ, prod_range_add_one_eq_factorial n]