simp only [t.eq_empty_of_isEmpty, encard_empty, nonpos_iff_eq_zero, encard_eq_zero]
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ ↔ Nonempty (↑s ↪ ↑∅)