α : Type ?u.20499
β : Type ?u.20502
inst✝ : LinearOrder α
s : Finset α
h : card s - 1 < card s
⊢ Finset.Nonempty s
α : Type ?u.20499
β : Type ?u.20502
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
⊢ Finset.Nonempty s
rw [length_sort] at h
no goals
α : Type ?u.20499
β : Type ?u.20502
inst✝ : LinearOrder α
s : Finset α
h : card s - 1 < card s
⊢ Finset.Nonempty s
exact card_pos.1 (lt_of_le_of_lt bot_le h)