chore(*): bump to lean 3.19.0c, fin is now a subtype (#3955)
* Some `decidable.*` order theorems have been moved to core.
* `fin` is now a subtype.
This means that the whnf of `fin n` is now `{i // i < n}`.
Also, the coercion `fin n → nat` is now preferred over `subtype.val`.
The entire library has been refactored accordingly. (Although I probably missed some cases.)
* `in_current_file'` was removed since the bug in
`in_current_file` was fixed in core.
* The syntax of `guard_hyp` in core was changed from
`guard_hyp h := t` to `guard_hyp h : t`, so the syntax
for the related `guard_hyp'`, `match_hyp` and
`guard_hyp_strict` tactics in `tactic.interactive` was changed as well.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
