Commit 2026-05-28 11:17 a953f2ee

feat(Tactic/Linter): add auxLemma linter for auto-generated declaration references (#37364) This PR adds a syntax linter that flags explicit references to auto-generated auxiliary declarations such as _proof_N, match_N, _sizeOf_N or _aux_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: https://github.com/leanprover-community/mathlib-ci/pull/17 🤖 Prepared with Claude Code