fix: restore ambient exporting scope in mkAuxDefinition

src/Lean/Meta/Closure.lean

@@ -432,14 +432,13 @@ end Closure
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false)
-    (compile : Bool := true) (logCompileErrors : Bool := true) (exposeBody : Bool := true) :
-    MetaM Expr := do
+    (compile : Bool := true) (logCompileErrors : Bool := true) : MetaM Expr := do
   let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
   let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
   let decl := Declaration.defnDecl (← mkDefinitionValInferringUnsafe name result.levelParams.toList
     result.type result.value  hints)
-  withExporting (isExporting := exposeBody) <| addDecl decl
+  addDecl decl
   if compile then
     compileDecl decl (logErrors := logCompileErrors)
   return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs

src/Lean/Meta/WrapInstance.lean

@@ -183,8 +183,8 @@ where go (inst expectedType : Expr) (isEta : Bool) : MetaM (Option Expr) := do
 
         if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
           let name ← mkAuxDeclName
-          let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
-            (exposeBody := exposeAux)
+          let wrapped ← withoutExporting (when := !exposeAux) <|
+            mkAuxDefinition name expectedType inst (compile := false)
           setReducibilityStatus name <|
             if (← withImplicit <| isDefEq expectedType instType) then
               .implicitReducible
@@ -279,8 +279,8 @@ where go (inst expectedType : Expr) (isEta : Bool) : MetaM (Option Expr) := do
             mvarId.assign arg
           else
             let name ← mkAuxDeclName
-            mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false)
-              (exposeBody := exposeAux))
+            mvarId.assign (← withoutExporting (when := !exposeAux) <|
+              mkAuxDefinition name argExpectedType arg (compile := false))
             setReducibilityStatus name <|
               if (← withImplicit <| isDefEq argExpectedType argType) then
                 .implicitReducible

tests/elab/privateDeclExpose.lean

@@ -0,0 +1,22 @@
+module
+
+/-! Term `private` should create unexposed bodies regardless of context. -/
+
+def privVal : Nat := 5
+
+@[expose] public def pubVal : Nat := private_decl% privVal
+
+/--
+info: @[expose] def pubVal : Nat :=
+pubVal._private_1
+-/
+#guard_msgs in
+#print pubVal
+
+-- The aux def must not be `@[expose]`: its body references the private `privVal`.
+/--
+info: def pubVal._private_1 : Nat :=
+privVal
+-/
+#guard_msgs in
+#print pubVal._private_1