no goals
α : Type u_1
β : Type ?u.201320
ι : Type ?u.201323
G : Type ?u.201326
M : Type u_2
N : Type ?u.201332
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
s : Set α
inst✝ : Fintype ↑s
⊢ (s ∩ mulSupport fun i => f i) = ↑(toFinset s) ∩ mulSupport fun i => f i
simp_rw [coe_toFinset s]