exact ⟨codRestrict (s.restrict f) t (fun x ↦ by aesop), hf.injective.codRestrict _⟩
case inr.intro.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
⊢ Nonempty (↑s ↪ ↑t)
no goals