diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 7ded2ff237..39479ff6be 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -90,7 +90,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
         mkForallFVars #[x] (← loop below (b.instantiate1 x))
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop below type) (← loop below val) fun x => do
-        mkLetFVars #[x] (← loop below (body.instantiate1 x))
+        mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
     | Expr.mdata d e _   => return mkMData d (← loop below e)
     | Expr.proj n i e _  => return mkProj n i (← loop below e)
     | Expr.app _ _ _ =>
diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index de623639af..00c5fd1e96 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -54,8 +54,8 @@ partial def visit (e : Expr) : M Expr := do
       if (← isNonTrivialProof e) then
         mkAuxLemma e
       else match e with
-        | Expr.lam _ _ _ _     => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b)
-        | Expr.letE _ _ _ _ _  => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b)
+        | Expr.lam _ _ _ _     => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
+        | Expr.letE _ _ _ _ _  => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
         | Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b)
         | Expr.mdata _ b _     => return e.updateMData! (← visit b)
         | Expr.proj _ _ b _    => return e.updateProj! (← visit b)
diff --git a/tests/lean/unusedLet.lean b/tests/lean/unusedLet.lean
new file mode 100644
index 0000000000..d1f0f86ffe
--- /dev/null
+++ b/tests/lean/unusedLet.lean
@@ -0,0 +1,11 @@
+def pro := let x := 42; false
+
+#print pro
+
+def f : Nat → Nat
+  | 0 => 1
+  | n+1 =>
+    let y := 42
+    2 * f n
+
+#print f
diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out
new file mode 100644
index 0000000000..f4ad0e5b09
--- /dev/null
+++ b/tests/lean/unusedLet.lean.expected.out
@@ -0,0 +1,14 @@
+def pro : Bool :=
+let x := 42;
+false
+def f : Nat → Nat :=
+fun x =>
+  Nat.brecOn x
+    fun x f =>
+      (match x : (x : Nat) → Nat.below x → Nat with 
+        | 0 => fun x => 1
+        | Nat.succ n =>
+          fun x =>
+            let y := 42;
+            2 * x.fst.fst)
+        f