def Lean.Elab.Tactic.Do.suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term

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.