diff --git a/tests/lean/run/letDeclSimp.lean b/tests/lean/run/letDeclSimp.lean
new file mode 100644
index 0000000000..41dbd3a38d
--- /dev/null
+++ b/tests/lean/run/letDeclSimp.lean
@@ -0,0 +1,12 @@
+example (a : Nat) : let n := 0; n + a = a := by
+  intro n
+  fail_if_success simp (config := { zeta := false })
+  simp (config := { zeta := false }) [n]
+
+example (a b : Nat) (h : a = b) : let n := 0; n + a = b := by
+  intro n
+  fail_if_success simp (config := { zeta := false })
+  trace_state
+  simp (config := { zeta := false }) [n]
+  trace_state
+  simp [h]