Generic VCGenM helpers: checked backward-rule application, telescope-aware simp driver, hygienic binder introduction, hypothesis-internalization for grind, and the trivial-conjunct collapser solveTrivialConjuncts. None of these know anything about the entailment shapes solve decomposes.

def Lean.MVarId.replaceTargetDefEqFast (goal : MVarId) (targetNew : Expr) : MetaM MVarId

Change goal's Prop-typed target to the definitionally-equal targetNew, mirroring the goal update in Sym.Simp: a fresh synthetic-opaque goal cast back through @id. Unlike MVarId.replaceTargetDefEq it skips the instantiateMVars/Expr.equal round-trip, so it neither detects a no-op change nor supports a non-Prop target; the caller must pass a genuinely different targetNew definitionally equal to the current target.

Equations

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

def Lean.Meta.Sym.BackwardRule.shareCommon (rule : BackwardRule) : SymM BackwardRule

Internalize a backward rule's pattern into the current SymM share table. See Pattern.shareCommon. Designed for dot notation: rule.shareCommon.

Equations

• rule.shareCommon = do let __do_lift ← rule.pattern.shareCommon pure { expr := rule.expr, pattern := __do_lift, resultPos := rule.resultPos }

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.processHypotheses (goal : Meta.Grind.Goal) : VCGenM Meta.Grind.Goal

Grind.processHypotheses if Context.internalize is true, otherwise a no-op.

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.processHypotheses goal = do let __do_lift ← read if __do_lift.internalize = true then liftM (Lean.Meta.Grind.processHypotheses goal) else pure goal

def Lean.Elab.Tactic.Do.Internal.VCGen.introsHygienic (goal : MVarId) (overrides : Array Name := #[]) : VCGenM MVarId

Introduce all leading binders of goal in one pass, naming the i-th binder overrides[i] when given and the binder's own name otherwise. Accessibility is decided by tactic.hygienic via mkFreshBinderNameForTactic. The introduction itself is a single Sym.intros call (which keeps the memoized, sharing-correct intro); only the names are chosen here. Returns the goal unchanged when there are no leading binders.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.simpGoalTelescope (goal : MVarId) : VCGenM Meta.Sym.SimpGoalResult

Simplify the goal's target with the configured hypothesis simp methods (a no-op without Context.hypSimpMethods), threading the persistent simp cache through VCGenM's state. .noProgress is forwarded to the caller.

Equations

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

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

Introduce the excess state arguments of an entailment goal pre ⊑ rhs whose lattice type is a function type σ₁ → … → σₙ → α: repeatedly apply stateArgIntro (a backward rule for Lean.Order.le_of_forall_le) and introduce the new state binder, until the lattice type is no longer a function type. Returns none when the carrier is not a function type (nothing to introduce); throws when the carrier is a function type that le_of_forall_le cannot peel, such as a dependent function lattice (a : α) → β a → ….

partial def Lean.Elab.Tactic.Do.Internal.VCGen.solveTrivialConjuncts (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.