feat(data/fin): simplify fin.mk (#3996)
After the recent changes to make `fin n` a subtype, expressions
involving `fin.mk` were not getting simplified as they used to be,
since the `simp` lemmas are for the anonymous constructor, which is
`subtype.mk` not `fin.mk`. Add a `simp` lemma converting `fin.mk` to
the anonymous constructor.
In particular, unsimplified expressions involving `fin.mk` were coming
out of `fin_cases` (I think this comes from `fin_range` in
`data/list/range.lean` using `fin.mk`). I don't know if that should
be avoiding creating the `fin.mk` expressions in the first place, but
simplifying them seems a good idea in any case.
