no goals
α : Type u_1
β : Type u_2
γ : Type ?u.71261
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a : α
b c : β
f : α → β
s : Finset α
y : β
⊢ Finset.Nonempty (filter (fun x => f x = y) s) ↔ y ∈ image f s
simp [Finset.Nonempty]