mathlib

9f252442 - chore(data/finset/sort): upgrade `finset.mono_of_fin` to an `order_iso` (#5495)

chore(data/finset/sort): upgrade `finset.mono_of_fin` to an `order_iso` (#5495) * Upgrade `finset.mono_of_fin` to an `order_embedding`. * Drop some lemmas that now immediately follow from `order_embedding.*`. * Upgrade `finset.mono_equiv_of_fin` to `order_iso`. * Define `list.nodup.nth_le_equiv` and `list.sorted.nth_le_iso`. * Upgrade `mono_equiv_of_fin` to an `order_iso`, make it `computable`.