no goals
α : Type u_2
β : Type u_1
γ : Type ?u.61453
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ b ∈ image f s ↔ ∃ a, a ∈ s ∧ f a = b
simp only [mem_def, image_val, mem_dedup, Multiset.mem_map, exists_prop]