[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
h : Finite α
f : α ≃ β
⊢ Finite β
[PROOFSTEP]
cases' h with n e
[GOAL]
case intro
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
f : α ≃ β
n : ℕ
e : α ≃ Fin n
⊢ Finite β
[PROOFSTEP]
exact Finite.intro (f.symm.trans e)
