fix: unfold auxiliary theorems created by decreasing_tactic

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -90,11 +90,13 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
     let packedArgType := type.bindingDomain!
     let wfRel ← elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf?
     trace[Elab.definition.wf] "wfRel: {wfRel}"
-    withoutModifyingEnv do
+    let (value, envNew) ← withoutModifyingEnv' do
       addAsAxiom unaryPreDef
       let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
-      let value ← eraseRecAppSyntaxExpr value
-      return { unaryPreDef with value }
+      eraseRecAppSyntaxExpr value
+    /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
+    let value ← unfoldDeclsFrom envNew value
+    return { unaryPreDef with value }
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
   addNonRec preDefNonRec

src/Lean/Meta/Transform.lean

@@ -122,5 +122,25 @@ def zetaReduce (e : Expr) : MetaM Expr := do
     | e => if e.hasFVar then return TransformStep.visit e else return TransformStep.done e
   liftM (m := CoreM) <| Core.transform e (pre := pre)
 
+/-- Unfold definitions and theorems in `e` that are not in the current environment, but are in `biggerEnv`. -/
+def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
+  withoutModifyingEnv do
+    let env ← getEnv
+    setEnv biggerEnv -- `e` has declarations from `biggerEnv` that are not in `env`
+    let pre (e : Expr) : CoreM TransformStep := do
+      match e with
+      | Expr.const declName us .. =>
+        if env.contains declName then
+          return TransformStep.done e
+        else if let some info := biggerEnv.find? declName then
+          if info.hasValue then
+            return TransformStep.visit (info.instantiateValueLevelParams us)
+          else
+            return TransformStep.done e
+        else
+          return TransformStep.done e
+      | _ => return TransformStep.visit e
+    Core.transform e (pre := pre)
+
 end Meta
 end Lean

src/Lean/MonadEnv.lean

@@ -31,6 +31,15 @@ def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
   let env ← getEnv
   try x finally setEnv env
 
+/-- Similar to `withoutModifyingEnv`, but also returns the updated environment -/
+@[inline] def withoutModifyingEnv' [Monad m] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m (α × Environment) := do
+  let env ← getEnv
+  try
+    let a ← x
+    return (a, ← getEnv)
+  finally
+    setEnv env
+
 @[inline] def matchConst [Monad m] [MonadEnv m] (e : Expr) (failK : Unit → m α) (k : ConstantInfo → List Level → m α) : m α := do
   match e with
   | Expr.const constName us _ => do

tests/lean/run/decreasingTacticUpdatedEnvIssue.lean

@@ -0,0 +1,24 @@
+def g (x : Nat) (b : Bool) :=
+  if b then
+    x - 1
+  else
+    x + 1
+
+theorem g_eq (x : Nat) (h : ¬ x = 0) : g x (x > 0) = x - 1 ∧ g x false = x + 1 := by
+  have : x > 0 := by match x with
+    | 0 => contradiction
+    | x+1 => apply Nat.zero_lt_succ
+  simp [g, this]
+
+macro_rules
+| `(tactic| decreasing_tactic) =>
+ `(tactic|
+   (simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel, g_eq, *]
+    apply Nat.pred_lt; assumption))
+
+def f (x : Nat) : Nat :=
+  if h : x = 0 then
+    1
+  else
+    f (g x (x > 0)) + 2
+termination_by f x => x