α : Type ?u.35647
β : Type ?u.35650
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < k
α : Type ?u.35647
β : Type ?u.35650
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < List.length (sort (fun x x_1 => x ≤ x_1) s)
rw [length_sort, h]
no goals
α : Type ?u.35647
β : Type ?u.35650
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < k
exact i.2