Pattern matching on Fin n breaks exhaustivity for n > 15

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

Pattern matching on numbers of Fin n breaks down for n > 15.

Context

def toBase16 : Fin 16 -> Char
| 0 => '0' | 1 => '1'
| 2 => '2' | 3 => '3'
| 4 => '4' | 5 => '5'
| 6 => '6' | 7 => '7'
| 8 => '8' | 9 => '9'
| 10 => 'A' | 11 => 'B'
| 12 => 'C' | 13 => 'D'
| 14 => 'E' | 15 => 'F'

Steps to Reproduce

Run the above code on Lean Nightly.

Actual behavior: The following error message occurs, despite all cases being covered:

Missing cases:
(Fin.mk (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 _)))))))))))))))) _)

Expected behavior: The code should compile. For reference, all of the following code compiles without issue:

def toBase2 : Fin 2 -> Char
| 0 => '0' | 1 => '1'

def toBase10 : Fin 10 -> Char
| 0 => '0' | 1 => '1'
| 2 => '2' | 3 => '3'
| 4 => '4' | 5 => '5'
| 6 => '6' | 7 => '7'
| 8 => '8' | 9 => '9'

def toBase15 : Fin 15 -> Char
| 0 => '0' | 1 => '1'
| 2 => '2' | 3 => '3'
| 4 => '4' | 5 => '5'
| 6 => '6' | 7 => '7'
| 8 => '8' | 9 => '9'
| 10 => 'A' | 11 => 'B'
| 12 => 'C' | 13 => 'D'
| 14 => 'E'

Versions

Lean 4.22.0-rc3

Start with the minimal Fin 16 pattern-matching example in the issue and run it against Lean nightly, then compare it with the compiling Fin 15 and Fin 10 examples. The fix is done when the Fin 16 definition compiles without a false missing-cases error and exhaustivity checking remains correct.