diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index c7cef17018..29af0ea2e1 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -329,7 +329,8 @@ 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))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
+    let isMeta := (← read).isMetaSection
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 327741d088..1b9bd26385 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -666,7 +666,8 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
   return {
     macroStack             := ctx.macroStack
     sectionVars            := sectionVars
-    isNoncomputableSection := scope.isNoncomputable }
+    isNoncomputableSection := scope.isNoncomputable
+    isMetaSection          := scope.isMeta }
 
 /--
 Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 9e339d7302..026e534b50 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -220,10 +220,12 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
+            let isMeta := (← read).isMetaSection
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
+                  (isMeta := isMeta)
             else
               pure result.instVal
             let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index 7fde3bc80a..d33ff9cf32 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/src/Lean/Elab/Term/TermElabM.lean
@@ -309,6 +309,8 @@ structure Context where
   heedElabAsElim     : Bool            := true
   /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
+  /-- `true` when inside a `meta section`. -/
+  isMetaSection : Bool                 := false
   /-- When `true` we skip TC failures. We use this option when processing patterns. -/
   ignoreTCFailures : Bool := false
   /-- `true` when elaborating patterns. It affects how we elaborate named holes. -/
diff --git a/src/Lean/Meta/InstanceNormalForm.lean b/src/Lean/Meta/InstanceNormalForm.lean
index 20fefdd6d9..86d53c3851 100644
--- a/src/Lean/Meta/InstanceNormalForm.lean
+++ b/src/Lean/Meta/InstanceNormalForm.lean
@@ -99,7 +99,7 @@ Normalize an instance value to "instance normal form".
 See the module docstring for the full algorithm specification.
 -/
 partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
-    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
+    (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.instanceNormalForm
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
@@ -124,9 +124,11 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             return inst
           else
             let name ← mkAuxDeclName
-            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
-              (logCompileErrors := logCompileErrors)
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
             setReducibilityStatus name .implicitReducible
+            if isMeta then modifyEnv (markMeta · name)
+            if compile then
+              compileDecls (logErrors := logCompileErrors) #[name]
             enableRealizationsForConst name
             return wrapped
         else
@@ -169,7 +171,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             catch _ => pure ()
 
           mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
-            (logCompileErrors := logCompileErrors))
+            (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.
           if backward.inferInstanceAs.wrap.data.get (← getOptions) then
@@ -180,6 +182,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
               let name ← mkAuxDeclName
               mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
               setInlineAttribute name
+              if isMeta then modifyEnv (markMeta · name)
               if compile then
                 compileDecls (logErrors := logCompileErrors) #[name]
               enableRealizationsForConst name
diff --git a/tests/elab/12897.lean b/tests/elab/12897.lean
new file mode 100644
index 0000000000..6582787bcc
--- /dev/null
+++ b/tests/elab/12897.lean
@@ -0,0 +1,12 @@
+-- Tests that `inferInstanceAs` auxiliary definitions are properly marked `meta`
+-- when used inside a `meta` section.
+
+module
+
+meta section
+
+def Foo := List Nat
+
+instance : EmptyCollection Foo := inferInstanceAs (EmptyCollection (List Nat))
+
+end