Attempt tweaking defeq heuristic

leanprover · Dec 8, 2024 · 937190f · 937190f
1 parent 6e60d13
commit 937190f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
@@ -1364,7 +1364,7 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
     unfold s (pure .undef) fun s =>
       isDefEqLeftRight fn t s
   | .app _ _,     .app _ _     =>
-    if (← tryHeuristic t s) then
+    if (← getProjectionFnInfo? fn).isNone && (← tryHeuristic t s) then
       return .true
     else
       unfold t