feat: Data.Fin.Lemmas <- mathlib

[digama0]

A WIP branch for porting Mathlib.Data.Fin.Basic to std.

[fgdorais]

What kind of assistance do you require?

[digama0]

It's basically unfinished work, I made it about 1/4 of the way through the file. The task here is to remove anything referencing mathlib notions like NeZero or Equiv and otherwise de-mathlibify all the other lemmas in the file. I haven't looked too carefully at the tail end of the file, maybe there is something that shouldn't be translated, but I would expect roughly the whole thing can move to std. This is relatively high priority since the mathlib std4 bump is blocked on this (in part).

[fgdorais]

Custom recursors work better when the hypotheses have predictable and meaningful names. This is to facilitate the use of the pattern induction x using foo with | hyp ... => ... I went through and recommended better names.

PS: Also consider using motive instead of C but I don't think that's essential.

[kmill]

The de-ord-embedding/iso-ification seems like it was done right, so here's a 👍 from me, though I only checked about 400-500 lines in detail