no goals
α : Type u_1
β : Type u_2
γ : Type ?u.10594
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : Nontrivial α
⊢ lcm s f = 0 ↔ 0 ∈ f '' ↑s
simp only [Multiset.mem_map, lcm_def, Multiset.lcm_eq_zero_iff, Set.mem_image, mem_coe, ←
  Finset.mem_def]