Using rcase/case tactic for recursive proofs when all arguments is variable cause an unexpected 'unknown identifier' error

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

namespace Working

variable {α : Type u} (as bs cs : List α)

theorem append_assoc (as : List α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
  rcases as with _ | ⟨a, as⟩
  . repeat rw [List.nil_append]
  . repeat rw [List.cons_append]
    apply congrArg
    rw [append_assoc]

end Working

namespace NotWorking

variable {α : Type u} (as bs cs : List α)

theorem append_assoc : as ++ bs ++ cs = as ++ (bs ++ cs) := by
  rcases as with _ | ⟨a, as⟩
  . repeat rw [List.nil_append]
  . repeat rw [List.cons_append]
    apply congrArg
    rw [append_assoc] -- Error: unknown identifier 'append_assoc'

end NotWorking

The code in NotWorking namespace is not working, it report an unknown identifier 'append_assoc' error.

But the code in Working namespace does working. The only difference is the as argument in Working namespace is an explicit argument, not from variable syntax.

Context

Zulip topic: #new members > unknown identifier if all args is defined in variable syntax

Steps to Reproduce

1. Test the the code above locally or in online playground.

Expected behavior: Code in NotWorking also working as it has no semantic difference with Working one.

Actual behavior: The code in NotWorking namespace is not working, it report an unknown identifier 'append_assoc' error.

Versions

4.20.0-nightly-2025-05-10

Additional Information

N/A

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 Working and NotWorking examples in the issue against the reported nightly version. Investigate how recursive theorem names are resolved when arguments come from variable syntax versus explicit binders; done means both examples elaborate without the unknown identifier error.