no goals
α : Type u_2
β : Type u_1
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
b : β
⊢ b ∈ pimage f s ↔ ∃ a, a ∈ s ∧ b ∈ f a
simp [pimage]