feat(data/finset/sort): range_mono_of_fin (#3987)
feat(data/finset/sort): range_mono_of_fin (#3987)

Add a `simp` lemma giving the range of `mono_of_fin`.






leanprover-community/mathlib,leanprover-community/mathlib