fix: universe normalization in getDecLevel

[sgraf812]

This PR adds level instantiation and normalization in getDecLevel and getDecLevel? before calling decLevel.

getLevel can return levels with uninstantiated metavariables or un-normalized structure, such as max ?u ?v where the metavariables have already been assigned. After instantiation and normalization (via normalizeLevel), a level like max ?u ?v (with ?u := 1, ?v := 0) simplifies to 1 = succ 0, which decLevel can decrement. Without this step, decLevel sees max ?u ?v, tries to decrement both arms, fails on a zero-valued arm, and reports "invalid universe level".

Concretely, this fixes for loops with mut variables of sort-polymorphic type (e.g. PProd Nat True) where the state tuple's universe level ends up as an uninstantiated max.

The expected-output change in doNotation1.lean is because the for loop's unit type now resolves to Unit instead of PUnit due to the improved level handling.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for c992f58 against d76e5a1 are in. No significant results found. @sgraf812

• ✅ build//instructions: -2.8G (-0.02%)

Small changes (4✅, 2🟥)

• ✅ build/module/Lean.Language.Lean//instructions: -52.9M (-0.73%)
• ✅ build/module/Lean.Meta.Match.MatchEqs//instructions: -36.5M (-0.53%)
• ✅ build/module/Lean.Meta.Match.MatcherApp.Transform//instructions: -37.7M (-0.64%)
• ✅ build/module/Std.Time.DateTime.PlainDateTime//instructions: -26.7M (-0.95%)
• 🟥 compiled/nat_repr//task-clock: +22ms (+2.19%)
• 🟥 compiled/nat_repr//wall-clock: +22ms (+2.22%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-13 16:09:01)