perf: whnf projections during defeq

src/Lean/Meta/ExprDefEq.lean

@@ -1732,24 +1732,19 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   -- TODO: investigate whether this is the place for putting this check
   if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then return true
   if (← isDefEqProj t s) then return true
-  let t' ← whnfCore t
-  let s' ← whnfCore s
-  if t != t' || s != s' then
-    Meta.isExprDefEqAux t' s'
+  whenUndefDo (isDefEqNative t s) do
+  whenUndefDo (isDefEqNat t s) do
+  whenUndefDo (isDefEqOffset t s) do
+  whenUndefDo (isDefEqDelta t s) do
+  if t.isConst && s.isConst then
+    if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
+  else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
+    return true
   else
-    whenUndefDo (isDefEqNative t s) do
-    whenUndefDo (isDefEqNat t s) do
-    whenUndefDo (isDefEqOffset t s) do
-    whenUndefDo (isDefEqDelta t s) do
-    if t.isConst && s.isConst then
-      if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
-    else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
-      return true
-    else
-      whenUndefDo (isDefEqProjInst t s) do
-      whenUndefDo (isDefEqStringLit t s) do
-      if (← isDefEqUnitLike t s) then return true else
-      isDefEqOnFailure t s
+    whenUndefDo (isDefEqProjInst t s) do
+    whenUndefDo (isDefEqStringLit t s) do
+    if (← isDefEqUnitLike t s) then return true else
+    isDefEqOnFailure t s
 
 private def mkCacheKey (t : Expr) (s : Expr) : Expr × Expr :=
   if Expr.quickLt t s then (t, s) else (s, t)
@@ -1774,9 +1769,8 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
   checkMaxHeartbeats "isDefEq"
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
-  -- We perform `whnfCore` again with `deltaAtProj := true` at `isExprDefEqExpensive` after `isDefEqProj`
-  let t' ← whnfCore t (deltaAtProj := false)
-  let s' ← whnfCore s (deltaAtProj := false)
+  let t' ← whnfCore t
+  let s' ← whnfCore s
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else

src/Lean/Meta/WHNF.lean

@@ -490,7 +490,6 @@ expand let-expressions, expand assigned meta-variables.
 
 The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
 then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
-We only set this flag to `false` when implementing `isDefEq`.
 
 If `simpleReduceOnly`, then `iota` and projection reduction are not performed.
 Note that the value of `deltaAtProj` is irrelevant if `simpleReduceOnly = true`.