no goals
α : Type u_1
β : Type u_2
s✝ t : Finset α
f✝ : α → β
n : ℕ
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ card (filter (fun x => f x = y) s) ≠ 0 ↔ y ∈ image f s
rw [← pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]