`ungrind` mode error message refers to non-existent `show_patterns` tactic

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

When grind tactic mode fails to instantiate new facts, it prints an error message suggesting to take a look at the theorems' patterns via a show_patterns tactic. However, such a tactic does not exist.

Steps to Reproduce

Take a look at the test grind_preinstance_set_bug.lean:

opaque f : Nat → Nat
opaque g : Nat → Nat
theorem fax : f (x + 1) = g (f x) := sorry

/--
error: `instantiate` tactic failed to instantiate new facts, use `show_patterns` to see active theorems and their patterns.
-/
#guard_msgs in
example : f (x + 5) = a := by
  grind =>
    use [fax]; use [fax]; use [fax]; use [fax]; use [fax];
    use [fax] -- Should fail - no new facts
    -- try writing `show_patterns` here; tactic does not exist

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

If a tactic (or command?) is mentioned, it should exist. Therefore, I would expect a show_patterns tactic to exist alongside show_local_thms etc.

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

show_patterns does not exist. The other tactics I know of, such as show_local_thms, do not actually show the e-matching patterns of the local theorems.

Versions

Lean 4.28.0-nightly-2026-01-12
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the grind_preinstance_set_bug.lean reproduction and the failing instantiate diagnostic. Trace how grind reports the missing show_patterns tactic and inspect the existing show_local_thms behavior. Done means the reported guidance names an available way to inspect theorem patterns, with the regression test passing.