no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝¹ : CommMonoid β
δ : Type u_1
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ ∏ k in Ico m n, f k = (∏ k in range n, f k) / ∏ k in range m, f k
simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h