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

Mathlib.lean

@@ -7081,6 +7081,7 @@ public import Mathlib.Tactic.LinearCombination
 public import Mathlib.Tactic.LinearCombination'
 public import Mathlib.Tactic.LinearCombination.Lemmas
 public import Mathlib.Tactic.Linter
+public import Mathlib.Tactic.Linter.AuxLemma
 public import Mathlib.Tactic.Linter.CommandRanges
 public import Mathlib.Tactic.Linter.CommandStart
 public import Mathlib.Tactic.Linter.DeprecatedModule

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -380,6 +380,7 @@ theorem constFormalMultilinearSeries_apply_of_nonzero [NontriviallyNormedField 
     {n : ℕ} (hn : n ≠ 0) : constFormalMultilinearSeries 𝕜 E c n = 0 :=
   Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn
 
+set_option linter.auxLemma false in
 @[simp]
 lemma constFormalMultilinearSeries_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
     [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] :

Mathlib/CategoryTheory/Functor/Category.lean

@@ -113,6 +113,7 @@ def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ H ⟶ G ⋙ I wh
 
 -- Horizontal composition has two possible definitions that are dual to each other,
 -- and we need to prove to `to_dual` that these are equivalent.
+set_option linter.auxLemma false in
 attribute [to_dual none] hcomp._proof_2 hcomp._proof_3
 to_dual_insert_cast hcomp := by ext x; exact β.naturality' (α.app x)
 

Mathlib/Data/List/Sigma.lean

@@ -547,6 +547,7 @@ theorem kerase_comm (a₁ a₂) (l : List (Sigma β)) :
       else by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]
     else by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]
 
+set_option linter.auxLemma false in
 theorem sizeOf_kerase [SizeOf (Sigma β)] (x : α)
     (xs : List (Sigma β)) : SizeOf.sizeOf (List.kerase x xs) ≤ SizeOf.sizeOf xs := by
   simp only [SizeOf.sizeOf, _sizeOf_1]
