no goals
α : Type u_1
β : Type u_2
γ : Type ?u.52785
ι : Sort ?u.52788
ι' : Sort ?u.52791
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ Set.Nonempty (f '' s ∩ t) ↔ Set.Nonempty (s ∩ f ⁻¹' t)
rw [← image_inter_preimage, nonempty_image_iff]