Cannot declare `let rec`s within the RHS of a multi-pattern-match arm

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

When attempting to declare a let rec in the body of a pattern-match arm that matches on multiple patterns simultaneously, the elaborator attempts to declare the let rec repeatedly in each desugared match arm, which fails because the duplicate declarations conflict with each other.

Context

This was discovered while debugging #6927, not "organically" during general use.

Steps to Reproduce

Consider the following code:

def foo (xs : List Nat) :=
  match xs with
  | [x] | [x, _] =>
    let rec y := x  -- error: 'foo.y' has already been declared
    y
  | _ => 0

def bar : List Nat → Nat
  | [x] | [x, _] =>
    let rec y := x  -- error: 'bar.y' has already been declared
    y
  | _ => 0

Expected behavior: The definitions compile.

Actual behavior: The definitions fail to compile with the error indicated above.

Versions

Lean 4.18.0-nightly-2025-03-03
Target: x86_64-unknown-linux-gnu

Impact

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

Start by compiling the two minimal examples in the issue on Lean 4.18.0-nightly-2025-03-03 and reproduce the duplicate-declaration error. Investigate the elaborator's handling of multi-pattern-match arms and their desugaring of the RHS; done means both foo and bar compile with the shown let rec bindings.