feat: add MonadControl lemmas for ReaderT, OptionT, StateT, and ExceptT

[eric-wieser]

This PR adds missing lemmas about how ReaderT.run, OptionT.run, StateT.run, and ExceptT.run interact with MonadControl operations.

This also leaves some comments noting that the lemmas may look less general than expected; but this is because the instances are also not very general.

[eric-wieser]

changelog-library

[eric-wieser]

Perhaps one for @kim-em or @digama0

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 466a24893bcdee0a6132e8e1444f6db939d2f4d2 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-11 00:17:00)

[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 466a24893bcdee0a6132e8e1444f6db939d2f4d2 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-11 00:17:02)