diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 5361aec984..fd0f152876 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -2176,6 +2176,8 @@ macro (name := mspecMacro) (priority:=low) "mspec" : tactic =>
 `mvcgen` will break down a Hoare triple proof goal like `⦃P⦄ prog ⦃Q⦄` into verification conditions,
 provided that all functions used in `prog` have specifications registered with `@[spec]`.
 
+### Verification Conditions and specifications
+
 A verification condition is an entailment in the stateful logic of `Std.Do.SPred`
 in which the original program `prog` no longer occurs.
 Verification conditions are introduced by the `mspec` tactic; see the `mspec` tactic for what they
@@ -2183,6 +2185,8 @@ look like.
 When there's no applicable `mspec` spec, `mvcgen` will try and rewrite an application
 `prog = f a b c` with the simp set registered via `@[spec]`.
 
+### Features
+
 When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` will additionally
 
 * add a Hoare triple specification `foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄` to `spec` set for a
@@ -2191,11 +2195,59 @@ When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` w
 * unfold any method of the `instBEqFloat : BEq Float` instance in `prog`.
 * it will no longer substitute away `let`-expressions that occur at most once in `P`, `Q` or `prog`.
 
-Furthermore, `mvcgen` tries to close trivial verification conditions by `SPred.entails.rfl` or
-the tactic sequence `try (mpure_intro; trivial)`. The variant `mvcgen_no_trivial` does not do this.
+### Config options
 
-For debugging purposes there is also `mvcgen_step 42` which will do at most 42 VC generation
-steps. This is useful for bisecting issues with the generated VCs.
+`+noLetElim` is just one config option of many. Check out `Lean.Elab.Tactic.Do.VCGen.Config` for all
+options. Of particular note is `stepLimit = some 42`, which is useful for bisecting bugs in
+`mvcgen` and tracing its execution.
+
+### Extended syntax
+
+Often, `mvcgen` will be used like this:
+```
+mvcgen [...]
+case inv1 => by exact I1
+case inv2 => by exact I2
+all_goals (mleave; try grind)
+```
+There is special syntax for this:
+```
+mvcgen [...] invariants
+· I1
+· I2
+with grind
+```
+
+### Invariant suggestions
+
+`mvcgen` will suggest invariants for you if you use the `invariants?` keyword.
+```
+mvcgen [...] invariants?
+```
+This is useful if you do not recall the exact syntax to construct invariants.
+Furthermore, it will suggest a concrete invariant encoding "this holds at the start of the loop and
+this must hold at the end of the loop" by looking at the corresponding VCs.
+Although the suggested invariant is a good starting point, it is too strong and requires users to
+interpolate it such that the inductive step can be proved. Example:
+```
+def mySum (l : List Nat) : Nat := Id.run do
+  let mut acc := 0
+  for x in l do
+    acc := acc + x
+  return acc
+
+/--
+info: Try this:
+  invariants
+    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
+-/
+#guard_msgs (info) in
+theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
+  generalize h : mySum l = r
+  apply Id.of_wp_run_eq h
+  mvcgen invariants?
+  all_goals admit
+```
 -/
 macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
   Macro.throwError "to use `mvcgen`, please include `import Std.Tactic.Do`"
diff --git a/src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean b/src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean
index 0f0d8bdee7..58fb1d5b25 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean
@@ -7,47 +7,113 @@ module
 
 prelude
 public import Lean.Elab.Tactic.Basic
+public import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Meta.Tactic.Simp.Main
 import Lean.Util.OccursCheck
+import Lean.PrettyPrinter.Delaborator
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Util.CollectFVars
 import Std.Do.Triple
 import Std.Tactic.Do -- Needed for use of `mleave` in quote
 
-public section
-
 namespace Lean.Elab.Tactic.Do
 
-open Lean Elab Tactic Meta
+open Lean Elab Tactic Meta ProofMode
 open Std.Do
 
-private def duplicateMVar (m : MVarId) : MetaM MVarId := do
-  let d ← m.getDecl
-  let e ← mkFreshExprMVarAt d.lctx d.localInstances d.type d.kind d.userName d.numScopeArgs
-  return e.mvarId!
+/--
+If the target of `vc` looks like `(H ⊢ₛ T) args`, return `H args` and `T args`.
+If the target looks like `ULift.down (T args)`, then this is likely a result of `mframe` and
+`mleave`. In this case, the last decl in the local context of `vc` will look like
+`ULift.down (H args)`. Then return `H args` and `T args`.
 
-private def eraseMacroScopesFromSyntax : Syntax → Syntax
-  | Syntax.ident info rawVal val preresolved =>
-    Syntax.ident info rawVal val.eraseMacroScopes preresolved
-  | Syntax.node info kind args =>
-    Syntax.node info kind (args.map eraseMacroScopesFromSyntax)
-  | Syntax.atom info val => Syntax.atom info val
-  | Syntax.missing => Syntax.missing
+This means that both `H args` and `T args` have type `SPred []`.
+-/
+def getSPredGoalHypsAndTarget (type : Expr) : MetaM (Option (Level × Expr × Expr)) := do
+  let args := type.getAppArgs
+  if (type.isAppOf ``Std.Tactic.Do.MGoalEntails || type.isAppOf ``SPred.entails) && args.size > 2 then
+    return (type.getAppFn.constLevels![0]!, (type.getArg! 1).beta args[3:], (type.getArg! 2).beta args[3:])
+  let some decl := (← getLCtx).lastDecl | return none
+  let hyps := decl.type.consumeMData
+  let lvl := (getULiftDownLevel type <|> getULiftDownLevel hyps).getD .zero
+  -- logWarning m!"getSPredGoalHypsAndTarget: {hyps} ⊢ₛ {type}"
+  return (lvl, toAssertion lvl hyps, toAssertion lvl type)
+where
+  getULiftDownLevel (expr : Expr) : Option Level :=
+    if expr.isAppOfArity ``ULift.down 2 then some expr.getAppFn.constLevels![0]! else none
+  toAssertion (lvl : Level) (prop : Expr) : Expr :=
+    if prop.isAppOfArity ``ULift.down 2 then
+      prop.getArg! 1
+    else
+      SPred.mkPure lvl (TypeList.mkNil lvl) prop
 
