Misleading error: `match` leads to an error about `cases` where no tactic is used

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

Consider the following seemingly correct dependent pattern matching using match:

inductive LTE : (n m : Nat) → Type
  | base  : LTE 0 0
  | less  : LTE n m → LTE n       (m + l)
  | equal : LTE n m → LTE (n + l) (m + l)

open LTE

def comp_LTE (N : LTE n₁ n₂) (M : LTE n₂ n₃) : LTE n₁ n₃ :=
  match N , M with -- <-- error points [HERE]
  | N'       , base     => N'
  | N'       , less  M' => less  (comp_LTE N' M')
  | less  N' , equal M' => less  (comp_LTE N' M')
  | equal N' , equal M' => equal (comp_LTE N' M')

Running the code leads to the following misleading error message:

tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  0 = n✝.add l✝
at case @equal after processing
  _, _, _, base, _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

Notice the code does not use cases, or any tactics.

Context

I raised this issue on a Discord server (Lean 4 anarchy); the description above summarises the issue fairly well.

Steps to Reproduce

You can reproduce the error by running the code.

Expected behavior: match is a commonly used construct, and related error messages should refer to the surface language rather than the internals (e.g., cases)

Actual behavior: match leads to an error about cases

Versions

[4.12.0-nightly-2024-10-22]

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 dependent-pattern-matching example from the issue and inspect the match/dependent pattern matcher path that produces the diagnostic. Done means the same failure is reported using the surface-language term match rather than the internal tactic name cases.