no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15667
f : α ↪ β
s✝ : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
x✝ : β
⊢ x✝ ∈ map f (toFinset s) ↔ x✝ ∈ toFinset (Multiset.map (↑f) s)
simp only [mem_map, Multiset.mem_map, exists_prop, Multiset.mem_toFinset]