From cd9648a61e30da360556c0ed2e2a77b4f0074615 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 18 Feb 2024 13:31:15 -0800
Subject: [PATCH] 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 | 2 ++
 tests/lean/run/zetaDSimpIssue.lean  | 8 ++++++++
 2 files changed, 10 insertions(+)
 create mode 100644 tests/lean/run/zetaDSimpIssue.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 4a35305b15..c8846c8f9b 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/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'}"
diff --git a/tests/lean/run/zetaDSimpIssue.lean b/tests/lean/run/zetaDSimpIssue.lean
new file mode 100644
index 0000000000..baab4277bb
--- /dev/null
+++ b/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