chore: add ReaderT.mk and StateT.mk

[eric-wieser]

These complement the existing ExceptT.mk and OptionT.mk, and provide a symbol to key simp lemmas on, to prevent getting stuck on StateT.run (fun s => f s) s.

A future PR could insert these new mks into the implementation of many definitions, such that unfolding the definitions leaves appropriate casts behind; but this is invasive, and by itself having mk provides value.

[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 310abce62b40e4b876f797c4aef7e29d483feb42 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-02 07:55:11)

[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 310abce62b40e4b876f797c4aef7e29d483feb42 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-02 07:55:13)