@@ -646,6 +647,7 @@ theorem dlookup_dedupKeys (a : α) (l : List (Sigma β)) : dlookup a (dedupKeys
     · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
       exact h
 
+set_option linter.auxLemma false in
 theorem sizeOf_dedupKeys [SizeOf (Sigma β)]
     (xs : List (Sigma β)) : SizeOf.sizeOf (dedupKeys xs) ≤ SizeOf.sizeOf xs := by
   simp only [SizeOf.sizeOf, _sizeOf_1]

Mathlib/Init.lean

@@ -4,6 +4,7 @@ public import Lean.Linter.Sets -- for the definition of linter sets
 public import Lean.LibrarySuggestions.Default -- for `+suggestions` modes in tactics
 public import Mathlib.Lean.Linter -- linter utilities; will be transitively imported in #31134
 public import Mathlib.Tactic.Lemma
+public import Mathlib.Tactic.Linter.AuxLemma
 public import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 public import Mathlib.Tactic.Linter.DirectoryDependency
 public import Mathlib.Tactic.Linter.DocPrime
@@ -82,6 +83,7 @@ all these linters, or add the `weak.linter.mathlibStandardSet` option to their l
 register_linter_set linter.mathlibStandardSet :=
   -- linter.allScriptsDocumented -- disabled, let's not impose this requirement downstream.
   -- linter.checkInitImports -- disabled, not relevant downstream.
+  linter.auxLemma
   linter.flexible
   linter.hashCommand
   linter.oldObtain
@@ -126,7 +128,7 @@ register_linter_set linter.weeklyLintSet :=
   linter.tacticAnalysis.verifyGrindOnly
 
 -- Check that all linter options mentioned in the mathlib standard linter set exist.
-open Lean Elab.Command Linter Mathlib.Linter Style UnusedInstancesInType
+open Lean Elab.Command Linter Mathlib.Linter Style UnusedInstancesInType AuxLemma
 
 run_cmd liftTermElabM do
   let DefinedInScripts : Array Name :=

Mathlib/Tactic.lean

@@ -158,6 +158,7 @@ public import Mathlib.Tactic.LinearCombination
 public import Mathlib.Tactic.LinearCombination'
 public import Mathlib.Tactic.LinearCombination.Lemmas
 public import Mathlib.Tactic.Linter
+public import Mathlib.Tactic.Linter.AuxLemma
 public import Mathlib.Tactic.Linter.CommandRanges
 public import Mathlib.Tactic.Linter.CommandStart
 public import Mathlib.Tactic.Linter.DeprecatedModule

Mathlib/Tactic/Linter/AuxLemma.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public meta import Lean.Elab.Command
+public meta import Mathlib.Tactic.Linter.Header  -- shake: keep
+
+/-!
+# 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.
+-/
+
+meta section
+
+open Lean Elab Linter
+
+namespace Mathlib.Linter.AuxLemma
+
+/-- Returns `true` if `s` has the form `pfx ++ digits`, e.g. `"_proof_17"`. -/
+@[inline] private def matchesAuxPattern (pfx : String) (s : String) : Bool :=
+  s.startsWith pfx && (s.drop pfx.length).all (·.isDigit) && s.rawEndPos > pfx.rawEndPos
+
+/-- Returns `true` if `s` is an auto-generated auxiliary name component,
+such as `_proof_1`, `match_2`, or `_sizeOf_3`. -/
+private def isAuxName (s : String) : Bool :=
+  matchesAuxPattern "_proof_" s ||
+  matchesAuxPattern "match_" s ||
+  matchesAuxPattern "_match_" s ||
+  matchesAuxPattern "_sizeOf_" s ||
+  matchesAuxPattern "grind_" s ||
+  matchesAuxPattern "_simp_" s ||
+  matchesAuxPattern "_gcongr_" s ||
+  matchesAuxPattern "_aux_" s
+
+/-- Returns `true` if any component of the name is an auto-generated auxiliary name. -/
+private def nameRefersToAuxLemma : Name → Bool
+  | .str p s => isAuxName s || nameRefersToAuxLemma p
+  | .num p _ => nameRefersToAuxLemma p
+  | .anonymous => false
+
+/-- 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. -/
+public register_option linter.auxLemma : Bool := {
+  defValue := true
+  descr := "enable the `auxLemma` linter"
+}
+
+@[inherit_doc linter.auxLemma]
+def auxLemmaLinter : Linter where run := withSetOptionIn fun stx => do
+    unless getLinterValue linter.auxLemma (← getLinterOptions) do
+      return
+    if ← MonadLog.hasErrors then
+      return
+    if let some id := stx.find? fun s => s.isIdent && nameRefersToAuxLemma s.getId then
+      logLint linter.auxLemma id
+        m!"`{id.getId}` refers to an auto-generated auxiliary declaration. \
+          These are not stable across refactors; consider using a different approach."
+
+initialize addLinter auxLemmaLinter
+
+end Mathlib.Linter.AuxLemma

MathlibTest/CompileInductive.lean

@@ -21,6 +21,7 @@ example := @Nat.brecOn
 example := @List.brecOn
 example := @Fin2.brecOn
 
+set_option linter.auxLemma false in
 example := @List._sizeOf_1
 
 open Lean Elab Term

MathlibTest/interactiveUnfold.lean

@@ -122,6 +122,7 @@ variable {α : Type} [Group α] (a : α) in
 -- The proof `aux._proof_1` is an implementation detail. It should not be a problem if
 -- that appears in the expression, as long as it appears inside an implicit argument.
 def aux {α : Type} [Semiring α] := (3 : α)
+set_option linter.auxLemma false in
 /--
 info: Unfolds for 3 + 3:
 · Nat.add 3 3

MathlibTest/toAdditive.lean

@@ -769,11 +769,13 @@ def Subtype.mul_inv_iff_mul_inv {α β : Type} [Group α] [MyRing β] (a : α) (
   exists a
   simp
 
+set_option linter.auxLemma false in
 /--
 info: Subtype.mul_inv_iff_mul_inv._proof_1 {α β : Type} [Group α] [MyRing β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1
 -/
 #guard_msgs in
 #check Subtype.mul_inv_iff_mul_inv._proof_1
+set_option linter.auxLemma false in
 /--
 info: Subtype.add_neg_iff_mul_inv._proof_1 {α β : Type} [AddGroup α] [MyRing β] (a : α) (b : β) : a + -a = 0 ↔ b * b⁻¹ = 1
 -/