case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
F : (i : α) → i ∈ s → β
a✝ : Fintype ↑s
⊢ Set.Finite {y | ∃ x hx, y = F x hx}
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
F : (i : α) → i ∈ s → β
⊢ Set.Finite {y | ∃ x hx, y = F x hx}
cases hs
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
F : (i : α) → i ∈ s → β
a✝ : Fintype ↑s
⊢ Set.Finite {y | ∃ x hx, y = F x hx}
simpa [range, eq_comm] using finite_range fun x : s => F x x.2