[Merged by Bors] - chore: replace Fin.castIso and Fin.revPerm with Fin.cast and Fin.rev for the bump of Std

[Komyyy]

Some theorems in Data.Fin.Basic are copied to Std at the recent commit in Std.
These are written using Fin.cast and Fin.rev, so declarations using Fin.castIso and Fin.revPerm in Mathlib should be rewritten.

---

[Ruben-VandeVelde]

Are these changes improvements?

[Komyyy]

@Ruben-VandeVelde Recently, the definitions like Fin.cast & Fin.rev are moved to Std and the types of Fin.cast & Fin.rev changed from OrderIso & Equiv.Perm to functions both. To prevent confusions, Fin.cast & Fin.rev and these related theorems are rewritten to Fin.castIso and Fin.revPerm. So the current Mathlib has few theorems about Fin.cast & Fin.rev.
This PR rewrites the related theorems back to Fin.cast & Fin.rev.

[eric-wieser]

I think this change is probably a good thing given that Std4 changed in the way it did, as the canonical form should usually be the lowest-common-denominator of all available bundlings.

[jcommelin]

@semorrison Could you please take a look at this PR?

[jcommelin]

One comment (applies in several places). Otherwise LGTM

Thanks for this PR!

bors d+

[bors]

✌️ Komyyy can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Komyyy]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style