From 66772d77fc886566cf913883bc22b552a9e5df2c Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Mon, 11 Aug 2025 08:40:19 +0200
Subject: [PATCH] fix: Work around a DefEq bug in `mspec` involving delayed
 assignments (#9833)

This PR works around a DefEq bug in `mspec` involving delayed
assignments.
---
 src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean | 7 +++++++
 src/Lean/Elab/Tactic/Do/Spec.lean           | 7 ++++++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
index 40c47d02a8..4926dc58d3 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
@@ -9,6 +9,7 @@ prelude
 public import Std.Tactic.Do.Syntax
 public import Lean.Elab.Tactic.Do.ProofMode.MGoal
 public import Lean.Elab.Tactic.Do.ProofMode.Focus
+public import Lean.Elab.Tactic.Meta
 
 public section
 
@@ -53,3 +54,9 @@ def elabMPure : Tactic
   | _ => throwUnsupportedSyntax
 
 macro "mpure_intro" : tactic => `(tactic| apply Pure.intro)
+
+def MGoal.triviallyPure (goal : MGoal) : OptionT MetaM Expr := do
+  let mv ← mkFreshExprMVar goal.toExpr
+  let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply Pure.intro; trivial)) catch _ => failure
+    | failure
+  return mv.consumeMData
diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean
index c7fc8c4beb..bfe8200a71 100644
--- a/src/Lean/Elab/Tactic/Do/Spec.lean
+++ b/src/Lean/Elab/Tactic/Do/Spec.lean
@@ -126,7 +126,12 @@ def dischargeMGoal (goal : MGoal) (goalTag : Name) : n Expr := do
   -- The `withDefault` ensures that a hyp `⌜s = 4⌝` can be used to discharge `⌜s = 4⌝ s`.
   -- (Recall that `⌜s = 4⌝ s` is `SVal.curry (σs:=[Nat]) (fun _ => s = 4) s` and `SVal.curry` is
   -- semi-reducible.)
-  let some prf ← liftMetaM (withDefault <| goal.assumption <|> goal.assumptionPure)
+  -- We also try `mpure_intro; trivial` through `goal.triviallyPure` here because later on an
+  -- assignment like `⌜s = ?c⌝` becomes impossible to discharge because `?c` will get abstracted
+  -- over local bindings that depend on synthetic opaque MVars (such as loop invariants), and then
+  -- the type of the new `?c` will not be defeq to itself. A bug, but we need to work around it for
+  -- now.
+  let some prf ← liftMetaM (withDefault <| goal.assumption <|> goal.assumptionPure <|> goal.triviallyPure)
     | mkFreshExprSyntheticOpaqueMVar goal.toExpr goalTag
   liftMetaM <| do trace[Elab.Tactic.Do.spec] "proof: {prf}"
   return prf