case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
a✝ : Fintype ↑s
⊢ Set.Finite (f '' s)
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
hs : Set.Finite s
⊢ Set.Finite (f '' s)
cases hs
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
a✝ : Fintype ↑s
⊢ Set.Finite (f '' s)
apply toFinite