feat: allow EStateM to be used universe-polymorphically

[eric-wieser]

This doesn't change IO or ST (such a change would be more invasive and require approval of #3011), but does enable downstream projects like Mathlib to use EStateM for their own purposes with full universe polymorphism.
The alternative is defining an entire copy of EStateM, which is a lot of boilerplate.

The generalized EStateM.map after this change can be invoked (in the non-monadic spelling) with ULift.up to move between universes. Previously it was only universe-monomorphic.

There seems to be no cost associated behind this generalization, besides that one test of the new compiler has its log output reordered.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-01 21:00:48)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 48711ce6ebefd6805b01c697703a8e6389e6b8cf --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 12:49:29)

[eric-wieser]

Marking this as "ready-for-review", since it seems that some Lean change in the last 9 month remove any fallout this once had (perhaps it was just a case of stage0 being outdated at the time)