From c6df4a4a8950cd7e7450646abd01db142c67c102 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Sat, 16 Aug 2025 11:40:42 +0200
Subject: [PATCH] fix: delegate to `exact` in `mvcgen using invariants` to
 avoid MVar mishaps (#9939)

This PR expands `mvcgen using invariants | $n => $t` to `mvcgen; case
inv<$n> => exact $t` to avoid MVar instantiation mishaps observable in
the test case for #9581.

Closes #9581.
---
 src/Lean/Elab/Tactic/Do/VCGen.lean | 4 ++--
 tests/lean/run/9581.lean           | 8 ++++++++
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index ec5338d29f..2af6c26022 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -362,7 +362,7 @@ where
 
 end VCGen
 
-def elabInvariants (stx : Syntax) (invariants : Array MVarId) : TermElabM Unit := do
+def elabInvariants (stx : Syntax) (invariants : Array MVarId) : TacticM Unit := do
   let some stx := stx.getOptional? | return ()
   let stx : TSyntax ``invariantAlts := ⟨stx⟩
   match stx with
@@ -381,7 +381,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) : TermElabM Unit :
           if ← mv.isAssigned then
             logErrorAt ref m!"Invariant {n} is already assigned"
             continue
-          mv.assign (← mv.withContext <| Term.elabTerm rhs (← mv.getType))
+          discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
       | _ => logErrorAt alt "Expected invariantAlt, got {alt}"
   | _ => logErrorAt stx "Expected invariantAlts, got {stx}"
 
diff --git a/tests/lean/run/9581.lean b/tests/lean/run/9581.lean
index f5c5ff909a..087acfa8d0 100644
--- a/tests/lean/run/9581.lean
+++ b/tests/lean/run/9581.lean
@@ -28,3 +28,11 @@ theorem F_spec :
   -- ⊢ (⇓x => ⌜1 < 2⌝).snd ⊢ₑ (⇓x => ⌜1 < 2⌝).snd
   · assumption
   · mleave
+
+theorem F_spec_using_with :
+   ⦃⌜True⌝⦄
+   F
+   ⦃⇓ _ => ⌜1 < 2⌝⦄ := by
+  mvcgen [F]
+  using invariants | 1 => ⇓ _ => ⌜1 < 2⌝
+  with omega