diff --git a/tests/lean/smartUnfolding.lean b/tests/lean/smartUnfolding.lean
new file mode 100644
index 0000000000..1c62670e82
--- /dev/null
+++ b/tests/lean/smartUnfolding.lean
@@ -0,0 +1,6 @@
+theorem ex1 (x y : Nat) (h : x + 2 = y + 2) : x = y := by
+  injection h with h
+  traceState -- without smart unfolding the state would be a mess
+  injection h with h
+  traceState -- without smart unfolding the state would be a mess
+  assumption
diff --git a/tests/lean/smartUnfolding.lean.expected.out b/tests/lean/smartUnfolding.lean.expected.out
new file mode 100644
index 0000000000..f7e5657466
--- /dev/null
+++ b/tests/lean/smartUnfolding.lean.expected.out
@@ -0,0 +1,6 @@
+x y : Nat
+h : Nat.add x 1 = Nat.add y 1
+⊢ x = y
+x y : Nat
+h : Nat.add x 0 = Nat.add y 0
+⊢ x = y