From f3ac38ff2cbfa3c0233c3280c3dc1c4207ca305c Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Mon, 21 Jul 2025 12:12:34 +0200
Subject: [PATCH] fix: Close pure, trivial goals in `mvcgen` (#9362) (#9447)

This PR ensures that `mvcgen` not only tries to close stateful subgoals
by assumption, but also pure Lean goals.

Closes #9362.
---
 src/Lean/Elab/Tactic/Do/VCGen.lean |  2 +-
 tests/lean/run/9362.lean           | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/9362.lean

diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index c02705271d..5309c40305 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -409,5 +409,5 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- but optConfig is not a leading_parser, and neither is the syntax for `lemmas`
   let ctx ← mkSpecContext stx[1] stx[2]
   let vcs ← genVCs (← getMainGoal) ctx (fuel := .unlimited)
-  let tac ← `(tactic| try (apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); trivial))
+  let tac ← `(tactic| try ((try apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro)); trivial))
   for vc in vcs do discard <| runTactic vc tac
diff --git a/tests/lean/run/9362.lean b/tests/lean/run/9362.lean
new file mode 100644
index 0000000000..e938cd2ce7
--- /dev/null
+++ b/tests/lean/run/9362.lean
@@ -0,0 +1,20 @@
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+axiom G (lt : Nat) : Id Unit
+
+noncomputable def F : Id Unit := do
+  G 1
+
+axiom P : Prop
+
+@[spec]
+axiom G_spec (h : P) :
+   ⦃⌜True⌝⦄ G 1 ⦃⇓ _ => ⌜0 < 1⌝⦄
+
+theorem F_spec (h : P) :
+   ⦃⌜True⌝⦄ F ⦃⇓ _ => ⌜0 < 1⌝⦄ := by
+  mvcgen [F] -- should close (h : P ⊢ P) by trivial