rw [← ht.cast_ncard_eq, Nat.cast_inj, ncard_eq_toFinset_card t ht] at hcard
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
ht : t.Finite
⊢ Nonempty (Fin n ↪ ↑s)
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ Nonempty (Fin n ↪ ↑s)