diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 5f346bd00eca..c6b96141d9b2 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/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
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index b54ca0e2ebb6..002f15cf214e 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/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,7 +1124,7 @@ 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
 
 /--
@@ -1125,21 +1132,21 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 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
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 6aa6578055d4..ec27f7db4666 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/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
diff --git a/tests/lean/zetaDeltaFVarIdsLeakage.lean b/tests/lean/zetaDeltaFVarIdsLeakage.lean
new file mode 100644
index 000000000000..7c8987f0de4f
--- /dev/null
+++ b/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]
diff --git a/tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out b/tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out
new file mode 100644
index 000000000000..2a3b2e617694
--- /dev/null
+++ b/tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out
@@ -0,0 +1,2 @@
+Try this: simp only [a]
+Try this: simp only