diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index b27cb5249c..dd3be8a93b 100644
--- a/src/Lean/Level.lean
+++ b/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
diff --git a/tests/lean/run/2689.lean b/tests/lean/run/2689.lean
new file mode 100644
index 0000000000..12a2775c56
--- /dev/null
+++ b/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)
diff --git a/tests/lean/run/level.lean b/tests/lean/run/level.lean
index ecf7d3b263..fe9d340edc 100644
--- a/tests/lean/run/level.lean
+++ b/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))