no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a ≤ b
f : ℕ → β
⊢ ∏ k in Ico a (b + 1), f k = (∏ k in Ico a b, f k) * f b
rw [Nat.Ico_succ_right_eq_insert_Ico hab, prod_insert right_not_mem_Ico, mul_comm]