feat: set priority in monadic class instances

[JovanGerb]

This PR changes the priority of some instances with monad transformers, most notably adding high priority to MonadExceptOf ε (ExceptT ε m). This means that in ExceptT α MetaM, throw will now throw the α instead of the Exception.

These instances now have high priority:

• 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)

And these instance now have low priority:

• MonadExceptOf Unit (OptionT m)
• [MonadExcept ε m] {α : Type v} : OrElse (m α)

The last one makes sure that the OrElse instance has 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, it has to be set 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

[JovanGerb]

!bench

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6725 has successfully built against this PR. (2025-01-21 14:23:57) View Log