exact Fin.sort_univ _
case h.e'_2.h.e'_4
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ = List.finRange k
no goals