fix: dsimp zeta bug

Before the `zeta` / `zetaDelta` split, `dsimp` was performing `zeta`
by going inside of a `let`-expression, performing `zetaDelta`, and
then removing the unused `let`-expression.

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

@@ -166,6 +166,8 @@ private def reduceStep (e : Expr) : SimpM Expr := do
   if cfg.zeta then
     if let some (args, _, _, v, b) := e.letFunAppArgs? then
       return mkAppN (b.instantiate1 v) args
+    if e.isLet then
+      return e.letBody!.instantiate1 e.letValue!
   match (← unfold? e) with
   | some e' =>
     trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}"

tests/lean/run/zetaDSimpIssue.lean

@@ -0,0 +1,8 @@
+def f (x : Nat) :=
+  let n := x + 1
+  n + n
+
+example : f x = 2*x + 2 := by
+  dsimp [f]
+  guard_target =ₛ x + 1 + (x + 1) = 2*x + 2
+  simp_arith