no goals
α : Type u_1
β : Type ?u.39891
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
⊢ Set.range ↑(orderEmbOfFin s h) = ↑s
simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h),
RelEmbedding.coe_trans, Set.image_univ, Finset.orderEmbOfFin, RelIso.range_eq,
  OrderEmbedding.subtype_apply, OrderIso.coe_toOrderEmbedding, eq_self_iff_true,
  Subtype.range_coe_subtype, Finset.setOf_mem, Finset.coe_inj]