exact ⟨Fintype.equivFinOfCardEq <| by simpa [encard_eq_coe_toFinset_card, Nat.cast_inj] using h⟩
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Nonempty (↑s ≃ Fin n)
no goals