no goals
α : Type u_2
β : Type ?u.215706
ι : Type ?u.215709
G : Type u_1
M : Type ?u.215715
N : Type ?u.215718
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hf : Set.Finite (mulSupport f)
hg : Set.Finite (mulSupport g)
⊢ (∏ᶠ (i : α), f i / g i) = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i
simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_inv g).symm.rec hg),
  finprod_inv_distrib]