diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index 2a175654b9..0152545733 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -478,3 +478,12 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}"
   replaceMainGoal (invariants ++ vcs).toList
   -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}"
+
+@[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
+def elabMVCGenHint : Tactic := fun stx => withMainContext do
+  let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
+    |>.setKind ``Lean.Parser.Tactic.mvcgen
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+  -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
+  -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
+  Lean.Meta.Tactic.TryThis.addSuggestion stx stx'
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index 268c72cbac..cdd0b5f7cd 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -365,5 +365,11 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 
 @[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
   (invariantAlts)? (vcAlts)? : tactic
+
+/--
+A hint tactic that expands to `mvcgen invariants?`.
+-/
+syntax (name := mvcgenHint) "mvcgen?" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")? : tactic
diff --git a/tests/lean/run/mvcgenInvariantsSuggestions.lean b/tests/lean/run/mvcgenInvariantsSuggestions.lean
index 6e3dccf3a5..49188979d9 100644
--- a/tests/lean/run/mvcgenInvariantsSuggestions.lean
+++ b/tests/lean/run/mvcgenInvariantsSuggestions.lean
@@ -26,6 +26,29 @@ theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
   mvcgen invariants?
   all_goals admit
 
+/--
+info: Try this:
+  [apply] mvcgen invariants?
+---
+info: Try this:
+  [apply] mvcgen [mySum] invariants?
+---
+info: Try this:
+  [apply] mvcgen +elimLets invariants?
+---
+info: Try this:
+  [apply] mvcgen +elimLets [mySum] invariants?
+-/
+#guard_msgs (info) in
+theorem mySum_suggest_invariant_short (l : List Nat) : mySum l = l.sum := by
+  generalize h : mySum l = r
+  apply Id.of_wp_run_eq h
+  mvcgen?
+  mvcgen? [mySum]
+  mvcgen? +elimLets
+  mvcgen? +elimLets [mySum]
+  all_goals admit
+
 def mySum2 (l : List Nat) : Nat := Id.run do
   let mut acc := 0
   let mut acc2 := 0