feat(Tactic/Linter): add auxLemma linter for auto-generated declaration references

[kim-em]

This PR adds a syntax linter that flags explicit references to auto-generated auxiliary declarations such as _proof_N, match_N, _match_N, and _sizeOf_N. These names are internal to the Lean elaborator and are not stable across refactors (e.g. reordering fields in a structure can renumber _proof_ indices).

The linter matches precisely: it requires the suffix after the prefix to be all digits, so _proof_helper would not be flagged. It only inspects identifier syntax nodes, so references in comments and docstrings are ignored.

Current hits in Mathlib (suppressed with set_option linter.style.auxLemma false):

• Mathlib/CategoryTheory/Functor/Category.lean — hcomp._proof_2
• Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean — constFormalMultilinearSeries.match_1.eq_2
• Mathlib/Data/List/Sigma.lean — _sizeOf_1

Companion PR to track these suppressions in the tech debt report: leanprover-community/mathlib-ci#17

🤖 Prepared with Claude Code

[github-actions]

PR summary 9036ce5439

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 7884 files with changed transitive imports taking up over 342404 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff

+ auxLemmaLinter
+ isAuxName
+ matchesAuxPattern
+ nameRefersToAuxLemma

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[thorimur]

Ah, this is great! :) These comments are mostly minor (style and naming), but I also extended what counts as autogenerated.

[thorimur]

!bench

[leanprover-radar]

Benchmark results for 5896be2 against 00fca21 are in. Significant changes detected! @thorimur

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

• 🟥 main exited with code 1

No significant changes detected.

[thorimur]

Hmm, maybe if you merge master, the bench will succeed. Let's try again after master is merged + the changes are applied.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[thorimur]

!bench

[leanprover-radar]

Benchmark results for 8261284 against 9036ce5 are in. No significant results found. @thorimur

• 🟥 build//instructions: +260.5G (+0.15%)

Small changes (1🟥)

• 🟥 build/module/Mathlib.Tactic.Linarith//instructions: +272.3M (+6.39%)

[grunweg]

Thanks for writing this!

Can we have a test for the linter itself? Right now, if Lean's naming scheme for auto-generated declarations would change, the linter could stop doing what it's supposed to do and we wouldn't notice.