no goals
α : Type u_1
β : Type ?u.333397
ι : Type ?u.333400
G : Type ?u.333403
M : Type u_2
N : Type ?u.333409
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hst : Disjoint s t
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
  mul_one]