diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean
index 8c8aea8b1b..7f49a622b7 100644
--- a/src/Init/Data/List/Sort/Impl.lean
+++ b/src/Init/Data/List/Sort/Impl.lean
@@ -210,7 +210,7 @@ theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} → (l : { l : List α // l
     | nil => simp at w'
     | cons x l' =>
       cases l' with
-      | nil => simp at w'; omega
+      | nil => simp at w'
       | cons y l' =>
         rw [mergeSort]
         congr 2
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index e443cf4dc0..d418a4108f 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -50,6 +50,11 @@ protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
 @[simp] protected theorem add_right_cancel_iff {n : Nat} : m + n = k + n ↔ m = k :=
   ⟨Nat.add_right_cancel, fun | rfl => rfl⟩
 
+@[simp] protected theorem add_left_eq_self  {a b : Nat} : a + b = b ↔ a = 0 := by omega
+@[simp] protected theorem add_right_eq_self {a b : Nat} : a + b = a ↔ b = 0 := by omega
+@[simp] protected theorem self_eq_add_right {a b : Nat} : a = a + b ↔ b = 0 := by omega
+@[simp] protected theorem self_eq_add_left  {a b : Nat} : a = b + a ↔ b = 0 := by omega
+
 @[simp] protected theorem add_le_add_iff_left {n : Nat} : n + m ≤ n + k ↔ m ≤ k :=
   ⟨Nat.le_of_add_le_add_left, fun h => Nat.add_le_add_left h _⟩
 
diff --git a/tests/lean/run/2669.lean b/tests/lean/run/2669.lean
index 30650fb1b3..acaab3c0af 100644
--- a/tests/lean/run/2669.lean
+++ b/tests/lean/run/2669.lean
@@ -6,7 +6,7 @@ def f : Nat → Nat := fun x => x - x
 example (n : Nat) : False := by
   let g := f n
   have : g + n = n := by
-    fail_if_success simp (config := { zeta := false }) [Nat.zero_add] -- Should not succeed
+    fail_if_success simp (config := { zeta := false }) [Nat.zero_add, -Nat.add_left_eq_self] -- Should not succeed
     simp [g]
   sorry
 
diff --git a/tests/lean/run/4290.lean b/tests/lean/run/4290.lean
index 263bdaa6c3..1c69f49fbb 100644
--- a/tests/lean/run/4290.lean
+++ b/tests/lean/run/4290.lean
@@ -1,3 +1,5 @@
+attribute [-simp] Nat.self_eq_add_right -- This was later added to the simp set and interfere with the test.
+
 def foo : Nat := 0
 def bar : Nat := 0
 
diff --git a/tests/lean/run/letDeclSimp.lean b/tests/lean/run/letDeclSimp.lean
index 15a0e9a336..9284f3fc24 100644
--- a/tests/lean/run/letDeclSimp.lean
+++ b/tests/lean/run/letDeclSimp.lean
@@ -1,3 +1,5 @@
+attribute [-simp] Nat.add_left_eq_self -- This was later added to the simp set and interfere with the test.
+
 example (a : Nat) : let n := 0; n + a = a := by
   intro n
   fail_if_success simp (config := { zeta := false })
diff --git a/tests/lean/simp_trace.lean b/tests/lean/simp_trace.lean
index 72237fb2d0..71e7df49e5 100644
--- a/tests/lean/simp_trace.lean
+++ b/tests/lean/simp_trace.lean
@@ -83,6 +83,9 @@ example : (a ∧ (b ∧ b)) = (a ∧ b) := by simp only [my_thm]
 example : x - 1 + 1 = x := by simp (discharger := sorry) [Nat.sub_add_cancel]
 
 -- The following examples test simplification at hypotheses.
+section
+-- These lemmas were subsequently added to the simp set and confuse the test.
+attribute [-simp] Nat.add_left_eq_self Nat.add_right_eq_self
 
 -- Two simp lemmas applied to one hypothesis.
 example (h' : bla x = x) : x + x = x := by
@@ -114,6 +117,8 @@ example (h' : bla x = x) : bla x = x := by
   simp [bla, h] at *
   exact h'
 
+end
+
 -- This example tests tracing of class projections.
 
 class HasProp (A) where
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 714d70454c..1fd49529f0 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -75,7 +75,7 @@ Try this: simp only [bla, h] at h'
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 Try this: simp only [bla, h, List.length_append] at *
-simp_trace.lean:99:101-100:40: error: unsolved goals
+simp_trace.lean:102:101-103:40: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α
@@ -88,7 +88,7 @@ h₂ : xs.length + ys.length = y
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 [Meta.Tactic.simp.rewrite] List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
 Try this: simp only [bla, h, List.length_append] at *
-simp_trace.lean:103:101-104:53: error: unsolved goals
+simp_trace.lean:106:101-107:53: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α