From 166d1c0dab729868ff5f5af4c7a0f232cce39b96 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 15 Jul 2025 11:38:11 -0700
Subject: [PATCH] perf: avoid `isDefEq` test at `simpEq` simproc used in
 `grind` (#9385)

This PR replaces the `isDefEq` test in the `simpEq` simproc used in
`grind`. It is too expensive.
---
 src/Lean/Meta/Tactic/Grind/SimpUtil.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
index 061058996a..019411dcd0 100644
--- a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
@@ -52,7 +52,7 @@ builtin_simproc_decl simpEq (@Eq _ _ _) := fun e => do
       return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.bool_eq_to_prop) lhs rhs }
     return .continue
   | _ =>
-    if (← isDefEq lhs rhs) then
+    if lhs == rhs then
       let u := f.constLevels!
       return .done { expr := mkConst ``True, proof? := mkApp2 (mkConst ``eq_self u) α lhs }
     else if rhs == mkConst ``True then