diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index 932da9683a..eb52a249a6 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -262,6 +262,8 @@ where
     let f := T.getAppFn
     if f.isLambda then
       return ← onLambda goal name
+    if f.isLet then
+      return ← onLet goal name
     if f.isConstOf ``SPred.imp then
       return ← onImp goal name
     else if f.isConstOf ``PredTrans.apply then
@@ -273,6 +275,11 @@ where
     (·.2) <$> mIntro goal (← `(binderIdent| _)) (fun g =>
         do return ((), ← onGoal g name))
 
+  onLet goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
+    burnOne
+    (·.2) <$> mIntro goal (← `(binderIdent| _)) (fun g =>
+        do return ((), ← onGoal g name))
+
   onLambda goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
     burnOne
     (·.2) <$> mIntroForall goal (← `(binderIdent| _)) (fun g =>
diff --git a/tests/lean/run/9365.lean b/tests/lean/run/9365.lean
index 974629bc68..c58ff7c38a 100644
--- a/tests/lean/run/9365.lean
+++ b/tests/lean/run/9365.lean
@@ -16,8 +16,8 @@ theorem setZeroHead_spec :
    setZeroHead
    ⦃⇓ _ => ⌜∃ ns', (#gns).toList = 0 :: ns'⌝⦄ := by
   mvcgen [setZeroHead]
-  -- We want `mintro`duce the tuple `t` here in order for us not having to repeat its
+  -- We want to see and name the tuple `t` here in order for us not having to repeat its
   -- definition in t.2.toList.tail below
-  mintro t
+  rename_i t
   simp
   exists t.2.toList.tail
diff --git a/tests/lean/run/9474.lean b/tests/lean/run/9474.lean
new file mode 100644
index 0000000000..9a98869c90
--- /dev/null
+++ b/tests/lean/run/9474.lean
@@ -0,0 +1,22 @@
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+abbrev gns : SVal ((List Nat)::[]) (List Nat) := fun s => SVal.pure s
+
+noncomputable def setZeroHead : StateM (List Nat) Unit := do
+  modify fun _ => [1, 0, 1, 2, 3, 4, 5]
+  pure ()
+  modify fun s => s.tail
+  pure ()
+
+theorem setZeroHead_spec :
+   ⦃⌜True⌝⦄
+   setZeroHead
+   ⦃⇓ _ => ⌜∃ ns', #gns = 0 :: ns'⌝⦄ := by
+  mvcgen [setZeroHead] -- should mintro through let/have bindings
+  mleave
+  rename_i t
+  exists t.2.tail
diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean
index 23ea9e2ce7..8bd98dad60 100644
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@@ -494,7 +494,7 @@ theorem mkFreshNat_spec [Monad m] [WPMonad m sh] :
   (mkFreshNat : StateT AppState m Nat)
   ⦃⇓ r => ⌜r = n ∧ #fst = n + 1 ∧ #snd = o⌝⦄ := by
   mvcgen [mkFreshNat]
-  simp_all
+  simp_all +zetaDelta
 
 theorem erase_unfold [Monad m] [WPMonad m sh] :
   ⦃⌜#fst = n ∧ #snd = o⌝⦄