diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 49992e0ae8..ff36e11b90 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -509,15 +509,14 @@ private def matchEqBwdPat (p : Expr) : M Unit := do
     if (n.heqProofs || n.isCongrRoot) &&
        (!useMT || n.mt == gmt) then
       let_expr Eq α lhs rhs := n.self | pure ()
-      if (← isDefEq α pα) then
-         let c₀ : Choice := { cnstrs := [], assignment, gen := n.generation }
-         let go (lhs rhs : Expr) : M Unit := do
-           let some c₁ ← matchArg? c₀ plhs lhs |>.run | return ()
-           let some c₂ ← matchArg? c₁ prhs rhs |>.run | return ()
-           modify fun s => { s with choiceStack := [c₂] }
-           processChoices
-         go lhs rhs
-         go rhs lhs
+      if let some c₀ ← matchArg? { cnstrs := [], assignment, gen := n.generation } pα α |>.run then
+        let go (lhs rhs : Expr) : M Unit := do
+          let some c₁ ← matchArg? c₀ plhs lhs |>.run | return ()
+          let some c₂ ← matchArg? c₁ prhs rhs |>.run | return ()
+          modify fun s => { s with choiceStack := [c₂] }
+          processChoices
+        go lhs rhs
+        go rhs lhs
     if isSameExpr n.next false then return ()
     curr := n.next
 
diff --git a/tests/lean/run/grind_eq_bwd_pat_bug.lean b/tests/lean/run/grind_eq_bwd_pat_bug.lean
new file mode 100644
index 0000000000..53560ea5c5
--- /dev/null
+++ b/tests/lean/run/grind_eq_bwd_pat_bug.lean
@@ -0,0 +1,4 @@
+@[grind ←=] theorem inv_eq {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := sorry
+
+theorem test {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := by
+  grind