fix: smal fixes

Author: volodeyka

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

@@ -200,7 +200,7 @@ private def normalizePre? (scope : VCGen.Scope) (goal : MVarId) (α pre target :
   if let some (g, h) ← ofPropPreIntro? goal pre then
     return some ({ scope with lastLiftedPre? := some h }, [g])
   if let some goal' ← introsExcessArgs goal then return some (scope, [goal'])
-  if let some gs ← truePre? goal pre target then
+  if let some gs ← normalizePreToTop? goal pre target then
     return some (scope, gs)
   if let some (g, h) ← barePreIntro? goal α pre then
     return some ({ scope with lastLiftedPre? := some h }, [g])

tests/bench/mvcgen/sym/test_do_logic.lean

@@ -691,7 +691,7 @@ theorem Spec.incr
     (post : PUnit → Nat → Pred) (epost : EPred) (n : Nat) :
     Triple (fun s => post ⟨⟩ (s + n))
       (incr n : StateT Nat m PUnit) post epost := by
-  mvcgen' [WhileLoop.incr]; rfl
+  mvcgen' [TopBetaReduction.incr]; rfl
 
 /--
 error: unsolved goals
@@ -728,4 +728,4 @@ theorem incr_poly (amounts : List Nat) :
   mvcgen' [incr]
 
 
-end WhileLoop
+end TopBetaReduction