From b6b2816112351e238ab2cbdd0cd5186125f1ae48 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 9 Jul 2024 18:55:16 -0700
Subject: [PATCH] fix: `.eq_def` theorem generation with messy universes

closes #4673
---
 src/Lean/Elab/PreDefinition/Eqns.lean |  2 +-
 tests/lean/run/4673.lean              | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/4673.lean

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index b180e3d6dcbc..3add152548ad 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -333,7 +333,7 @@ def tryContradiction (mvarId : MVarId) : MetaM Bool := do
 partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
   let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for '{declName}'"
   let tryEqns (mvarId : MVarId) : MetaM Bool :=
-    eqs.anyM fun eq => commitWhen do
+    eqs.anyM fun eq => commitWhen do checkpointDefEq (mayPostpone := false) do
       try
         let subgoals ← mvarId.apply (← mkConstWithFreshMVarLevels eq)
         subgoals.allM fun subgoal => do
diff --git a/tests/lean/run/4673.lean b/tests/lean/run/4673.lean
new file mode 100644
index 000000000000..80c460cdfe00
--- /dev/null
+++ b/tests/lean/run/4673.lean
@@ -0,0 +1,20 @@
+def iscoh_wmap {A:Type _}{B:Type _} : (A -> B) -> Type _ :=
+  fun f => @Subtype (B -> A) fun r => ∀ a , a = r (f a)
+def wmap : Type _ -> Type _ -> Type _ :=
+  fun A B => @Sigma (A -> B) fun f => iscoh_wmap f
+
+def hgroup : Nat -> Type _ -> Type _
+| .zero , T => wmap T T
+| .succ a, T => wmap (hgroup a T) (hgroup a T)
+
+example : hgroup 0 Unit := by
+  unfold hgroup
+  admit
+
+-- TODO: we should improve univere inference. It should be
+-- hgroup.{u} : Nat → Type u → Type u
+/--
+info: hgroup.{u_1, u_2} : Nat → Type (max u_1 u_2) → Type (max u_1 u_2)
+-/
+#guard_msgs in
+#check hgroup