From a5162ca7489bfdbf1a2851cffd8fdcca9d2b9b56 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Tue, 3 Sep 2024 19:05:04 +1000
Subject: [PATCH] feat: add @[simp] to Nat.add_eq_zero_iff (#5241)

---
 src/Init/Data/Nat/Lemmas.lean | 2 +-
 tests/lean/run/simp4.lean     | 2 +-
 tests/lean/run/simpStar.lean  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index d958f0898b..2bd96124b9 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -46,7 +46,7 @@ theorem succ_add_eq_add_succ (a b) : succ a + b = a + succ b := Nat.succ_add ..
 protected theorem eq_zero_of_add_eq_zero_right (h : n + m = 0) : n = 0 :=
   (Nat.eq_zero_of_add_eq_zero h).1
 
-protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
+@[simp] protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
   ⟨Nat.eq_zero_of_add_eq_zero, fun ⟨h₁, h₂⟩ => h₂.symm ▸ h₁⟩
 
 @[simp] protected theorem add_left_cancel_iff {n : Nat} : n + m = n + k ↔ m = k :=
diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean
index ccd0f74455..cce6c8cdf7 100644
--- a/tests/lean/run/simp4.lean
+++ b/tests/lean/run/simp4.lean
@@ -49,7 +49,7 @@ theorem ex8 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
   simp (config := { contextual := true })
 
 theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
-  fail_if_success simp
+  fail_if_success simp [-Nat.add_eq_zero_iff]
   intro h₁ h₂
   simp [h₁] at h₂
   simp [h₂]
diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean
index 5706bc4cc7..d39ba1dd14 100644
--- a/tests/lean/run/simpStar.lean
+++ b/tests/lean/run/simpStar.lean
@@ -20,7 +20,7 @@ h₂ : g x < 5
 -/
 #guard_msgs in
 theorem ex3 (x y : Nat) (h₁ : f x x = g x) (h₂ : f x x < 5) : f x x + f x x = 0 := by
-  simp [*] at *
+  simp [*, -Nat.add_eq_zero_iff] at *
   trace_state
   have aux₁ : f x x = g x := h₁
   have aux₂ : g x < 5     := h₂