`grind` is defeated by trivial `List` goal

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

grind fails to prove the following goal:

example {l : List Nat} : l ++ [0] ≠ [] := by
  grind

This fails running out of ematching rounds, with the diagnostics pointing at the lemmas List.append_assoc and List.cons_append. Removing them from the grind set causes grind to no longer run into the threshold, but it still fails to prove the goal.

I'm sorry if this is out of scope for grind, but it seems simple enough that grind ought to be able to do it.

Expected behavior: grind proves the goal.

Actual behavior: grind fails

Versions

Lean 4.30.0-nightly-2026-03-09 on live.lean-lang.org

Impact

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

Start by reproducing the minimal List Nat example with grind on the reported Lean nightly version, then inspect how the tactic handles List.append_assoc and List.cons_append during ematching. Done means grind proves l ++ [0] ≠ [] without exhausting its ematching-round threshold.