no goals
α : Type u_1
β : Type ?u.207591
ι : Type ?u.207594
G : Type ?u.207597
M : Type u_2
N : Type ?u.207603
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i
rw [← finprod_mem_inter_mulSupport, h, finprod_mem_inter_mulSupport]