no goals
α : Type u_1
β : Type ?u.43189
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
hz : 0 < k
⊢ ↑(orderEmbOfFin s h) { val := 0, isLt := hz } = min' s (_ : Finset.Nonempty s)
simp only [orderEmbOfFin_apply, Fin.val_mk, sorted_zero_eq_min']