no goals
α : Type u_1
β : Type ?u.201940
ι : Type ?u.201943
G : Type ?u.201946
M : Type u_2
N : Type ?u.201952
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
hs : Set.Finite s
⊢ (s ∩ mulSupport fun i => f i) = ↑(Finite.toFinset hs) ∩ mulSupport fun i => f i
rw [hs.coe_toFinset]