grind fails to activate lemma with `-1` in its pattern

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following example, grind fails to activate a lemma with a pattern containing -1. If the lemma is used as grind [→ blub], it seems that grind automatically activates it and everything works.

def f (x : Int) := -x
opaque a (x : Int) : Bool
opaque b (x : Int) : Bool

@[grind →]
theorem blub (x : Int) (h : a (-1 * x)) : b x := by
  sorry

/--
error: `grind` failed
case grind
x : Int
h : a (-x) = true
h_1 : b x = false
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] a (-1 * x) = true
    [prop] b x = false
  [eqc] Equivalence classes
    [eqc] {false, b x}
    [eqc] {true, a (-1 * x)}
  [cutsat] Assignment satisfying linear constraints
    [assign] x := 0
-/
#guard_msgs in
example (x : Int) (h : a (-x)) : b x := by
  grind

/--
warning: this parameter is redundant, environment already contains `blub` annotated with `@[grind →]`
-/
#guard_msgs in
example (x : Int) (h : a (-x)) : b x := by
  grind [→ blub]

Expected behavior: [Clear and concise description of what you expect to happen]

No error, grind should apply blub and succeed.

Actual behavior: [Clear and concise description of what actually happens]

grind only succeeds when blub is passed explicitly.

Versions

Lean 4.30.0-nightly-2026-03-02
Target: x86_64-unknown-linux-gnu

Additional Information

It's instructive to enable a few traces:

set_option trace.grind.ematch.pattern true
set_option trace.grind.debug.theorem.activate true

def f (x : Int) := -x
opaque a (x : Int) : Bool
opaque b (x : Int) : Bool

/--
trace: [grind.ematch.pattern] blub: [a (@HMul.hMul `[Int] `[Int] `[Int] `[instHMul] `[-1] #1)]
---
warning: declaration uses `sorry`
-/
#guard_msgs in
@[grind →]
theorem blub (x : Int) (h : a (-1 * x)) : b x := by
  sorry

/--
error: `grind` failed
case grind
x : Int
h : a (-x) = true
h_1 : b x = false
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] a (-1 * x) = true
    [prop] b x = false
  [eqc] Equivalence classes
    [eqc] {false, b x}
    [eqc] {true, a (-1 * x)}
  [cutsat] Assignment satisfying linear constraints
    [assign] x := 0
---
trace: [grind.debug.theorem.activate] `a` => `blub`
[grind.debug.theorem.activate] reinsert `blub`
[grind.debug.theorem.activate] `HMul.hMul` => `blub`
[grind.debug.theorem.activate] reinsert `blub`
-/
#guard_msgs in
example (x : Int) (h : a (-x)) : b x := by
  grind

/--
warning: this parameter is redundant, environment already contains `blub` annotated with `@[grind →]`
---
trace: [grind.debug.theorem.activate] `a` => `blub`
[grind.debug.theorem.activate] reinsert `blub`
[grind.debug.theorem.activate] `HMul.hMul` => `blub`
[grind.debug.theorem.activate] reinsert `blub`
---
trace: [grind.ematch.pattern] blub: [a (@HMul.hMul `[Int] `[Int] `[Int] `[instHMul] `[-1] #1)]
-/
#guard_msgs in
example (x : Int) (h : a (-x)) : b x := by
  grind [→ blub]

Perhaps Neg.neg becomes a guard symbol, but later -1 is treated as a literal, so that blub is never being activated.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the self-contained grind reproducer and enable the trace.grind.ematch.pattern and trace.grind.debug.theorem.activate options shown in the issue. Follow the grind pattern-matching and theorem-activation entry points to determine why -1 prevents automatic activation; done means the unmodified grind example succeeds without explicitly passing blub.