chore: bump toolchain and Mathlib to v4.18.0

[kim-em]

This PR updates the Lean toolchain and Mathlib dependency to v4.18.0.

This requires two additional changes:

• The Mathlib module Mathlib.Logic.Equiv.Fin has been split, and the newly relevant import is Mathlib.Logic.Equiv.Fin.Rotate. I've also update the name of the relevant module in ForMathlib/
• A golfed proof by AlphaProof submitted in kim-em@8ec6582 actually made the proof more fragile, and in particular more fragile in way that broke when updating the toolchain. For now, I have reverted the proof for simplicity.

I'd encourage anyone interested to re-golf that proof in a way that remains compatible with v4.18.0.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[eric-wieser]

Thanks!

We are still letting the dust settle from a transition from having this be an internal to an open-source project, and until it has settled, switching the Lean version is probably a bad idea.

Nevertheless, it's still very helpful to have this PR ready to go!

[mo271]

Thanks! Perhaps also good to bump what is in ./docbuild to v4.18 simultaneously.

[mo271]

rebasing this to keep this up to date for when we need it