no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∏ x in Ico 1 (n + 1 + 1), x = (n + 1)!
rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ,
  prod_Ico_id_eq_factorial n, Nat.succ_eq_add_one, mul_comm]