no goals
α : Type u_1
β : Type u_2
γ : Type ?u.45893
ι : Sort ?u.45896
ι' : Sort ?u.45899
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Injective f
⊢ Disjoint (f '' s) (f '' sᶜ)
simp [disjoint_iff_inf_le, ←image_inter H]