no goals
ι : Type ?u.614536
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
M : Type u_1
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
nonempty : Finset.Nonempty s
base : ∀ (x : α), x ∈ s → p (f x)
⊢ Multiset.map (fun x => f x) s.val ≠ ∅
simp [nonempty_iff_ne_empty.mp nonempty]