no goals
α : Type u_1
β : Type ?u.180289
ι : Type ?u.180292
G : Type ?u.180295
M : Type u_2
N : Type ?u.180301
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ Finite.toFinset (_ : Set.Finite (mulSupport f)) ⊆ s
simpa [← Finset.coe_subset, Set.coe_toFinset]