Universe normalization associates max suboptimally

[eric-wieser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When working with terms containing max u v w level parameters, Lean.Level.normalize often normalizes these to max (max u v) w.
Recall that `(level| max $u $v $w) refers to max u (max v w), so this choice is inconsistent with the associativity of the notation

Context

Explicit universe arguments frequently appear in the goal state in Mathlib's Cardinal library, and it is frustrating when the shorter max u v w x is replaced with the long max (max (max u v) w) x.

Discovered in this Zulip thread.

Steps to Reproduce

Run the following:

universe u v w
set_option pp.all true
example (x y : ULift.{max u v w} Nat) : x = y := by
  sorry

Expected behavior: State is

x y : ULift.{max u v w, 0} Nat
⊢ @Eq.{max (u + 1) (v + 1) (w + 1)} (ULift.{max u v w, 0} Nat) x y

Actual behavior: State is

x y : ULift.{max u v w, 0} Nat
⊢ @Eq.{max (max (u + 1) (v + 1)) (w + 1)} (ULift.{max u v w, 0} Nat) x y

Either changing the normalization or changing the associativity of the notation would fix this.

Versions

[Output of #version or #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kmill]

#5695