no goals
α : Type u_1
β : Type ?u.362387
ι : Type ?u.362390
G : Type ?u.362393
M : Type u_2
N : Type ?u.362399
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hst : s ⊆ t
ht : Set.Finite (t ∩ mulSupport f)
⊢ ((∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i
rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]