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

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

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