chore: realization of private def should run in private scope (#11618)

In fact the scope should be solely determined by the def name but this
breaks some existing realizer, so postponed.

src/Lean/Meta/Basic.lean

@@ -2673,7 +2673,8 @@ where
         let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
         observing do
           withDeclNameForAuxNaming constName do
-            realize
+            withoutExporting (when := isPrivateName constName) do
+              realize
           -- Meta code working on a non-exported declaration should usually do so inside
           -- `withoutExporting` but we're lenient here in case this call is the only one that needs
           -- the setting.