case intro
α✝ : Sort ?u.366
β : Sort u_2
α : Sort u_1
f : α ≃ β
n : ℕ
e : α ≃ Fin n
⊢ Finite β
α✝ : Sort ?u.366
β : Sort u_2
α : Sort u_1
h : Finite α
f : α ≃ β
⊢ Finite β
cases' h with n e
no goals
case intro
α✝ : Sort ?u.366
β : Sort u_2
α : Sort u_1
f : α ≃ β
n : ℕ
e : α ≃ Fin n
⊢ Finite β
exact Finite.intro (f.symm.trans e)