no goals
α : Type u_1
β : Type ?u.61043
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ card s
a : Fin k
⊢ ↑(orderEmbOfCardLe s h) a ∈ s
simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem,
  Function.comp_apply]