From 737fd607e81a33fa73e748dd316ca506d4779d90 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 2 Jul 2025 14:54:13 -0700
Subject: [PATCH] refactor: Add heuristic case to `isAuxLemma`

---
 Pantograph/Delate.lean      | 9 +++++----
 Pantograph/Environment.lean | 2 +-
 Test/Metavar.lean           | 2 +-
 Test/Serial.lean            | 4 ++--
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 8f7c1cd..cecf758 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -63,15 +63,16 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
       (List.range numFields)
     mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
-def _root_.Lean.Name.isAuxLemma (n : Name) : Bool :=
+def isAuxLemma (n : Name) : Bool :=
   match n with
-  | .str _ s => "_proof_".isPrefixOf s
+  -- `mkAuxLemma` generally allows for arbitrary prefixes but these are the ones produced by core.
+  | .str _ s => "_proof_".isPrefixOf s || "_simp_".isPrefixOf s
   | _ => false
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
 @[export pantograph_unfold_aux_lemmas_m]
-def unfoldAuxLemmas : Expr → CoreM Expr :=
-  (Meta.deltaExpand · Lean.Name.isAuxLemma)
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
+  Meta.deltaExpand e isAuxLemma
 /-- Unfold all matcher applications -/
 @[export pantograph_unfold_matchers_m]
 def unfoldMatchers (expr : Expr) : CoreM Expr :=
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index f52e7d2..1184850 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -14,7 +14,7 @@ namespace Pantograph.Environment
 @[export pantograph_is_name_internal]
 def isNameInternal (n: Name): Bool :=
   -- Returns true if the name is an implementation detail which should not be shown to the user.
-  n.isAuxLemma ∨ n.hasMacroScopes
+  isAuxLemma n ∨ n.hasMacroScopes
 
 /-- Catalog all the non-internal and safe names -/
 @[export pantograph_environment_catalog]
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 0d6f399..f3bcda3 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -303,7 +303,7 @@ def test_replay_environment : TestM Unit := do
   let stateT ← state2.replay state state1
   checkEq "(stateT goals)" stateT.goals.length 0
   let .some root := stateT.rootExpr? | fail "Root expression must exist"
-  checkTrue "root has aux lemma" $ root.getUsedConstants.any (·.isAuxLemma)
+  checkTrue "root has aux lemma" $ root.getUsedConstants.any isAuxLemma
   checkEq "(root)" (toString $ ← Meta.ppExpr root) "⟨_proof_1, _proof_2⟩"
   let root ← unfoldAuxLemmas root
   checkEq "(root unfold)" (toString $ ← Meta.ppExpr root) "⟨sorry, sorry⟩"
diff --git a/Test/Serial.lean b/Test/Serial.lean
index cca7dbd..e627853 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -87,12 +87,12 @@ def test_pickling_env_extensions : TestM Unit := do
       pure type
     let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable!
     let parentExpr := state1.parentExpr!
-    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
+    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any isAuxLemma
     goalStatePickle state1 statePath
   let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
     let (state1, _) ← goalStateUnpickle statePath (← getEnv)
     let parentExpr := state1.parentExpr!
-    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
+    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any isAuxLemma
 
   return ()