rintro rfl
case inl.mp
α : 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 ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
case inl.mp
α : Type u_1
β : Type u_2
s s₁ s₂ t✝ t' : Set α
f : α → β
t : Set β
h✝ : IsEmpty β
hs : ∅.Finite
⊢ Nonempty (↑∅ ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