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.