omega hits the recursion limit on a reflexive multiplication goal with an unused hypothesis

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: nightly-2026-09-09, commit fe53f21e05980b97d7bbb6717cf7566e3700e576.

Description

omega fails on a reflexive natural-number inequality when an unused multiplication hypothesis is present. The failure occurs in its preliminary assumption check, before the arithmetic solver runs.

Context

This arose while upgrading proofs involving 128/192-bit arithmetic. The large powers are unnecessary to reproduce the failure; the example below needs no imports or option changes.

Steps to Reproduce

example (m : Nat) (h : m * 1000 ≤ 0) :
    (1000 : Nat) * 1000 ≤ 1000 * 1000 := by
  omega

Expected behavior: omega proves the reflexive inequality.

Actual behavior: maximum recursion depth has been reached at omega.

Adding clear h before omega makes the example succeed.

Versions

Output of #eval Lean.versionString:

"4.35.0-nightly-2026-09-09"

Commit: fe53f21e05980b97d7bbb6717cf7566e3700e576.

OS: Debian GNU/Linux 13.6 (trixie), x86_64.

The example succeeds on Lean 4.27.0 and fails on 4.29.0, 4.32.2, 4.33.0, and 4.34.0-rc2.

Bisection

The regression was introduced by ab26eaf647c36df820450f3a1efdc414194c3be3 (#12572).

Revision	Result
833434cd56a5fab011bc3380236c239d92c0d178	Succeeds
ab26eaf647c36df820450f3a1efdc414194c3be3	Recursion-depth error

Technical details

In evalOmega, the preliminary assumption check uses .instances transparency. The introducing commit changed the reducibility of Nat.mul, allowing multiplication to unfold at that transparency.

A trace shows isDefEq comparing 1000 * 1000 with m * 1000. After failing to match 1000 with m, it unfolds both multiplications and repeats with coefficients 999, 998, and so on until the recursion limit is reached. Recursion-depth exceptions propagate through the ordinary <|> fallback, so the arithmetic solver never runs. Calling Lean.Elab.Tactic.Omega.omegaDefault directly succeeds on the investigated snapshot.

A possible local fix is to treat recursion-depth exhaustion in this preliminary check as a failed assumption attempt, then continue with the arithmetic solver.

Related issue

Related: #5613 also involves recursive arithmetic unfolding during a speculative tactic step, but it predates this regression. There, apply?/exact? try Nat.le_of_sub_eq_zero, followed by rfl on x - 125 = 0, which unfolds subtraction. Its reproducer already fails on the passing parent above, and remains failing with the proposed local omega fix. This report therefore concerns a separate regression in omega. Earlier, #3525 removed expensive definitional-equality checks between solver atoms; the failure here occurs before the solver runs.

Impact

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

Assisted by GPT-6 Astra

Start with src/Lean/Elab/Tactic/Omega/Frontend.lean at evalOmega and reproduce the minimal example from the issue on the stated nightly version. Trace the preliminary assumption check and compare it with the direct omegaDefault behavior described. Done means the reflexive inequality succeeds despite the unused multiplication hypothesis, without a recursion-depth error.