fix: realizeValue should default to the private scope (#11748)

This PR fixes an edge case where some tactics did not allow access to
private declarations inside private proofs under the module system

Fixes #11747

(cherry picked from commit f317e28)

Author: Kha

src/Lean/Meta/Basic.lean

@@ -2583,7 +2583,11 @@ where
         -- catch all exceptions
         let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
         observing do
-          realize)
+          -- The scope at which `enableRealizationsForConst forConst` was called is essentially
+          -- arbitrary, normalize here. As `realize` will not add new constants nor should it
+          -- directly be connected to user input to be checked, be permissive.
+          withoutExporting do
+            realize)
         <* addTraceAsMessages
     let res? ← act |>.run' |>.run coreCtx { env } |>.toBaseIO
     let res ← match res? with

tests/lean/run/11747.lean

@@ -0,0 +1,12 @@
+module
+
+/-! `ext_iff.2` used to fail because `getFunInfo` was operating in the public scope. -/
+
+public structure A where
+  private a : Nat
+
+theorem ext_iff {x y : A} : x = y ↔ x.a = y.a := by
+  rw [A.mk.injEq]
+
+theorem ext {x y : A} : x.a = y.a → x = y := by
+  exact ext_iff.2