diff --git a/tests/lean/pplevel.lean.expected.out b/tests/lean/pplevel.lean.expected.out
index cc9abba3ea..e6e05f6c2e 100644
--- a/tests/lean/pplevel.lean.expected.out
+++ b/tests/lean/pplevel.lean.expected.out
@@ -1,6 +1,6 @@
 Type (max u v w) : Type ((max u v w) + 1)
 Type u : Type (u + 1)
 id.{max u v w} : {α : Sort (max u v w)} → α → α
-Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max (w + 1) ((max u v) + 1))
+Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max ((max u v) + 1) (w + 1))
 Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1)
 Type u_1 : Type (u_1 + 1)