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

@@ -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

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;