fix: respect explicitly inaccessible pattern variables

[cppio]

This PR changes the matcher elaboration to keep explicit inaccessible pattern variables inaccessible.

Closes #6557

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-6558 build failed against this PR. (2025-01-07 01:41:08) View Log
• ❌ Mathlib branch lean-pr-testing-6558 built against this PR, but testing failed. (2025-01-08 03:02:45) View Log

[kim-em]

@cppio, you can write a comment like changelog-language to set the changelog labels, thereby satisfying the CI failure.

[kim-em]

I pushed the required Mathlib fixes to the lean-pr-testing-6558 branch of Mathlib, and hopefully we'll now get a builds-mathlib label.

It's great when PR authors can do this step themselves too (ask me on zulip if you need write access to Mathlib branches), but also don't hesitate to ask me for help when breaks-mathlib labels appear.

[cppio]

changelog-language

[cppio]

The mathlib test failure occurs due to it relying on #6570. The following change fixes the test, but I lack the access to push it.

 def walk.map (f : α → β) (w : walk α x y) : walk β (f x) (f y) :=
-  match x, y, w with
-  | _, _, .nil n => .nil (f n)
+  match w with
+  | nil x => nil (f x)