refactor: use std::optional

[eric-wieser]

This PR removes the custom lean::optional now that C++20 is available.

The only breakage is that the forwarding constructor now needs an initial std::in_place argument.

One motivation for this is that it replaces #10815, which corrects an inefficient move constructor and an exception-unsafe copy-constructor.

Future stylistic cleanup could use nullopt in more places and drop the some helpers, or even drop the lean::optional alias entirely.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e61bb27413928f773d9046cb760e965d1affe94e --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-17 17:25:29)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e61bb27413928f773d9046cb760e965d1affe94e --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-17 17:25:31)

[Kha]

!bench

[leanprover-radar]

Benchmark results for 6fdb26f against e61bb27 are in. No significant results found. @Kha

• 🟥 build//instructions: +1.7G (+0.02%)

No significant changes detected.