perf: instantiate only the entailment sides in mvcgen' solve (#14072)

This PR avoids re-instantiating the whole `solve` target on every
iteration of `mvcgen'` VC generation, with no change in behaviour. A
rule application only ever leaves a metavariable-application head on the
two sides of the entailment (for instance a lattice-split operand), so
`solve` instantiates just those sides for its shape tests instead of
running `instantiateMVars` over the full target on every step;
`elimTopPre` instantiates the precondition it inspects.

Stacked on #14071.

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.lean

@@ -91,7 +91,7 @@ where the reduction is sound; entailments at an abstract lattice carrier pass th
 public def elimTopPre (goal : MVarId) : VCGenM MVarId := do
   let some (.sort .zero, _, pre, _) := (← goal.getType).app4? ``Lean.Order.PartialOrder.rel
     | return goal
-  unless pre.isAppOf ``Lean.Order.top do return goal
+  unless (← instantiateMVarsIfMVarApp pre).isAppOf ``Lean.Order.top do return goal
   let .goals [goal] ← (← read).backwardRules.elimPre.apply goal
     | throwError "Failed to strip the `⊤ ⊑` wrapper of {goal}"
   return goal

src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean

@@ -351,16 +351,9 @@ The function performs the following steps in order:
 -/
 public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   if ← outOfFuel then return .stop .outOfFuel
-  let mut goal := goal
-  let mut target ← goal.getType
+  let target ← goal.getType
   trace[Elab.Tactic.Do.vcgen] "🎯 Target: {target}"
 
-  if target.hasExprMVar then
-    -- Rule application may have assigned metavariables in the target; re-normalise so the
-    -- syntactic shape tests below see the assigned form.
-    target ← instantiateMVars target
-    goal ← goal.replaceTargetDefEq target
-
   -- Phase 1: simplify `target` until it is of the form `pre ⊑ rhs`.
   if let some gs ← forallIntro? goal target then return .goals scope gs
   if let some g ← targetLetIntro? goal target then return .goals scope [g]
@@ -371,6 +364,12 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
   let_expr PartialOrder.rel α inst pre rhs := target
     | return .stop (.noEntailment target)
 
+  -- A previous rule application may have assigned the entailment's sides to fresh metavariables
+  -- (e.g. a lattice-split operand). Instantiate those heads so the shape tests below see the
+  -- assigned form.
+  let pre ← instantiateMVarsIfMVarApp pre
+  let rhs ← instantiateMVarsIfMVarApp rhs
+
   -- Phase 2: close reflexive goals, then drive `pre` toward `⊤`, lifting any pure content so a
   -- later spec application sees a `⊤` precondition.
   if let some gs ← rfl? goal then return .goals scope gs