feat: set priority in monadic class instances

[JovanGerb]

I added the high priority to these instances with monad transformers

• MonadReaderOf ρ (ReaderT ρ m)
• MonadWithReaderOf ρ (ReaderT ρ m)
• MonadStateOf σ (StateT σ m)
• MonadStateOf σ (EStateT ε σ m)
• MonadExceptOf ε (ExceptT ε m)
• MonadExceptOf ε (EStateT ε σ m)
• MonadExceptOf ε (ExceptCpsT ε m)
• MonadCallStackOf κ (CallStackT κ m)
• MonadCycleOf κ (CycleT κ m)
• MonadStore1Of k (β k) m

I added the low priority to this instance with a monad transformer

• MonadExceptOf Unit (OptionT m).

I added the low priority to MonadExcept.instOrElse, because it needs to have lower priority than instOrElseOfAlternative (this change doesn't affect the synthesis order, because the order of the files in which the instances were declared was already 'correct').

In Prelude.lean, instead of setting the priority to high or low, I had to set it to 10000 or 100, which is the same.

The increased priority of MonadExceptOf ε (ExceptT ε m) affected a few files that had to be fixed.

Closes #4212

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-09 19:19:03) View Log

[JovanGerb]

The test that broke had the number from the name generator offset by 8.
The line local infix:65 (priority := high) "*" => mul previously used to increment the name generator by 1560, and now this became 1568. I don't understand where these 8 extra names come from, but I equally don't understand why a simple infix declaration needs to use so ridiculously many names.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-09 22:09:04) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-10 23:25:37) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-11 01:25:32) View Log

[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 6aa0c46b04e78011af49eb4f272ea07e9173e584 --onto adfd6c090ef7d6bdcc8f69c5dd6f919b1b71cab3. (2024-09-12 11:37:11)

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 90ac0f7.
There were significant changes against commit 6aa0c46:

  Benchmark   Metric       Change
  ========================================
- rbmap       task-clock     2.2% (23.0 σ)
- rbmap       wall-clock     2.3% (24.8 σ)