no goals
α : Type u_2
β : Type ?u.322592
ι : Type ?u.322595
G : Type u_1
M : Type ?u.322601
N : Type ?u.322604
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hs : Set.Finite s
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i / g i) = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i
simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]