Match case elimination fails on `n : Nat` with `h : n ≤ 16`

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

match will fail to eliminate remaining cases for a discriminant n : Nat when the known upper bound is at least n ≤ 16.

Steps to Reproduce

-- works
def test15 (n : Nat) (h : n ≤ 15) :=
  match n with
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | 3 => 3
  | 4 => 4
  | 5 => 5
  | 6 => 6
  | 7 => 7
  | 8 => 8
  | 9 => 9
  | 10 => 10
  | 11 => 11
  | 12 => 12
  | 13 => 13
  | 14 => 14
  | 15 => 15

/--
error: Missing cases:
(Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ _))))))))))))))))), _
-/
#guard_msgs in
def test16 (n : Nat) (h : n ≤ 16) :=
  match n with
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | 3 => 3
  | 4 => 4
  | 5 => 5
  | 6 => 6
  | 7 => 7
  | 8 => 8
  | 9 => 9
  | 10 => 10
  | 11 => 11
  | 12 => 12
  | 13 => 13
  | 14 => 14
  | 15 => 15
  | 16 => 16

Expected behavior:

Match eliminations succeeds, or, if necessary, there is an option that can be set to get Lean to try harder and then succeed.

Actual behavior:

Match elimination fails even with increases to standard "try harder" options like maxHeartbeats and maxRecDepth.

Versions

eanprover/lean4:v4.22.0-rc4
leanprover/lean4:nightly-2025-08-10

Additional Information

This is approximately the same as #9292, but for Nat.

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 reproducer and comparing test15, which succeeds, with test16, which reports a missing case. Trace the match-elimination path for Nat bounds and make the test16 case succeed without relying on increased maxHeartbeats or maxRecDepth; the reproducer's expected behavior defines done.