case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
hi : InjOn f s
a✝ : Fintype ↑(f '' s)
⊢ Set.Finite s
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
h : Set.Finite (f '' s)
hi : InjOn f s
⊢ Set.Finite s
cases h
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
hi : InjOn f s
a✝ : Fintype ↑(f '' s)
⊢ Set.Finite s
exact
  ⟨Fintype.ofInjective (fun a => (⟨f a.1, mem_image_of_mem f a.2⟩ : f '' s)) fun a b eq =>
      Subtype.eq <| hi a.2 b.2 <| Subtype.ext_iff_val.1 eq⟩