-private def eraseMacroScopesFromTSyntax (syn : TSyntax name) : TSyntax name :=
-  ⟨eraseMacroScopesFromSyntax syn.raw⟩
+structure InvariantUse where
+  /-- Index 0 is the success condition, all the others are exception conditions. -/
+  conditionIdx : Nat
+  /-- The prefix expression of the call to `Cursor.mk`. -/
+  cursorPrefix : Expr
+  /-- The suffix expression of the call to `Cursor.mk`. -/
+  cursorSuffix : Expr
+  /-- The argument expressions of the `let mut` variables. -/
+  letMuts : Array Expr
+  letMutsTuple : Expr
+  stateArgs : Array Expr
+
+inductive ClassifyInvariantUseResult where
+  | success (invariantUse : InvariantUse)
+  | notAnInvariantUse
+  | unknownInvariantUse
+
+def classifyInvariantUse (assertion : Expr) (inv : MVarId) : ClassifyInvariantUseResult := Id.run do
+  -- Looking through metadata here is important because of the name hints the proof mode leaves behind
+  let assertion := assertion.consumeMData
+  -- `assertion` looks like `?inv.2.2....1 payload args`. The number of `2`s is the condition index.
+  -- The 0 index case is the success condition case and by far the most common.
+  -- There we have `assertion = ?inv.1 payload args`.
+  -- The chain of `.2.2...1` is normalized to nested applications of `Prod.fst` and `Prod.snd`:
+  --   `@Prod.fst _ _ (@Prod.snd _ _ (@Prod.snd _ _ ... ?inv)) payload args`
+  if !assertion.isAppOf ``Prod.fst then return .notAnInvariantUse
+  let mut head := assertion.getArg! 2 -- indices 0 and 1 are type args
+  let mut conditionIdx := 0
+  while head != mkMVar inv do
+    if !head.isAppOfArity ``Prod.snd 4 then return .notAnInvariantUse -- cannot classify as a use of the invariant!
+    conditionIdx := conditionIdx + 1
+    head := head.getRevArg! 1
+  -- `head` is ?inv => Found the end of the chain.
+  -- conditionIdx is the number of `Prod.snd`s in the chain, and ?inv really is the end of the chain.
+
+  let args := assertion.getAppArgs
+  -- logWarning m!"Found Prod.fst. Args: {args}"
+  if args.size < 4 then return .notAnInvariantUse -- not an overapplication of `Prod.fst`. Types should prohibit this case
+  let payload := args[3]!
+  let stateArgs := args[4:]
+  -- `stateArgs` can be non-empty when `σs` is non-empty.
+  -- logWarning m!"Payload: {payload}"
+
+  let_expr Prod.mk _ _ cursor letMutsTuple := payload | return .unknownInvariantUse -- NB: be conservative here
+  let_expr List.Cursor.mk _α _l pref suff _prf := cursor | return .unknownInvariantUse -- dito
+  let mut acc := letMutsTuple
+  let mut letMuts := #[]
+  while acc.isAppOfArity ``MProd.mk 4 do
+    letMuts := letMuts.push (acc.getArg! 2)
+    acc := acc.getArg! 3
+  letMuts := letMuts.push acc
+  return .success { conditionIdx, cursorPrefix := pref, cursorSuffix := suff, letMuts, letMutsTuple, stateArgs }
 
 /--
-Returns `some (ρ, σ)` if `doStateTupleTy` is of the form `MProd (Option ρ) σ` and every VC in `vcs`
+Returns `some (ρ, σ)` if `letMutsTy` is of the form `MProd (Option ρ) σ` and every VC in `vcs`
 uses the `Option ρ` component according to early return semantics.
 * `ρ` is the type of early return (`Unit` in case of `break`)
 * `σ` is an `n`-ary `MProd`, carrying the current value of the `let mut` variables.
   NB: When `n=0`, we have `MProd (Option ρ) PUnit` rather than `Option ρ`.
 -/
-private def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (doStateTupleTy : Expr) : MetaM (Option (Expr × Expr)) := do
-  if !(doStateTupleTy.isAppOf ``MProd) || doStateTupleTy.getAppNumArgs < 2 then return none
-  let_expr Option ρ := doStateTupleTy.getArg! 0 | return none
-  let σ := doStateTupleTy.getArg! 1
+def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (letMutsTy : Expr) : MetaM (Option (Expr × Expr)) := do
+  if !(letMutsTy.isAppOf ``MProd) || letMutsTy.getAppNumArgs < 2 then return none
+  let_expr Option ρ := letMutsTy.getArg! 0 | return none
+  let σ := letMutsTy.getArg! 1
 
-  -- The predicate on `doStateTupleTy` above is not sufficient; after all the user might just have
+  -- The predicate on `letMutsTy` above is not sufficient; after all the user might just have
   -- introduced `let mut ret : Option α` and not use this variable according to "early return
   -- semantics", meaning that *if* `ret = some r` for some `r : ρ`, then the loop body returns
   -- `ForInStep.done (ret, ...)`. This is a property upheld by the `do` elaborator.
