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

@@ -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}"
 

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