fix: auxiliary whnfAux used at mkEqns

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -132,10 +132,11 @@ def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := wit
   replaceTargetDefEq mvarId (← mkEq lhs rhs)
 
 private partial def whnfAux (e : Expr) : MetaM Expr := do
-  let e ← whnfR e
-  match e with
-  | Expr.proj _ _ s _ => e.updateProj! (← whnfAux s)
-  | _ => e
+  let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
+  let f := e.getAppFn
+  match f with
+  | Expr.proj _ _ s _ => mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
+  | _ => return e
 
 /-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
 def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do

tests/lean/run/eqnsAtSimp3.lean

@@ -0,0 +1,19 @@
+import Lean
+
+open Lean
+open Lean.Meta
+def tst (declName : Name) : MetaM Unit := do
+  IO.println (← getEqnsFor? declName)
+
+def f (x y : Nat) : Nat :=
+  match x, y with
+  | 0,   0 => 1
+  | 0,   y => y
+  | x+1, 5 => 2 * f x 0
+  | x+1, y => 2 * f x y
+
+#eval tst ``f
+#check f._eq_1
+#check f._eq_2
+#check f._eq_3
+#check f._eq_4