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 : β
t : Finset β
⊢ pimage f s ⊆ t ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ f x → y ∈ t
simp [subset_iff, @forall_swap _ β]