fix: .eq_def theorem generation with messy universes

closes #4673

Author: leodemoura

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

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