no goals
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
f g : α →. β
inst✝² : (x : α) → Decidable (f x).Dom
inst✝¹ : (x : α) → Decidable (g x).Dom
s t : Finset α
b : β
inst✝ : DecidableEq α
⊢ pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t
simp only [← coe_subset, coe_pimage, coe_inter, PFun.image_inter]