From d131cf39c1eea72d782edad81da67ef524fda62a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 18 Jun 2025 16:19:37 +0900
Subject: [PATCH] fix: set public aux decl prefix in `init_grind_norm` (#8856)

This PR ensures simp theorems generated by `init_grind_norm` are
accessible in other `module`s
---
 src/Lean/Elab/Tactic/Grind.lean | 5 ++++-
 stage0/src/stdlib_flags.h       | 2 ++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index a9f2ef9ed2..1d8a8ba502 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -50,7 +50,10 @@ def elabInitGrindNorm : CommandElab := fun stx =>
     Command.liftTermElabM do
       let pre ← pre.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
       let post ← post.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
-      Grind.registerNormTheorems pre post
+      -- Creates `Lean.Grind._simp_1` etc.. As we do not use this command in independent modules,
+      -- there is no chance of name conflicts.
+      withDeclNameForAuxNaming `Lean.Grind do
+        Grind.registerNormTheorems pre post
   | _ => throwUnsupportedSyntax
 
 def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) : MetaM Grind.Params := do
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..1bbdca66f7 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear bot, please update stage 0
+
 namespace lean {
 options get_default_options() {
     options opts;