fix: reduce through lets in mvcgen main loop (#10453)

This PR makes `mvcgen` reduce through `let`s, so that it progresses over
`(have t := 42; fun _ => foo t) 23` by reduction to `have t := 42; foo
t` and then introducing `t`.

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -181,6 +181,10 @@ partial def reduceProjBeta? (e : Expr) : MetaM (Option Expr) :=
           let e' := mkAppRev f' rargs
           go (some e') e'.getAppFn e'.getAppRevArgs
         | none    => pure lastReduction
+      | .letE x ty val body nondep =>
+        match ← go none body rargs with
+        | none => pure lastReduction
+        | some body' => pure (some (.letE x ty val body' nondep))
       | _ => pure lastReduction
 
 def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do

tests/lean/run/mvcgenTutorial.lean

@@ -115,6 +115,11 @@ def mkFreshN (n : Nat) : AppM (List Nat) := do
     acc := acc.push n
   return acc.toList
 
+theorem mkFreshN_spec_noncompositional (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
+  mvcgen [mkFreshN, mkFresh, liftCounterM]
+  case inv1 => exact ⇓⟨xs, acc⟩ _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝
+  all_goals mleave; grind
+
 @[spec]
 theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) :
     ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh (m := m) ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by