no goals
α : Type u_1
β : Type ?u.206039
ι : Type ?u.206042
G : Type ?u.206045
M : Type u_2
N : Type ?u.206051
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i
rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]