feat: use StateT.run instead of function application

[kim-em]

It's arguably defeq abuse to just use function application.

(To really solve this, we would make StateT irreducible, but that is not happening here.)

[tydeu]

If we are not treating StateT as see-through, are we also not going to treat ReaderT as see-through? I notice that in many of these cases this is now using run for the StateT component but not the ReadertT component of a monad stack. That strikes me as a bit confusing / inconsistent.

[leanprover-community-mathlib4-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 6a473e67aa7a750ddd90cedfb393a8c301e0d6d4 --onto 0e823710e30e0d65f02bc2b65e7af217c730ebd3. (2024-08-22 01:30:39)