simp only [Finite.mem_toFinset]
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
⊢ { x // x ∈ ht.toFinset } ↪ ↑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
⊢ { x // x ∈ t } ↪ ↑s