The auxLemma linter #
The auxLemma linter flags explicit references to auto-generated "auxiliary" declarations
such as _proof_1, match_1, or _sizeOf_1.
Why is this bad? #
These names are internal implementation details generated by the Lean elaborator.
They are not stable across refactors (e.g. reordering fields in a structure can renumber
_proof_ indices), so depending on them makes code fragile.
The auxLemma linter emits a warning on any explicit reference to an auto-generated
auxiliary declaration (such as _proof_1, match_1, or _sizeOf_1).
These names are internal to the Lean elaborator and are not stable across refactors.