fix: use declName? pattern for normalizeInstance meta marking (#13059)

This PR switches `normalizeInstance` from using `isMetaSection` to the
existing `declName?` pattern (already used by `unsafe` in
`BuiltinNotation.lean` and `private_decl%` in `BuiltinTerm.lean`) for
determining whether aux defs should be marked `meta`.

#13043 used `isMetaSection` to determine whether `normalizeInstance` aux
defs should be marked `meta`. This caused `deriving` in meta sections to
fail: the deriving handler doesn't mark the instance itself as meta, so
the non-meta instance couldn't access its meta-marked aux defs:

```
Invalid definition `instInhabitedLibraryNote`, may not access declaration
`instInhabitedLibraryNote._aux_1` marked as `meta`
```

The `declName?` pattern inherits meta status from the parent declaration
rather than the scope. This correctly handles both cases:
- **`inferInstanceAs`**: parent declaration is marked meta by
`processHeaders`, so `declName?.any (isMarkedMeta env)` is true and aux
defs are correctly marked meta
- **`deriving`**: `declName?` is `none` (the deriving handler runs
outside `withDeclName`), so `isMeta` is `false` and aux defs are not
marked meta — matching the instance itself, which the deriving handler
also does not mark meta

Found while adapting Batteries to nightly-2026-03-23.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Elab/BuiltinTerm.lean

@@ -329,7 +329,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    let isMeta := (← read).isMetaSection
+    let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
     withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst

src/Lean/Elab/Deriving/Basic.lean

@@ -220,7 +220,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).isMetaSection
+            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType

tests/elab/12897.lean

@@ -1,12 +1,25 @@
--- Tests that `inferInstanceAs` auxiliary definitions are properly marked `meta`
--- when used inside a `meta` section.
+-- Tests that `normalizeInstance` auxiliary definitions work correctly
+-- when used inside a `meta` section, for both `inferInstanceAs` and `deriving`.
 
 module
 
-meta section
+public meta import Lean.Elab.Command
 
-def Foo := List Nat
+public meta section
 
-instance : EmptyCollection Foo := inferInstanceAs (EmptyCollection (List Nat))
+namespace Test
 
-end
+open Lean
+
+-- `@[expose]` forces `normalizeInstance` to create aux wrapper definitions,
+-- which is where the meta marking matters.
+@[expose] def Foo := Unit
+deriving Inhabited
+
+@[expose] def Bar := Name
+deriving Inhabited
+
+@[expose] def Baz := List Nat
+instance : EmptyCollection Baz := inferInstanceAs (EmptyCollection (List Nat))
+
+end Test

tests/elab/13043.lean

@@ -0,0 +1,20 @@
+-- Tests that `deriving` instances inside a `meta section` are properly marked `meta`.
+-- Regression test for https://github.com/leanprover/lean4/pull/13043
+
+module
+
+public meta import Lean.Elab.Command
+
+public meta section
+
+namespace Test
+
+open Lean
+
+@[expose] def Foo := Unit
+deriving Inhabited
+
+@[expose] def Bar := Name
+deriving Inhabited
+
+end Test