diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 29af0ea2e1..6bedad5ea8 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/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
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 026e534b50..a74061c69b 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/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
diff --git a/tests/elab/12897.lean b/tests/elab/12897.lean
index 6582787bcc..7a7718f9f8 100644
--- a/tests/elab/12897.lean
+++ b/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
diff --git a/tests/elab/13043.lean b/tests/elab/13043.lean
new file mode 100644
index 0000000000..bcadc1e9e2
--- /dev/null
+++ b/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