fix: use declName? pattern for normalizeInstance meta marking

The previous fix (#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.

Switch to the existing `declName?` pattern (already used by `unsafe`
and `private_decl%`), which 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 aux defs are also marked meta
- `deriving`: `declName?` reflects the actual meta status of the
  declaration being elaborated, avoiding the mismatch

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