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.

src/data/fin.lean

@@ -109,6 +109,8 @@ lemma eq_iff_veq (a b : fin n) : a = b ↔ a.1 = b.1 :=
 lemma ne_iff_vne (a b : fin n) : a ≠ b ↔ a.1 ≠ b.1 :=
 ⟨vne_of_ne, ne_of_vne⟩
 
+@[simp] lemma mk_eq_subtype_mk (a : ℕ) (h : a < n) : mk a h = ⟨a, h⟩ := rfl
+
 protected lemma mk.inj_iff {n a b : ℕ} {ha : a < n} {hb : b < n} :
   (⟨a, ha⟩ : fin n) = ⟨b, hb⟩ ↔ a = b :=
 ⟨subtype.mk.inj, λ h, by subst h⟩