diff --git a/tests/lean/letFun.lean b/tests/lean/letFun.lean
new file mode 100644
index 0000000000..0da44ce333
--- /dev/null
+++ b/tests/lean/letFun.lean
@@ -0,0 +1,10 @@
+#check
+  let_fun f x := x * 2
+  let_fun x := 1
+  let_fun y := x + 1
+  f (y + x)
+
+example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
+  simp (config := { beta := false }) [h1]
+  traceState
+  simp [h2]
diff --git a/tests/lean/letFun.lean.expected.out b/tests/lean/letFun.lean.expected.out
new file mode 100644
index 0000000000..9d4337b024
--- /dev/null
+++ b/tests/lean/letFun.lean.expected.out
@@ -0,0 +1,10 @@
+let_fun f := fun x => x * 2;
+let_fun x := 1;
+let_fun y := x + 1;
+f (y + x) : Nat
+a b : Nat
+h1 : a = 0
+h2 : b = 0
+⊢ (let_fun x := 1;
+    x + x) >
+    b