fix: missing pushScope and popScope

src/Lean/Elab/Tactic/Basic.lean

@@ -328,9 +328,13 @@ private def getOptRotation (stx : Syntax) : Nat :=
   setGoals <| (← getGoals).rotateRight n
 
 @[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do
-  let openDecls ← elabOpenDecl stx[1]
-  withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
-    evalTactic stx[3]
+  try
+    pushScope
+    let openDecls ← elabOpenDecl stx[1]
+    withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
+      evalTactic stx[3]
+  finally
+    popScope
 
 @[builtinTactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[2]

src/Lean/Elab/Term.lean

@@ -1421,9 +1421,13 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
 
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
-  let openDecls ← elabOpenDecl stx[1]
-  withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
-    elabTerm stx[3] expectedType?
+  try
+    pushScope
+    let openDecls ← elabOpenDecl stx[1]
+    withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
+      elabTerm stx[3] expectedType?
+  finally
+    popScope
 
 @[builtinTermElab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[2]

src/Lean/ScopedEnvExtension.lean

@@ -180,7 +180,7 @@ def ScopedEnvExtension.modifyState (ext : ScopedEnvExtension α β σ) (env : En
   let s := ext.ext.getState env
   match s.stateStack with
   | top :: stack => ext.ext.setState env { s with stateStack := { top with state := f top.state } :: stack }
-  | _ => env  
+  | _ => env
 
 def pushScope [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit := do
   for ext in (← scopedEnvExtensionsRef.get) do

tests/lean/run/openInScopeBug.lean

@@ -0,0 +1,32 @@
+constant f : Nat → Nat
+constant g : Nat → Nat
+
+namespace Foo
+
+@[scoped simp] axiom ax1 (x : Nat) : f (g x) = x
+@[scoped simp] axiom ax2 (x : Nat) : g (g x) = g x
+
+end Foo
+
+theorem ex1 : f (g (g (g x))) = x := by
+  simp -- does not use ax1 and ax2
+  simp [Foo.ax1, Foo.ax2]
+
+theorem ex2 : f (g (g (g x))) = x :=
+  have h₁ : f (g (g (g x))) = f (g x) by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
+  have h₂ : f (g x) = x               by simp; open Foo in simp
+  Eq.trans h₁ h₂
+  -- open Foo in simp -- works
+
+theorem ex3 : f (g (g (g x))) = x := by
+  simp
+  simp [Foo.ax1, Foo.ax2]
+
+open Foo in
+theorem ex4 : f (g (g (g x))) = x := by
+  simp
+
+theorem ex5 : f (g (g (g x))) = x ∧ f (g x) = x := by
+  apply And.intro
+  { simp; open Foo in simp }
+  { simp; open Foo in simp }