test: add test for issue #4585

This issue has been fixed by #6123 closes #4585
2026-03-17 18:34:06 +00:00 · 2024-12-14 13:52:07 -08:00
1 changed files with 13 additions and 0 deletions
--- a/tests/lean/run/4585.lean
+++ b/tests/lean/run/4585.lean
@@ -0,0 +1,13 @@
+example (x y : Nat) : let a := (x,y); a.2 = 0 := by
+  intro a
+  fail_if_success simp
+  guard_target =ₛ a.2 = 0
+  simp +zetaDelta
+  guard_target =ₛ y = 0
+  sorry
+
+example (x y : Nat) : let a := (x,y); a.2 = 0 := by
+  intro a
+  simp [a]
+  guard_target =ₛ y = 0
+  sorry