no goals
α : Type u_1
β : Type ?u.44950
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
hz : 0 < k
⊢ ↑(orderEmbOfFin s h) { val := k - 1, isLt := (_ : k - 1 < k) } = max' s (_ : Finset.Nonempty s)
simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]