feat: add @[simp] to Nat.add_eq_zero_iff (#5241)

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 :=

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₂]

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₂