simp only [Set.subset_inter_iff, Set.image_subset_iff, Set.subset_def]
α β : Type
X Y : Set α
f : α → β
⊢ f '' (X ∩ Y) ⊆ f '' X ∩ f '' Y
α β : Type
X Y : Set α
f : α → β
⊢ ∀ x ∈ f '' (X ∩ Y), x ∈ f '' X ∩ f '' Y