no goals
α : Type u_1
β : Type u_2
γ : Type ?u.120582
f : α → β
s✝ t✝ : Set α
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ Disjoint s t
rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
  image_empty]