fix: use withFreshZetaDeltaFVarIds to avoid leaking zetaDeltaFVarIds between different simp calls

src/Lean/Elab/MutualDef.lean

@@ -958,7 +958,6 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
   let letRecsToLift := letRecsToLift.toArray
   let mainFVarIds := mainFVars.map Expr.fvarId!
   let recFVarIds  := (letRecsToLift.map fun toLift => toLift.fvarId) ++ mainFVarIds
-  resetZetaDeltaFVarIds
   withTrackingZetaDelta do
     -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`.
     let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do

src/Lean/Meta/Basic.lean

@@ -681,8 +681,15 @@ def getConfig : MetaM Config :=
 def getConfigWithKey : MetaM ConfigWithKey :=
   return (← getConfig).toConfigWithKey
 
-def resetZetaDeltaFVarIds : MetaM Unit :=
-  modify fun s => { s with zetaDeltaFVarIds := {} }
+@[inline] def withFreshZetaDeltaFVarIds (x : MetaM α) : MetaM α := do
+    let fvarIdsSaved ← modifyGet fun s => (s.zetaDeltaFVarIds, { s with zetaDeltaFVarIds := {} })
+    try
+      x
+    finally
+      if (← read).trackZetaDelta then
+        modify fun s => { s with zetaDeltaFVarIds := fvarIdsSaved.union s.zetaDeltaFVarIds }
+      else
+        modify fun s => { s with zetaDeltaFVarIds := fvarIdsSaved }
 
 def getZetaDeltaFVarIds : MetaM FVarIdSet :=
   return (← get).zetaDeltaFVarIds
@@ -1117,29 +1124,29 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 -/
 @[inline] def withTrackingZetaDelta : n α → n α :=
-  mapMetaM fun x =>
+  mapMetaM fun x => withFreshZetaDeltaFVarIds <|
     withFreshCache <| withReader (fun ctx => { ctx with trackZetaDelta := true }) x
 
 /--
 `withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`.
 The cache is reset while executing `x` if `s` is not empty.
 -/
 def withZetaDeltaSet (s : FVarIdSet) : n α → n α :=
-  mapMetaM fun x =>
+  mapMetaM fun x => withFreshZetaDeltaFVarIds <|
     if s.isEmpty then
       x
     else
-      withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s }) x
+      withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := ctx.zetaDeltaSet.union s }) x
 
 /--
 Similar to `withZetaDeltaSet`, but also enables `withTrackingZetaDelta` if `s` is not empty.
 -/
 def withTrackingZetaDeltaSet (s : FVarIdSet) : n α → n α :=
-  mapMetaM fun x =>
+  mapMetaM fun x => withFreshZetaDeltaFVarIds <|
     if s.isEmpty then
       x
     else
-      withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s, trackZetaDelta := true }) x
+      withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := ctx.zetaDeltaSet.union s, trackZetaDelta := true }) x
 
 @[inline] def withoutProofIrrelevance (x : n α) : n α :=
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x

src/Lean/Meta/Closure.lean

@@ -342,7 +342,6 @@ structure MkValueTypeClosureResult where
   exprArgs    : Array Expr
 
 def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do
-  resetZetaDeltaFVarIds
   withTrackingZetaDelta do
     let type  ← collectExpr type
     let value ← collectExpr value

tests/lean/zetaDeltaFVarIdsLeakage.lean

@@ -0,0 +1,15 @@
+example : True := by
+  let a := 1
+  let b := 2
+  have : b = 2 := by simp [a,b]
+  have : a = 1 := by simp? [a]
+  have : 1 = 1 := by simp?
+  trivial
+
+axiom test_sorry {α : Sort _} : α
+
+example : False := by
+  let a := 1
+  let b := 1
+  have : a = 1 → False := test_sorry
+  simp (disch := simp [b]) [this, a]

tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out

@@ -0,0 +1,2 @@
+Try this: simp only [a]
+Try this: simp only