no goals
α : Type u_2
β : Type u_1
γ : Type ?u.11639
δ : Type ?u.11642
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s : Multiset β
f : β → α
h : p ∣ Multiset.prod (Multiset.map f s)
⊢ ∃ a, a ∈ s ∧ p ∣ f a
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
  hp.exists_mem_multiset_dvd h