rw [hs.encard_eq, top_le_iff, encard_eq_top_iff, Set.Infinite, iff_true_intro ht,
  not_true, false_iff]
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ ¬Nonempty (↑s ↪ ↑t)