`grind` fails where `subst; grind` succeeds

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

Here is the example:

example (n t d B' t' : Int)
    (h1 : 4 * n = t ^ 2 - d * (2 * B' + 1) ^ 2)
    (h2 : t = 2 * t' + 1) :
    4 ∣ 1 - d := by
  grind -- fails

My current belief is that it fails because one of the propagators fires before cc runs using h2. Note that subst h2; grind succeeds.
I think this last observation is inconsistent with the description of grind here https://lean-lang.org/doc/reference/latest/The--grind--tactic/; since the subst h2; grind proof is using a congruence closure step before running grind, so this behaviour is confusing to beginners.

Context

This came up here: #ItaLean 2025 > Projects: Improve Automation @ 💬

Steps to Reproduce

1. Code as above.

Expected behavior: grind fails.

Actual behavior: grind succeeds, or subst h2; grind also fails.

Versions

Lean 4.27.0-nightly-2025-12-11 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.

No source file or test is named. Start by running the minimal Int example with grind and with subst h2; grind on the referenced Lean nightly, then read the grind tactic documentation and trace the differing behavior. Done means the discrepancy is reproduced and the intended behavior is established with a regression test or a clearly confirmed explanation.