`grind` missing patterns for simple inequalities

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 is unable to perform very simple inequality manipulations, causing it to fail to discover some one-line proofs.

Context

I was teaching myself Lean by formalizing my old Honors Calculus homework, and I discovered that there are some simple manipulations using inequalities that grind is unable to use. Specifically Nat.mul_le_mul_left and Int.mul_le_mul_of_nonneg_left, but there seem to be more as well.

Steps to Reproduce

#check Nat.mul_le_mul_left
-- Nat.mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m
#check Nat.mul_le_mul_right
-- Nat.mul_le_mul_right {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k

example {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m := by
  grind --Err: `grind` failed

example {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k := by
  grind --Err: `grind` failed

grind_pattern Nat.mul_le_mul_left => k * n, k * m
grind_pattern Nat.mul_le_mul_right => n * k, m * k

example {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m := by
  grind --success

example {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k := by
  grind --success

Expected behavior: Grind should be able to perform these simple manipulations of inequalities

Actual behavior: Grind does not recognize the theorems as applicable even if the goal is the theorem exactly.

Versions

Tested locally on Lean 4.29.0-rc6, as well as on Lean4Web with Lean 4.30.0-nightly-2026-03-12.

Additional Information

Importing Mathlib does not resolve the issue, if that is relevant.

Impact

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

Start by running the minimal examples using Nat.mul_le_mul_left and Nat.mul_le_mul_right, then compare them with the versions that include grind_pattern. Trace the grind entry point and its handling of these theorem patterns. Done means the inequalities succeed without explicit pattern declarations, with regression coverage for the reproducer.