fix: universe level in .below and .brecOn construction (#4651)

I made a mistake in #4517, fixed here, so about time to add a test.

I wonder if this generic level optimization should be moved into
`mkLevelMax'`, but not today.

fixes #4650

src/Lean/Meta/Constructions/BRecOn.lean

@@ -149,8 +149,8 @@ private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
     if ibelow then
       0
     else if indVal.isReflexive then
-      if let .max 1 lvl := ilvl then
-        mkLevelMax' (.succ lvl) lvl
+      if let .max 1 ilvl' := ilvl then
+        mkLevelMax' (.succ lvl) ilvl'
       else
         mkLevelMax' (.succ lvl) ilvl
     else
@@ -317,8 +317,8 @@ def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
     if ind then
       0
     else if indVal.isReflexive then
-      if let .max 1 lvl := ilvl then
-        mkLevelMax' (.succ lvl) lvl
+      if let .max 1 ilvl' := ilvl then
+        mkLevelMax' (.succ lvl) ilvl'
       else
         mkLevelMax' (.succ lvl) ilvl
     else

tests/lean/run/issue4650.lean

@@ -0,0 +1,47 @@
+set_option pp.universes true
+
+inductive Foo1 : Sort (max 1 u) where
+  | intro: (h : Nat → Foo1) → Foo1
+
+/--
+info: Foo1.below.{u_1, u} {motive : Foo1.{u} → Type u_1} (t : Foo1.{u}) : Sort (max (u_1 + 1) u)
+-/
+#guard_msgs in
+#check Foo1.below
+
+inductive Foo2 : Sort (max u 1) where
+  | intro: (h : Nat → Foo2) → Foo2
+
+/--
+info: Foo2.below.{u_1, u} {motive : Foo2.{u} → Type u_1} (t : Foo2.{u}) : Sort (max (u_1 + 1) u 1)
+-/
+#guard_msgs in
+#check Foo2.below
+
+inductive Foo3 : Sort (u+1) where
+  | intro: (h : Nat → Foo3) → Foo3
+
+/-- info: Foo3.below.{u_1, u} {motive : Foo3.{u} → Type u_1} (t : Foo3.{u}) : Type (max u_1 u) -/
+#guard_msgs in
+#check Foo3.below
+
+inductive Foo4 : Sort (max 1 u) where
+  | intro: Foo4 → Foo4
+
+/-- info: Foo4.below.{u_1, u} {motive : Foo4.{u} → Sort u_1} (t : Foo4.{u}) : Sort (max 1 u_1) -/
+#guard_msgs in
+#check Foo4.below
+
+inductive Foo5 : Sort (max u 1) where
+  | intro: Foo5 → Foo5
+
+/-- info: Foo5.below.{u_1, u} {motive : Foo5.{u} → Sort u_1} (t : Foo5.{u}) : Sort (max 1 u_1) -/
+#guard_msgs in
+#check Foo5.below
+
+inductive Foo6 : Sort (u+1) where
+  | intro: Foo6 → Foo6
+
+/-- info: Foo6.below.{u_1, u} {motive : Foo6.{u} → Sort u_1} (t : Foo6.{u}) : Sort (max 1 u_1) -/
+#guard_msgs in
+#check Foo6.below