@@ -78,69 +144,334 @@ private def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (doStateTupleTy :
   -- Hence we check all VCs for the property above.
 
   for vc in vcs do
-    -- No point in traversing the VC if the invariant is not used in it.
-    let type ← instantiateMVars (← vc.getType)
-    if ← occursCheck inv type then continue
-    -- log m!"Looking at {vc}."
-    let some spredTarget :=
-      if type.isAppOf ``ULift.down && type.getAppNumArgs > 1 then some (type.getArg! 1)
-      else if type.isAppOf ``Std.Tactic.Do.MGoalEntails && type.getAppNumArgs > 2 then some (type.getArg! 2)
-      else if type.isAppOf ``SPred.entails && type.getAppNumArgs > 2 then some (type.getArg! 2)
-      else none
-      | continue
-    -- `spredTarget` should be an overapplication of `Prod.fst`: `spredTarget = Prod.fst ?inv payload args`
-    -- `args` can be non-empty when `σs` is non-empty.
-    if !spredTarget.isAppOf ``Prod.fst then continue
-    let args := spredTarget.getAppArgs
-    -- log m!"Found Prod.fst. Args: {args}"
-    if args.size < 4 then continue -- not an overapplication. Types should prohibit this case
-    if args[2]! != mkMVar inv then continue -- not ?inv that is applied
-    let payload := args[3]!
-    -- log m!"Payload: {payload}"
-
-    let_expr Prod.mk _ _ cursor acc := payload | return none -- NB: be conservative here
-    let_expr List.Cursor.mk _α _l _pref suff _prop := cursor | return none -- dito
+    -- logWarning m!"Looking at {vc}."
+    let type ← Expr.consumeMData <$> instantiateMVars (← vc.getType)
+    let some (_, _, spredTarget) ← vc.withContext <| getSPredGoalHypsAndTarget type | continue
+    -- logWarning m!"Found spredTarget: {spredTarget}"
+    match classifyInvariantUse spredTarget inv with
+    | .notAnInvariantUse => continue
+    | .unknownInvariantUse => return none -- conservative
+    | .success invariantUse =>
+    -- logWarning m!"Invariant use: {invariantUse.letMuts}"
     -- The following check could be smarter. Essentially it tries to construct a proof that
     -- `suff = []` or `acc = (none, _)` and returns `none` upon failure.
-    if !suff.isAppOf ``List.nil && !(acc.isAppOf ``MProd.mk && (acc.getArg! 2 |>.isAppOf ``Option.none)) then
-      -- log m!"No early return! Not a `List.nil`: {suff} and not an `Option.none`: {acc.getArg! 2}"
+    -- NB: There always is at least one `invariantUse.letMuts`.
+    if !invariantUse.cursorSuffix.isAppOf ``List.nil && !invariantUse.letMuts[0]!.isAppOf ``Option.none then
+      -- logWarning m!"No early return! Not a `List.nil`: {invariantUse.cursorSuffix} and not an `Option.none`: {invariantUse.letMuts[0]!}"
       return none
+
   return (ρ, σ)
 
+/-- Largely lifted from `Lean.MetavarContext.MkBinding.mkAuxMVarType`. -/
+def revertFVarsInTypeExcept (e : Expr) (dontRevert : FVarId → Bool) : MetaM Expr := do
+  let xs := (collectFVars {} e).fvarIds
+    |>.filter (not ∘ dontRevert)
+    |>.map mkFVar
+  let xs ← collectForwardDeps xs false
+  let lctx ← getLCtx
+  let_expr c@SPred _σs := (← inferType e) | return e
+  let lvl := c.constLevels![0]!
+  -- logWarning m!"Reverting {xs} in {e}, {lvl}"
+  let e ← xs.size.foldRevM (init := e.abstract xs) fun i _ e => do
+    let x := xs[i]
+    match lctx.getFVar! x with
+    | LocalDecl.cdecl _ _ n type bi _ =>
+      let type := type.headBeta
+      let type := type.abstractRange i xs
+      return mkApp3 (mkConst ``SPred.forall [← getLevel type, lvl]) type (TypeList.mkNil lvl) (Lean.mkLambda n bi type e)
+    | LocalDecl.ldecl (nondep := true) _ _ n type _ _ =>
+      let type := type.headBeta
+      let type := type.abstractRange i xs
+      return mkApp3 (mkConst ``SPred.forall [← getLevel type, lvl]) type (TypeList.mkNil lvl) (Lean.mkLambda n .default type e)
+    | LocalDecl.ldecl (nondep := false) _ _ n type value _ =>
+      if e.hasLooseBVar 0 then
+        let type := type.headBeta
+        let type := type.abstractRange i xs
+        let value := value.abstractRange i xs
+        return mkLet n type value e false
+      else
+        return e.lowerLooseBVars 1 1
+  return e
+
+structure SuccessPoint where
+  /-- The level of the `SPred` state tuple. -/
+  lvl : Level
+  /-- An `SPred` like `⌜xs.prefix = []⌝` or `⌜xs.suffix = []⌝`. -/
+  cursorPred : Expr
+  /-- An arbitrary `SPred` on `letMuts`. -/
+  letMutsPred : Expr
+
+def SPredNil.mkAnd (lvl : Level) (lhs rhs : Expr) : Expr :=
+  mkApp3 (mkConst ``SPred.and [lvl]) (TypeList.mkNil lvl) lhs rhs
+
+def SPredNil.mkOr (lvl : Level) (lhs rhs : Expr) : Expr :=
+  mkApp3 (mkConst ``SPred.or [lvl]) (TypeList.mkNil lvl) lhs rhs
+
+def SuccessPoint.clause (p : SuccessPoint) : Expr :=
+  SPredNil.mkAnd p.lvl p.cursorPred p.letMutsPred
+
+/-- The last syntactic element of a `FailureCond`. -/
+inductive ExceptCondsDefault where
+  /-- `()`. This means we can suggest `post⟨...⟩`. -/
+  | unit
+  /-- `ExceptConds.false`. This means we can suggest `⇓ _ => _`. -/
+  | false
+  /-- `ExceptConds.true`. This means we can suggest `⇓? _ => _`. -/
+  | true
+  /-- Something else. This means we can only suggest `by exact ⟨..., e⟩`. -/
+  | other (e : Expr)
+
+/--
+If `points[n]` is `fun e => assertion`, then the invariant should look like
+```
+post⟨... success ..., ... n except conds ..., fun e => assertion, ... other stuff ...⟩
+```
+So each entry describes a non-`False` exception condition.
+
+When the default is not defeq to `ExceptConds.false`, we use it as the default.
+-/
+structure FailureCondHints where
+  points : Array Expr := #[]
+  default : ExceptCondsDefault := .unit
+
+/-- Look at how `inv` is used in the `vcs` and collect hints about how `inv` should be instantiated.
+In case it succeeds, there will be
+* A `SuccessPoint` for the `xs.prefix = []` case
+* A `SuccessPoint` for all the `xs.suffix = []` case (control flow splits can introduce multiple
+  relevant VCs)
+* A `FailureCondHints` with the default exception condition (i.e., `FailureConds.false`, `()` or
+  something else?) and the non-defaulted exception conditions.
+-/
+def collectInvariantHints (vcs : Array MVarId) (inv : MVarId) (xs : Expr) (letMuts : Expr) : MetaM (Option (SuccessPoint × SuccessPoint × FailureCondHints)) := do
+  let lctx ← getLCtx -- this is the local context of `inv` extended by `xs` and `letMuts`
+  let mut prefixPoint? : Option SuccessPoint := none
+  let mut suffixPoint? : Option SuccessPoint := none
+  let mut failureConds : FailureCondHints := {}
+  for vc in vcs do
+    -- logWarning m!"Looking at {vc}."
+    let target ← Expr.consumeMData <$> instantiateMVars (← vc.getType)
+    if let some (lvl, spredHyps, spredTarget) ← vc.withContext <| getSPredGoalHypsAndTarget target then
+      let mkPure p := SPred.mkPure lvl (TypeList.mkNil lvl) p
+      -- vc.withContext <| logWarning m!"collectPoint: {spredHyps} ⊢ₛ {spredTarget}"
+      if let .success invariantUse := classifyInvariantUse spredTarget inv then
+        -- This is the `xs.prefix = []` case.
+        -- vc.withContext <| logWarning m!"Invariant use: {invariantUse.letMutsTuple}"
+        if invariantUse.conditionIdx != 0 then continue -- concerns the success conditions
+        if invariantUse.cursorPrefix.isAppOf ``List.nil then
+          -- eqNil := `(xs.prefix = [])
+          let xsPrefix ← mkProjection xs `prefix
+          let eqNil ← mkEq xsPrefix invariantUse.cursorPrefix
+          -- eqLetMuts := `(letMuts = $(invariantUse.letMutsTuple))
+          let eqLetMuts ← mkPure <$> mkEq letMuts invariantUse.letMutsTuple
+          -- logWarning m!"Found prefix point: {eqLetMuts}"
+          prefixPoint? := some { lvl, cursorPred := mkPure eqNil, letMutsPred := eqLetMuts }
+      if let .success invariantUse := classifyInvariantUse spredHyps inv then
+        -- This is a `xs.suffix = []` case.
+        -- vc.withContext <| logWarning m!"Found spredHyp: {spredHyps}"
+        if invariantUse.conditionIdx != 0 then continue -- concerns the success conditions
+        if invariantUse.cursorSuffix.isAppOf ``List.nil && invariantUse.letMutsTuple.isFVar then
+          let xsPrefix ← mkProjection xs `suffix
+          let eqNil ← mkEq xsPrefix invariantUse.cursorSuffix
+          let dontRevert fvarId := fvarId == invariantUse.letMutsTuple.fvarId! || lctx.contains fvarId
+          let eqLetMuts ← vc.withContext <| revertFVarsInTypeExcept spredTarget dontRevert
+          let eqLetMuts := eqLetMuts.replaceFVar invariantUse.letMutsTuple letMuts
+          -- logWarning m!"Reverted to {eqLetMuts}"
+          if let some suffixPoint := suffixPoint? then
+            suffixPoint? := some { suffixPoint with letMutsPred := SPredNil.mkAnd lvl suffixPoint.letMutsPred eqLetMuts }
+          else
+            suffixPoint? := some { lvl, cursorPred := mkPure eqNil, letMutsPred := eqLetMuts }
+    if let some (_ps, lhs, rhs) := target.app3? ``ExceptConds.entails then
+      -- This is a exception condition case.
+      -- logWarning m!"Found ExceptConds.entails: {lhs}, {rhs}"
+      -- We are targeting `Prod.snd ?inv ⊢ₑ blah` specifically
+      unless lhs.isAppOfArity ``Prod.snd 3 && lhs.getArg! 2 == mkMVar inv do continue
+      let mut n := 0
+      let mut conds := rhs
+      let mut points := #[]
+      while conds.isAppOfArity ``Prod.mk 4 do
+        points := points.push (conds.getArg! 2)
+        n := n + 1
+        conds := conds.getArg! 3
+      if points.size > failureConds.points.size then
+        -- Just overwrite the existing entry. Computing a join here is overkill for the few cases
+        -- where this is going to be used.
+        failureConds := { failureConds with points := points }
+        if conds.isConstOf ``Unit.unit then
+          failureConds := { failureConds with default := .unit }
+        else if conds.isAppOfArity ``ExceptConds.false 1 then
+          failureConds := { failureConds with default := .false }
+        else if conds.isAppOfArity ``ExceptConds.true 1 then
+          failureConds := { failureConds with default := .true }
+        else
+          failureConds := { failureConds with default := .other conds }
+      -- vc.withContext <| logWarning m!"Found failure conds: {failureConds.points.toList}"
+  return (·, ·, ·) <$> prefixPoint? <*> suffixPoint? <*> pure failureConds
+
+def duplicateMVar (m : MVarId) : MetaM MVarId := do
+  let d ← m.getDecl
+  let e ← mkFreshExprMVarAt d.lctx d.localInstances d.type d.kind d.userName d.numScopeArgs
+  return e.mvarId!
+
+/-- Remove the macro scopes introduced by quote expansion from the syntax. -/
+def eraseQuoteMacroScopesFromSyntax : Syntax → Syntax
+  | Syntax.ident info rawVal val preresolved =>
+    if rawVal.contains '@' then
+      -- This was an inaccessible name in the proof state. Its raw val looks like
+      --   "acc._@.external:file:///.../tests/lean/run/mvcgenInvariantsSuggestions.lean.2049968788._hygCtx._hyg.56"
+      -- Keep the macro scopes!
+      Syntax.ident info rawVal val preresolved
+    else
+      -- This was one of the names made inaccessible by quote expansion. Its raw val looks like
+      --   "xs"
+      -- Erase the macro scopes.
+      Syntax.ident info rawVal val.eraseMacroScopes preresolved
+  | Syntax.node info kind args =>
+    Syntax.node info kind (args.map eraseQuoteMacroScopesFromSyntax)
+  | Syntax.atom info val => Syntax.atom info val
+  | Syntax.missing => Syntax.missing
+
+/-- Remove the macro scopes introduced by quote expansion from the syntax. -/
+def eraseQuoteMacroScopesFromTSyntax (syn : TSyntax name) : TSyntax name :=
+  ⟨eraseQuoteMacroScopesFromSyntax syn.raw⟩
+
+/--
+A simple ad-hoc version of `SPred.Tactic.IsPure`, but without producing a proof and without
+involving the type class machinery.
+Example: `spred(∀x, ⌜a⌝ → let y := v; ⌜b⌝ ∧ ⌜c⌝ ∨ ⌜d⌝)` becomes `⌜∀x, a → let y := v; b ∧ c ∨ d⌝`.
+-/
+partial def tryHoistPure (e : Expr) : Expr :=
+  match go e with
+  | none => e
+  | some (lvl, e) => SPred.mkPure lvl (TypeList.mkNil lvl) e
+where
+  go (e : Expr) : Option (Level × Expr) := do
+    if e.isAppOfArity ``SPred.pure 2 then
+      return (e.getAppFn.constLevels![0]!, e.getArg! 1)
+    if let some (_, lhs, rhs) := e.app3? ``SPred.and then
+      let (_, lhs) ← go lhs
+      let (lvl, rhs) ← go rhs
+      return (lvl, mkAnd lhs rhs)
+    if let some (_, lhs, rhs) := e.app3? ``SPred.or then
+      let (_, lhs) ← go lhs
+      let (lvl, rhs) ← go rhs
+      return (lvl, mkOr lhs rhs)
+    if let some (_, _, .lam n ty body bi) := e.app3? ``SPred.forall then
+      let (lvl, body) ← go body
+      return (lvl, mkForall n bi ty body)
+    if let .letE n ty val body nondep := e then
+      let (lvl, body) ← go body
+      return (lvl, .letE n ty val body nondep)
+    failure
+
 /--
 Based on how a given metavariable `inv` binding a `Std.Do.Invariant` is used in the `vcs`, suggest
 an initial assignment for `inv` to fill in for the user.
 -/
-def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term := do
+public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term := do
   -- We only synthesize suggestions for invariant subgoals
   let invType ← instantiateMVars (← inv.getType)
-  let_expr _c@Std.Do.Invariant _α _l doStateTupleTy _ps := invType
+  let_expr c@Std.Do.Invariant α l letMutsTy _ps := invType
     | throwError "Expected invariant type, got {invType}"
+  let us := c.constLevels!
 
   -- Simplify the VCs a bit using `mleave`. Makes the job of the analysis below simpler.
   let vcs ← vcs.flatMapM fun vc =>
     try
       (·.toArray) <$> evalTacticAt (← `(tactic| mleave)) (← duplicateMVar vc)
     catch _e =>
-      -- log m!"Failed to simplify {vc}: {_e.toMessageData}"
+      -- logWarning m!"Failed to simplify {vc}: {_e.toMessageData}"
       pure #[vc]
 
   inv.withContext do
-  -- When the loop has an early return, we want to suggest an invariant using `Invariant.withEarlyReturn`.
-  if let some (_ρ, _σ) ← hasEarlyReturn vcs inv doStateTupleTy then
-    -- log m!"Found early return for {inv}!"
-    -- I tried to construct the Expr directly below, but elaborating and then delaborating `_` felt
-    -- strange; furthermore calling the delaborator felt wrong. I might resurrect this code once
-    -- the suggested invariants become deeper, though.
-    --let us := c.constLevels!
-    --withLocalDeclsDND #[(`xs, mkApp2 (mkConst ``List.Cursor us) α l), (`acc, σ)] fun _ => _
-    --let onContinue ← withLocalDeclsDND #[(`xs, mkApp2 (mkConst ``List.Cursor us) α l), (`acc, σ)] fun _ => _dunno
-    --let onReturn ← withLocalDeclsDND #[(`r, ρ), (`acc, σ)] fun _ => _dunno
-    --let onExcept := mkConst ``ExceptConds.false us
-    --let e := mkApp8 (mkConst ``Std.Do.Invariant.withEarlyReturn us) ps α l σ ρ onContinue onReturn onExcept
-    -- how to delab `e : Expr` back into a `Term` to show to the user?
-    let t ← ``(Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _))
-    -- log m!"Suggested invariant: {toString t}"
-    -- log m!"Suggested invariant: {toMessageData t}"
-    return eraseMacroScopesFromTSyntax t
-  eraseMacroScopesFromTSyntax <$> `(⇓ ⟨xs, acc⟩ => _)
+  -- Build the success points into self-contained lambdas, to be beta reduced below.
+  let suggestion? ←
+    withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
+    withLocalDeclD `letMuts letMutsTy fun letMuts => do
+    let some (prefixPoint, suffixPoint, failureConds) ← collectInvariantHints vcs inv xs letMuts | return none
+    let pred := SPredNil.mkOr prefixPoint.lvl prefixPoint.clause suffixPoint.clause
+    let success ← mkLambdaFVars #[xs, letMuts] (tryHoistPure pred)
+    let onReturn ← mkLambdaFVars #[letMuts] (tryHoistPure suffixPoint.letMutsPred)
+    return some (success, onReturn, failureConds)
+
+  -- Quotes introduce macro scopes to any binders. `eraseQuoteMacroScopesFromTSyntax` removes just
+  -- those, and will not remove any inaccessible markers stemming from inaccessible free variables
+  -- in the proof state.
+  eraseQuoteMacroScopesFromTSyntax <$> do
+  --
+  -- Finally, build the syntax for the suggestion. It's a giant configuration space mess, because
+  -- 1. Generally want to suggest something using `⇓ ⟨xs, letMuts⟩ => ...`, i.e. `PostCond.noThrow`.
+  -- 2. However, on early return we want to suggest something using `Invariant.withEarlyReturn`.
+  -- 3. When there are non-`False` failure conditions, we cannot suggest `⇓ ⟨xs, letMuts⟩ => ...`.
+  --    We might be able to suggest `⇓? ⟨xs, letMuts⟩ => ...` (`True` failure condition),
+  --    or `post⟨...⟩` (more than 0 failure handlers, but ending in `()`), and fall back to
+  --    `by exact ⟨...⟩` (not ending in `()`).
+  -- 4. Similarly for the `onExcept` argument of `Invariant.withEarlyReturn`.
+  -- Hence the spaghetti code.
+  --
+  if let some (ρ, σ) ← hasEarlyReturn vcs inv letMutsTy then
+    -- logWarning m!"Found early return for {inv}!"
+    -- Suggest an invariant using `Invariant.withEarlyReturn`.
+    if let some (success, onReturn, failureConds) := suggestion? then
+      -- First construct `onContinue` and `onReturn` clause and simplify them according to the
+      -- definition of `Invariant.withEarlyReturn`.
+      let (onContinue, onReturn) ← withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
+        withLocalDeclD `r ρ fun r =>
+        withLocalDeclD `letMuts σ fun letMuts => do
+        let onContinue := success.beta #[xs, ← mkAppM ``MProd.mk #[← mkNone ρ, letMuts]]
+        let onReturn := onReturn.beta #[← mkAppM ``MProd.mk #[← mkSome ρ r, letMuts]]
+        let ctx ← Simp.mkContext
+          (config := {})
+          (simpTheorems := #[(← Meta.getSimpTheorems)])
+          (congrTheorems := (← Meta.getSimpCongrTheorems))
+        let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
+        let (res1, _) ← Lean.Meta.simp onContinue ctx simprocs
+        let (res2, _) ← Lean.Meta.simp onReturn ctx simprocs
+        return (← Lean.PrettyPrinter.delab res1.expr, ← Lean.PrettyPrinter.delab res2.expr)
+      -- Now the configuration mess.
+      if failureConds.points.isEmpty then
+        match failureConds.default with
+        | .false | .unit =>
+          `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue))
+        -- we handle the following two cases here rather than through
+        -- `postCondWithMultipleConditions` below because that would insert a superfluous `by exact _`.
+        | .true =>
+          `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := ExceptConds.true)))
+        | .other e =>
+          `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := $(← Lean.PrettyPrinter.delab e))))
+      else -- need the postcondition long form as `onExcept` arg
+        let mut terms : Array Term := #[]
+        for point in failureConds.points do
+          terms := terms.push (← Lean.PrettyPrinter.delab point)
+        let onExcept ← postCondWithMultipleConditions terms failureConds.default
+        `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue) (onExcept := $onExcept))
+    else -- No suggestion. Just fill in `_`.
+      `(Invariant.withEarlyReturn (onReturn := fun r letMuts => _) (onContinue := fun xs letMuts => _))
+  else if let some (success, _, failureConds) := suggestion? then
+    -- No early return, but we do have a suggestion.
+    withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
+    withLocalDeclD `letMuts letMutsTy fun letMuts => do
+    let successBody ← Lean.PrettyPrinter.delab (success.beta #[xs, letMuts])
+    -- Configuration mess
+    if failureConds.points.isEmpty && not (failureConds.default matches .other _) then
+      if (failureConds.default matches .true) then
+        `(⇓? ⟨xs, letMuts⟩ => $successBody)
+      else
+        `(⇓ ⟨xs, letMuts⟩ => $successBody)
+    else -- need the long form
+      let mut terms : Array Term := #[← `(fun ⟨xs, letMuts⟩ => $successBody)]
+      for point in failureConds.points do
+        terms := terms.push (← Lean.PrettyPrinter.delab point)
+      postCondWithMultipleConditions terms failureConds.default
+  else
+    -- No early return and no suggestion. Just suggest _something_.
+    -- `PostCond.noThrow` is the most common case.
+    `(⇓ ⟨xs, letMuts⟩ => _)
+where
+  postCondWithMultipleConditions (handlers : Array Term) (default : ExceptCondsDefault) : MetaM Term := do
+    let handlers := Syntax.TSepArray.ofElems (sep := ",") handlers
+    match default with
+    | .unit => `(post⟨$handlers,*⟩)
+    -- See the comment in `post⟨_⟩` syntax for why we emit `by exact` here.
+    | .false => `(by exact ⟨$handlers,*, ExceptConds.false⟩)
+    | .true => `(by exact ⟨$handlers,*, ExceptConds.true⟩)
+    | .other e => `(by exact ⟨$handlers,*, $(← Lean.PrettyPrinter.delab e)⟩)
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index cb36aef8b5..3c7a398d34 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -359,16 +359,3 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 syntax (name := mvcgen) "mvcgen" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
   (invariantAlts)? (vcAlts)? : tactic
-
-/--
-Like `mvcgen`, but does not attempt to prove trivial VCs via `mpure_intro; trivial`.
--/
-syntax (name := mvcgenNoTrivial) "mvcgen_no_trivial" optConfig
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
-
-/--
-Like `mvcgen_no_trivial`, but `mvcgen_step 42` will only do 42 steps of the VC generation procedure.
-This is helpful for bisecting bugs in `mvcgen` and tracing its execution.
--/
-syntax (name := mvcgenStep) "mvcgen_step" optConfig
- (num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
diff --git a/tests/lean/run/mvcgenInvariantsSuggestions.lean b/tests/lean/run/mvcgenInvariantsSuggestions.lean
index a5c8dcaab7..d98dda2fb3 100644
--- a/tests/lean/run/mvcgenInvariantsSuggestions.lean
+++ b/tests/lean/run/mvcgenInvariantsSuggestions.lean
@@ -5,6 +5,8 @@ open Std Do
 
 set_option grind.warning false
 set_option mvcgen.warning false
+set_option pp.rawOnError true
+set_option warn.sorry false
 
 def mySum (l : List Nat) : Nat := Id.run do
   let mut acc := 0
@@ -15,7 +17,7 @@ def mySum (l : List Nat) : Nat := Id.run do
 /--
 info: Try this:
   invariants
-    · ⇓⟨xs, acc⟩ => _
+    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
 -/
 #guard_msgs (info) in
 theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
@@ -24,6 +26,49 @@ theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
   mvcgen invariants?
   all_goals admit
 
+def mySum2 (l : List Nat) : Nat := Id.run do
+  let mut acc := 0
+  let mut acc2 := 0
+  for x in l do
+    acc := acc + x
+    acc2 := acc2 + x
+  return acc
+
+/--
+info: Try this:
+  invariants
+    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = ⟨0, 0⟩ ∨ xs.suffix = [] ∧ letMuts.fst = l.sum⌝
+-/
+#guard_msgs (info) in
+theorem mySum2_suggest_invariant (l : List Nat) : mySum2 l = l.sum := by
+  generalize h : mySum2 l = r
+  apply Id.of_wp_run_eq h
+  mvcgen invariants?
+  all_goals admit
+
+def copy (l : List Nat) : Id (Array Nat) := do
+  let mut acc := #[]
+  for x in l do
+    acc := acc.push x
+  return acc
+
+/--
+info: Try this:
+  invariants
+    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts = l.toArray⌝
+-/
+#guard_msgs (info) in
+theorem copy_suggest_invariant (l : List Nat) : ⦃⌜True⌝⦄ copy l ⦃⇓ r => ⌜r = l.toArray⌝⦄ := by
+  mvcgen [copy] invariants?
+  /-
+  case inv1
+  l : List Nat
+  acc✝ : Array Nat := #[]
+  ⊢ Invariant l (Array Nat) PostShape.pure
+  ...
+  -/
+  all_goals admit
+
 def nodup (l : List Int) : Bool := Id.run do
   let mut seen : HashSet Int := ∅
   for x in l do
@@ -35,7 +80,9 @@ def nodup (l : List Int) : Bool := Id.run do
 /--
 info: Try this:
   invariants
-    · Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
+    ·
+      Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
+        (onContinue := fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
 -/
 #guard_msgs (info) in
 theorem nodup_suggest_invariant (l : List Int) : nodup l ↔ l.Nodup := by
@@ -60,8 +107,18 @@ def nodup_twice (l : List Int) : Bool := Id.run do
 /--
 info: Try this:
   invariants
-    · Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
-    · Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
+    ·
+      Invariant.withEarlyReturn (onReturn := fun r letMuts =>
+        spred(Prod.fst ?inv2 ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, ∅⟩) ∧
+            { down := r = true ↔ l.Nodup }))
+        (onContinue := fun xs letMuts =>
+        spred({ down := xs.prefix = [] ∧ letMuts = ∅ } ∨
+            ⌜xs.suffix = []⌝ ∧
+              Prod.fst ?inv2 ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, ∅⟩) ∧
+                { down := True }))
+    ·
+      Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
+        (onContinue := fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
 -/
 #guard_msgs (info) in
 theorem nodup_twice_suggest_invariant (l : List Int) : nodup_twice l ↔ l.Nodup := by
@@ -70,7 +127,6 @@ theorem nodup_twice_suggest_invariant (l : List Int) : nodup_twice l ↔ l.Nodup
   mvcgen invariants?
   all_goals admit
 
-
 structure Supply where
   counter : Nat
 
@@ -89,10 +145,11 @@ def mkFreshN (n : Nat) : AppM (List Nat) := do
     acc := acc.push n
   return acc.toList
 
+-- In the following, we suggest an inaccessible variable `acc` in the invariant. Unfortunate.
 /--
 info: Try this:
   invariants
-    · ⇓⟨xs, acc⟩ => _
+    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts.toList.Nodup⌝
 -/
 #guard_msgs (info) in
 theorem mkFreshN_suggest_invariant (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
@@ -110,7 +167,10 @@ def mkFreshN_early_return (n : Nat) : AppM (List Nat) := do
 /--
 info: Try this:
   invariants
-    · Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
+    ·
+      Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜letMuts.toList.Nodup ∧ r.Nodup⌝)
+        (onContinue := fun xs letMuts =>
+        ⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts.toList.Nodup⌝)
 -/
 #guard_msgs (info) in
 theorem mkFreshN_early_return_suggest_invariant (n : Nat) : ⦃⌜True⌝⦄ mkFreshN_early_return n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
@@ -125,7 +185,9 @@ def earlyReturnWithoutLetMut (l : List Int) : Bool := Id.run do
 /--
 info: Try this:
   invariants
-    · Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
+    ·
+      Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜r = true⌝) (onContinue :=
+        fun xs letMuts => ⌜xs.prefix = [] ∨ xs.suffix = []⌝)
 -/
 #guard_msgs (info) in
 theorem earlyReturnWithoutLetMut_suggest_invariant (l : List Int) : earlyReturnWithoutLetMut l := by
@@ -147,7 +209,8 @@ def notQuiteEarlyReturn (l : List Nat) : Option Nat := Id.run do
 /--
 info: Try this:
   invariants
-    · ⇓⟨xs, acc⟩ => _
+    · ⇓⟨xs, letMuts⟩ =>
+      ⌜xs.prefix = [] ∧ letMuts = ⟨none, ()⟩ ∨ xs.suffix = [] ∧ letMuts.fst = l.getLast?⌝
 -/
 #guard_msgs (info) in
 theorem notQuiteEarlyReturn_suggest_invariant (l : List Nat) : notQuiteEarlyReturn l = l.getLast? := by
@@ -156,23 +219,124 @@ theorem notQuiteEarlyReturn_suggest_invariant (l : List Nat) : notQuiteEarlyRetu
   mvcgen invariants?
   all_goals admit
 
-def polyMonad [Monad m] (l : List Nat) : m (Option Nat) := do
-  -- The idea here is that the type of the state tuple *looks* like it's an early return, but `last`
-  -- is not used as if it is an early return variable. Specifically, `last` is set without breaking
-  -- out of the loop.
-  let mut last : Option Nat := none
-  let mut mdummy : Unit := () -- m* is important because let mut vars are sorted alphabetically
+def polySum [Monad m] (l : List Nat) : m Nat := do
+  let mut acc := 0
+  let mut acc2 := 0
   for x in l do
-    last := some x
-    mdummy := ()
-  return last
+    acc := acc + x
+    acc2 := acc2 + x
+  return acc
 
 /--
 info: Try this:
   invariants
-    · ⇓⟨xs, acc⟩ => _
+    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = ⟨0, 0⟩ ∨ xs.suffix = [] ∧ letMuts.fst = l.sum⌝
 -/
 #guard_msgs (info) in
-theorem polyMonad_suggest_invariant [Monad m] [WPMonad m ps] (l : List Nat) : ⦃⌜True⌝⦄ @polyMonad m _ l ⦃⇓ r => ⌜True⌝⦄ := by
-  mvcgen [polyMonad] invariants?
+theorem polySum_suggest_invariant [Monad m] [WPMonad m ps] (l : List Nat) : ⦃⌜True⌝⦄ @polySum m _ l ⦃⇓ r => ⌜r = l.sum⌝⦄ := by
+  mvcgen [polySum] invariants?
   all_goals admit
+
+def polyNodup [Monad m] (l : List Int) : m Bool := do
+  let mut seen : HashSet Int := ∅
+  for x in l do
+    if x ∈ seen then
+      return false
+    seen := seen.insert x
+  return true
+
+/--
+info: Try this:
+  invariants
+    ·
+      Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
+        (onContinue := fun xs letMuts =>
+        ⌜xs.prefix = [] ∧ letMuts = seen✝ ∨ xs.suffix = [] ∧ l.Nodup⌝)
+-/
+#guard_msgs (info) in
+theorem polyNodup_suggest_invariant [Monad m] [WPMonad m ps] (l : List Int) : ⦃⌜True⌝⦄ @polyNodup m _ l ⦃⇓r => ⌜r ↔ l.Nodup⌝⦄ := by
+  mvcgen [polyNodup] invariants?
+  all_goals admit
+
+def fast_expo (x n : Nat) : Nat := Id.run do
+  let mut x := x
+  let mut y := 1
+  let mut e := n
+  for _ in [:n] do -- simulating a while loop running at most n times
+    if e = 0 then break
+    if e % 2 = 1 then
+      y := x * y
+      e := e - 1
+    else
+      x := x*x
+      e := e/2
+
+  return y
+
+open Std.Do
+
+/--
+info: Try this:
+  invariants
+    · ⇓⟨xs, letMuts⟩ =>
+      ⌜xs.prefix = [] ∧ letMuts = ⟨n, x, 1⟩ ∨ xs.suffix = [] ∧ letMuts.2.snd = x ^ n⌝
+-/
+#guard_msgs (info) in
+theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
+  generalize h : fast_expo x n = r
+  apply Id.of_wp_run_eq h
+  mvcgen invariants?
+  all_goals admit
+
+namespace FreshBounded
+
+structure Supply where
+  counter : Nat
+  limit : Nat
+  property : counter ≤ limit
+
+def mkFresh : EStateM String Supply Nat := do
+  let supply ← get
+  if h : supply.counter = supply.limit then
+    throw s!"Supply exhausted: {supply.counter} = {supply.limit}"
+  else
+    let n := supply.counter
+    have := supply.property
+    set {supply with counter := n + 1, property := by omega}
+    pure n
+
+def mkFreshN (n : Nat) : ExceptT Char (EStateM String Supply) (List Nat) := do
+  let mut acc := #[]
+  for _ in [:n] do
+    acc := acc.push (← mkFresh)
+  pure acc.toList
+
+@[spec]
+theorem mkFresh_spec (c : Nat) :
+    ⦃fun state => ⌜state.counter = c⌝⦄
+    mkFresh
+    ⦃post⟨fun r state => ⌜r = c ∧ c < state.counter⌝, fun _msg state => ⌜c = state.counter ∧ c = state.limit⌝⟩⦄ := by
+  mvcgen [mkFresh]
+  all_goals grind
+
+/--
+info: Try this:
+  invariants
+    ·
+      post⟨fun ⟨xs, letMuts⟩ =>
+        ⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts.toList.Nodup⌝, fun x => ⌜False⌝,
+        fun _msg state => ⌜state.counter = state.limit⌝⟩
+-/
+#guard_msgs (info) in
+theorem mkFreshN_spec (n : Nat) :
+    ⦃⌜True⌝⦄
+    mkFreshN n
+    ⦃post⟨fun r => ⌜r.Nodup⌝, fun _ => ⌜False⌝, fun _msg state => ⌜state.counter = state.limit⌝⟩⦄ := by
+  mvcgen [mkFreshN] invariants?
+  -- The full invariant is:
+  -- · post⟨fun ⟨xs, acc⟩ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝,
+  --        fun _ => ⌜False⌝,
+  --        fun _msg state => ⌜state.counter = state.limit⌝⟩
+  all_goals admit
+
+end FreshBounded