exact Nonempty.intro <| (hf.equiv _).symm
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
h : s.encard = t.encard
f : β → α
hf : BijOn f t s
⊢ Nonempty (↑s ≃ ↑t)
no goals