Entailment-shaped goal decomposition for pre ⊑ rhs targets: unfolding Triple, introducing excess state arguments and pure preconditions, reducing exception-postcondition projections, and decomposing lattice connectives.

def Lean.Elab.Tactic.Do.Internal.VCGen.unfoldTriple (goal : MVarId) : VCGenM MVarId

Unfold ⦃P⦄ x ⦃Q; E⦄ into the underlying entailment P ⊑ wp x Q E.

def Lean.Elab.Tactic.Do.Internal.VCGen.introPre (rule : Meta.Sym.BackwardRule) (goal : MVarId) : VCGenM (MVarId × FVarId)

Apply precondition-intro rule rule to goal, then introduce the freed hypothesis, leaving ⊤ as the residual precondition. Returns the new goal and the introduced hypothesis.

def Lean.Elab.Tactic.Do.Internal.VCGen.reduceEPostHead? (goal : MVarId) (target α inst pre rhs : Expr) : VCGenM (Option MVarId)

Reduce an EPost.Cons.head projection on the RHS of pre ⊑ rhs to the underlying component: concrete epost⟨…⟩ values project to the selected component, and ⊥.head x₁ … xₙ rewrites to ⊥ via replaceEPostHeadBot?. Returns none if the RHS is not such a projection.

def Lean.Elab.Tactic.Do.Internal.VCGen.splitLatticeOp? (goal : MVarId) (rhs : Expr) : VCGenM (Option (List MVarId))

Decompose a supported lattice connective (⊓, ⇨, ⌜p⌝, ⊤, iInf) or a registered frame operator on the RHS of pre ⊑ rhs by saturating it with the built-in and @[frameproc] rewrites, closing it with a terminal, and point-framing any excess state arguments. Returns none if the head is neither a built-in connective nor a frame operator, or its rule does not apply.

An embedded proposition ⌜p⌝ is decomposed only when the precondition is ⊤: its ⊤-fixed terminal top_le_ofProp fails to apply otherwise, since turning pre ⊑ ⌜p⌝ into the subgoal p drops pre.

def Lean.Elab.Tactic.Do.Internal.VCGen.splitForallLe? (goal : MVarId) (rhs : Expr) : VCGenM (Option (List MVarId))

Decompose a ∀/→ on the RHS of pre ⊑ (∀ x, q x) via le_forall.

def Lean.Elab.Tactic.Do.Internal.VCGen.reduceTopAppliedPre? (goal : MVarId) (target pre : Expr) : Meta.Sym.SymM (Option MVarId)

Reduce a precondition that is the bare top applied to the state arguments introduced by le_of_forall_le, (⊤ : σ₁ → … → σₙ → Prop) s₁ … sₙ, to the bare (⊤ : Prop), rewriting goal's target pre ⊑ rhs to ⊤ ⊑ rhs. The equation pre = ⊤ is built on demand by folding Lean.Order.top_apply over the excess arguments (mirroring replaceEPostHeadBot?'s bot_apply fold) and applied with replaceTargetEq.

The proof term is built directly with mkApp/mkConst and instances extracted from pre, avoiding mkAppM/instance synthesis (both expensive and unable to unify max-of-universe-variable instance levels in the abstract-monad setting). Returns none if pre is not the bare top applied to ≥ 1 argument, or its lattice instances are not in the expected instCompleteLatticePi shape (the caller then falls through).

def Lean.Elab.Tactic.Do.Internal.VCGen.elimTopPre (goal : MVarId) : VCGenM MVarId

Reduce a Prop-lattice goal (⊤ : Prop) ⊑ φ to the bare proposition φ via top_le_prop, returning any other goal unchanged. The match on Sort 0 keeps it to the Prop base lattice, where the reduction is sound; entailments at an abstract lattice carrier pass through.