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