no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Finite s
⊢ range ↑(Equiv.asEmbedding (Fintype.equivFin ↑↑(Finite.toFinset h)).symm) = s
simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]