fix: unused let_fun elimination in simp

This PR fixes a bug in the simplifier. It was producing terms with
loose bound variables when eliminating unused `let_fun` expressions.

This issue was affecting the example at #6374. The example is now
timing out.

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -647,6 +647,8 @@ partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
       let x := mkConst `__no_used_dummy__ -- dummy value
       let { expr, proof, .. } ← go (xs.push x) body.bindingBody!
       let proof := mkApp6 (mkConst ``letFun_unused us) alpha betaFun.bindingBody! val body.bindingBody! expr proof
+      let expr := expr.lowerLooseBVars 1 1
+      let proof := proof.lowerLooseBVars 1 1
       return { expr, proof, modified := true }
     else
       let beta    := betaFun.bindingBody!

tests/lean/run/letFunUnusedVarBug.lean

@@ -0,0 +1,30 @@
+theorem ex1 (h : a = 5) :
+   let_fun x := 1
+   let_fun _y := 2
+   let_fun _z := 3
+   let_fun w := 4
+   x + w = a := by
+  simp -zeta only
+  guard_target =ₛ
+    let_fun x := 1;
+    let_fun w := 4;
+    x + w = a
+  simp only
+  guard_target =ₛ 1 + 4 = a
+  simp [h]
+
+theorem ex2 (h : a = 6) :
+   let_fun x := 1
+   let_fun _y := 2 + x
+   let_fun _z := 3 + x
+   let_fun w := 4 + x
+   let_fun _z := 2 + w
+   x + w = a := by
+  simp -zeta only
+  guard_target =ₛ
+    let_fun x := 1;
+    let_fun w := 4 + x;
+    x + w = a
+  simp only
+  guard_target =ₛ 1 + (4 + 1) = a
+  simp [h]