fix: preserve unused let declarations

This commit fixes reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unused.20let.20disappears/near/257528105

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 _ _ _ =>

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)

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

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