Generic VCGenM helpers: small-cap operations on MVarIds, telescope-aware simp driver, hypothesis-internalization for grind, and a residual-goal generalization of applyRflAndAndIntro. None of these know anything about SPred entailment specifically.

def Lean.Elab.Tactic.Do.Internal.Lean.Meta.Sym.BackwardRule.applyChecked (rule : Meta.Sym.BackwardRule) (goal : MVarId) (ruleDesc? : Option MessageData := none) : VCGenM Meta.Sym.ApplyResult

VCGenM wrapper around BackwardRule.apply. Behaves identically to rule.apply goal unless the application fails and Context.debug is on. In that case it retries on a fresh metavariable whose type is the unfoldReducible-normalized goal type. If the retry succeeds, an earlier step forgot a normalization; we throw a hard error pointing at the rule and the missing reduction.

ruleDesc? describes the rule for debug output. When none, the description is reconstructed from rule.expr.getAppFn — works for the common case of a constant rule. Pass a custom message for dynamically-built rules.

Designed for dot notation: rule.applyChecked goal. Requires open Lean.Elab.Tactic.Do.Internal in scope so that the dot lookup resolves.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.simpTargetTelescope (mvarId : MVarId) : VCGenM (MVarId × Bool)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.introsSimp (mvarId : MVarId) (errorMsg : MessageData) : VCGenM MVarId

Simplify the forall telescope of the target using Sym.Simp.simpTelescope, then introduce all binders via Sym.intros.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.PreTac.processHypotheses (preTac : PreTac) (goal : Meta.Grind.Goal) : VCGenM Meta.Grind.Goal

Internalize pending hypotheses into the E-graph for sharing before forking to multiple subgoals. If processHypotheses discovers a contradiction (inconsistent = true), the E-graph state contains stale proof data (the contradiction proof targets the parent's mvar, not the children's). In that case, restore the pre-internalization state so each child can discover the contradiction independently and construct its own proof via closeGoal.

Equations

• preTac.processHypotheses goal = if preTac.isGrind = true then liftM (Lean.Meta.Grind.processHypotheses goal) else pure goal

partial def Lean.Elab.Tactic.Do.Internal.VCGen.repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId)

Solves conjunctions whose leaves are True or e₁ = e₂, and returns a residual goal containing exactly the conjuncts that could not be solved. This procedure may assign metavariables in e₁/e₂, for example for e = ?m it will assign ?m := e.