diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index a021b72..3dae649 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -63,7 +63,10 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
       (List.range numFields)
     mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
-def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+def _root_.Lean.Name.isAuxLemma (n : Name) : Bool :=
+  match n with
+  | .str _ s => "_proof_".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]
diff --git a/Test/Environment.lean b/Test/Environment.lean
index 13afbfd..354473e 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -30,7 +30,6 @@ def test_symbol_visibility: IO LSpec.TestSeq := do
   let entries: List (Name × Bool) := [
     ("Nat.add_comm".toName, false),
     ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
-    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>
     let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index a3b03eb..ddd6e56 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -162,7 +162,7 @@ def test_m_couple_simp: TestM Unit := do
   checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   let unfoldedRoot ←  unfoldAuxLemmas root
   checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
-    "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   return ()
 
 def test_proposition_generation: TestM Unit := do