no goals
α : Type u_1
β : Type u_2
γ : Type ?u.75968
inst✝¹ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
s : Multiset α
x✝ : β
⊢ x✝ ∈ image f (toFinset s) ↔ x✝ ∈ toFinset (Multiset.map f s)
simp only [mem_image, Multiset.mem_toFinset, exists_prop, Multiset.mem_map]