fix: add a missing case to Level.geq (#2689)

This PR adds a case to `Level.geq` that is present in the kernel's level
`is_geq` procedure, making them consistent with one another.

This came up during testing of `lean4lean`. Currently `Level.geq`
differs from `level::is_geq` in the case of `max u v >= imax u v`. The
elaborator function is overly pessimistic and yields `false` on this
while the kernel function yields true. This comes up concretely in the
`Trans` class:
```lean
class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where
  trans : r a b → s b c → t a c
```
The type of this class is `Sort (max (max (max (max (max (max 1 u) u_1)
u_2) u_3) v) w)` (where `u_1 u_2 u_3` are the levels of `α β γ`), but if
you try writing that type explicitly then the `class` command fails.
Omitting the type leaves the `class` to infer the universe level (the
command assumes the level is correct, and the kernel agrees it is), but
including the type then the elaborator checks the level inequality with
`Level.geq` and fails.

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/Lean/Level.lean

@@ -599,17 +599,20 @@ def geq (u v : Level) : Bool :=
 where
   go (u v : Level) : Bool :=
     u == v ||
+    let k := fun () =>
+      match v with
+      | imax v₁ v₂ => go u v₁ && go u v₂
+      | _          =>
+        let v' := v.getLevelOffset
+        (u.getLevelOffset == v' || v'.isZero)
+        && u.getOffset ≥ v.getOffset
     match u, v with
-    | _,          zero       => true
-    | u,          max v₁ v₂  => go u v₁ && go u v₂
-    | max u₁ u₂,  v          => go u₁ v || go u₂ v
-    | u,          imax v₁ v₂ => go u v₁ && go u v₂
-    | imax _  u₂, v          => go u₂ v
-    | succ u,     succ v     => go u v
-    | _, _ =>
-      let v' := v.getLevelOffset
-      (u.getLevelOffset == v' || v'.isZero)
-      && u.getOffset ≥ v.getOffset
+    | _,          zero      => true
+    | u,          max v₁ v₂ => go u v₁ && go u v₂
+    | max u₁ u₂,  v         => go u₁ v || go u₂ v || k ()
+    | imax _  u₂, v         => go u₂ v
+    | succ u,     succ v    => go u v
+    | _,          _         => k ()
   termination_by (u, v)
 
 end Level

tests/lean/run/2689.lean

@@ -0,0 +1,36 @@
+/-!
+# Tests of universe constraints for inductive types
+
+https://github.com/leanprover/lean4/pull/2689 corrected the elaborator's `Level.geq`,
+which was missing cases that the kernel `is_geq` could handle.
+-/
+
+/-!
+This always worked. The universe level of `Trans₁` is inferred from the fields.
+-/
+structure Trans₁ {α : Sort a} {β : Sort b} {γ : Sort c}
+    (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where
+  trans : r a b → s b c → t a c
+
+/-!
+Regression test: This was failing. An explicit universe invokes `Level.geq`.
+-/
+structure Trans₂ {α : Sort a} {β : Sort b} {γ : Sort c}
+    (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) :
+    Sort (max 1 a b c u v w) where
+  trans : r a b → s b c → t a c
+
+/-!
+Regression test: This was failing. An explicit universe invokes `Level.geq`.
+-/
+inductive Trans₃ {α : Sort a} {β : Sort b} {γ : Sort c}
+    (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) :
+    Sort (max 1 a b c u v w) where
+  | mk : (∀ a b c, r a b → s b c → t a c) → Trans₃ r s t
+
+/-!
+Regression test: This was failing due to the included `Type (max u v)`
+even though this is the inferred universe.
+-/
+inductive I (α : Type u) (Hom : α → α → Sort v) : Type (max u v) where
+  | mk (id : ∀ X : α, Hom X X)

tests/lean/run/level.lean

@@ -6,3 +6,4 @@ open Lean
 #guard levelZero != mkLevelSucc levelZero
 #guard mkLevelMax (mkLevelSucc levelZero) levelZero != mkLevelSucc levelZero
 #guard mkLevelMax (mkLevelSucc levelZero) levelZero == mkLevelMax (mkLevelSucc levelZero) levelZero
+#guard Level.geq (.max (.param `u) (.param `v)) (.imax (.param `u) (.param `v))