diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean
index b22d89396e..72bbfcc39b 100644
--- a/src/Init/Data/Array/Erase.lean
+++ b/src/Init/Data/Array/Erase.lean
@@ -59,7 +59,7 @@ theorem exists_or_eq_self_of_eraseP (p) (xs : Array α) :
 @[simp] theorem size_eraseP_of_mem {xs : Array α} (al : a ∈ xs) (pa : p a) :
     (xs.eraseP p).size = xs.size - 1 := by
   let ⟨_, ys, zs, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
-  rw [e₂]; simp [size_append, e₁]; omega
+  rw [e₂]; simp [size_append, e₁]
 
 theorem size_eraseP {xs : Array α} : (xs.eraseP p).size = if xs.any p then xs.size - 1 else xs.size := by
   split <;> rename_i h
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index d5941ee4c2..3a790fcdeb 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3035,7 +3035,7 @@ theorem foldrM_start_stop {m} [Monad m] {xs : Array α} {f : α → β → m β}
     simp
   | succ i ih =>
     unfold foldrM.fold
-    simp only [beq_iff_eq, Nat.add_right_eq_self, Nat.add_one_ne_zero, ↓reduceIte, Nat.add_eq,
+    simp only [beq_iff_eq, Nat.add_eq_left, Nat.add_one_ne_zero, ↓reduceIte, Nat.add_eq,
       getElem_extract]
     congr
     funext b
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 8351c4bd60..96c05e54e8 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1456,7 +1456,6 @@ theorem udiv_intMin_of_msb_false {x : BitVec w} (h : x.msb = false) :
   have wpos : 0 < w := by omega
   have := Nat.two_pow_pos (w-1)
   simp [toNat_eq, wpos]
-  rw [Nat.div_eq_zero_iff_lt (by omega)]
   exact toNat_lt_of_msb_false h
 
 theorem sdiv_intMin {x : BitVec w} :
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1beb2fc973..10ae9534a3 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2032,7 +2032,6 @@ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
       have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le (by decide) (by omega)
       omega
     simp [this] at h
-    omega
 
 /--
 Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree,
@@ -4914,7 +4913,6 @@ theorem intMin_eq_zero_iff {w : Nat} : intMin w = 0#w ↔ w = 0 := by
   · constructor
     · have := Nat.two_pow_pos (w - 1)
       simp [toNat_eq, show 0 < w by omega]
-      omega
     · simp [h]
 
 /--
diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean
index a30e72a44f..e8791e2a7d 100644
--- a/src/Init/Data/Int/DivMod/Bootstrap.lean
+++ b/src/Init/Data/Int/DivMod/Bootstrap.lean
@@ -156,7 +156,7 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
       rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
       apply congrArg negSucc
-      rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
+      rw [Nat.mul_comm, Nat.sub_mul_div_of_le]; rwa [Nat.mul_comm]
 
 theorem add_mul_ediv_left (a : Int) {b : Int}
     (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index e09deca8f4..2455e3126f 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -481,7 +481,7 @@ theorem ediv_eq_neg_one_of_neg_of_le {a b : Int} (H1 : a < 0) (H2 : -a ≤ b) :
   | negSucc a', ofNat (b' + 1), H1, H2 =>
     rw [Int.div_def, ediv, Int.negSucc_eq, Int.neg_inj]
     norm_cast
-    rw [Nat.add_left_eq_self, Nat.div_eq_zero_iff_lt (by omega)]
+    rw [Nat.add_eq_right, Nat.div_eq_zero_iff_lt (by omega)]
     simp [Int.negSucc_eq] at H2
     omega
 
@@ -491,7 +491,7 @@ theorem ediv_eq_one_of_neg_of_le {a b : Int} (H1 : a < 0) (H2 : b ≤ a) : a / b
   | negSucc a', negSucc b', H1, H2 =>
     rw [Int.div_def, ediv, ofNat_eq_coe]
     norm_cast
-    rw [Nat.succ_eq_add_one, Nat.add_left_eq_self, Nat.div_eq_zero_iff_lt (by omega)]
+    rw [Nat.succ_eq_add_one, Nat.add_eq_right, Nat.div_eq_zero_iff_lt (by omega)]
     simp [Int.negSucc_eq] at H2
     omega
 
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 834e34084c..12d0f64439 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -88,7 +88,7 @@ theorem exists_or_eq_self_of_eraseP (p) (l : List α) :
 @[simp] theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
     length (l.eraseP p) = length l - 1 := by
   let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
-  rw [e₂]; simp [length_append, e₁]; rfl
+  rw [e₂]; simp [length_append, e₁]
 
 theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by
   split <;> rename_i h
@@ -542,7 +542,7 @@ theorem eraseIdx_eq_take_drop_succ :
   match l, i with
   | [], _
   | a::l, 0
-  | a::l, i + 1 => simp [Nat.succ_inj']
+  | a::l, i + 1 => simp [Nat.succ_inj]
 
 @[deprecated eraseIdx_eq_nil_iff (since := "2025-01-30")]
 abbrev eraseIdx_eq_nil := @eraseIdx_eq_nil_iff
@@ -551,7 +551,7 @@ theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2
   match l with
   | []
   | [a]
-  | a::b::l => simp [Nat.succ_inj']
+  | a::b::l => simp [Nat.succ_inj]
 
 @[deprecated eraseIdx_ne_nil_iff (since := "2025-01-30")]
 abbrev eraseIdx_ne_nil := @eraseIdx_ne_nil_iff
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index be7225e8b5..1e2ea43315 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -792,7 +792,7 @@ theorem of_findIdx?_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
   | nil => simp_all
   | cons x xs ih =>
     simp_all only [findIdx?_cons, Nat.zero_add]
-    split at w <;> cases i <;> simp_all [succ_inj']
+    split at w <;> cases i <;> simp_all [succ_inj]
 
 @[deprecated of_findIdx?_eq_some (since := "2025-02-02")]
 abbrev findIdx?_of_eq_some := @of_findIdx?_eq_some
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index e23621dc9b..c7244cfa4d 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -701,7 +701,7 @@ theorem set_comm (a b : α) : ∀ {i j : Nat} {l : List α}, i ≠ j →
   | _+1, 0, _ :: _, _ => by simp [set]
   | 0, _+1, _ :: _, _ => by simp [set]
   | _+1, _+1, _ :: t, h =>
-    congrArg _ <| set_comm a b fun h' => h <| Nat.succ_inj'.mpr h'
+    congrArg _ <| set_comm a b fun h' => h <| Nat.succ_inj.mpr h'
 
 @[simp]
 theorem set_set (a : α) {b : α} : ∀ {l : List α} {i : Nat}, (l.set i a).set i b = l.set i b
diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean
index 336a17f7b4..9fcc8c6ad4 100644
--- a/src/Init/Data/List/Nat/Basic.lean
+++ b/src/Init/Data/List/Nat/Basic.lean
@@ -118,7 +118,7 @@ theorem mem_eraseIdx_iff_getElem {x : α} :
   | a::l, 0 => by simp [mem_iff_getElem, Nat.succ_lt_succ_iff]
   | a::l, k+1 => by
     rw [← Nat.or_exists_add_one]
-    simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj', Nat.succ_lt_succ_iff]
+    simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj, Nat.succ_lt_succ_iff]
 
 theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x := by
   simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, exists_and_left]
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index 766ad82ce6..3bc53e7824 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -40,7 +40,6 @@ theorem getLast?_range' {n : Nat} : (range' s n).getLast? = if n = 0 then none e
       simp [h]
     · rw [if_neg h]
       simp
-      omega
 
 @[simp] theorem getLast_range' {n : Nat} (h) : (range' s n).getLast h = s + n - 1 := by
   cases n with
@@ -358,7 +357,7 @@ theorem zipIdx_singleton {x : α} {k : Nat} : zipIdx [x] k = [(x, k)] :=
 @[simp] theorem getLast?_zipIdx {l : List α} {k : Nat} :
     (zipIdx l k).getLast? = l.getLast?.map fun a => (a, k + l.length - 1) := by
   simp [getLast?_eq_getElem?]
-  cases l <;> simp; omega
+  cases l <;> simp
 
 theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : List α} :
     (x, k + i) ∈ zipIdx l k ↔ l[i]? = some x := by
@@ -497,7 +496,7 @@ theorem head?_enumFrom (n : Nat) (l : List α) :
 theorem getLast?_enumFrom (n : Nat) (l : List α) :
     (enumFrom n l).getLast? = l.getLast?.map fun a => (n + l.length - 1, a) := by
   simp [getLast?_eq_getElem?]
-  cases l <;> simp; omega
+  cases l <;> simp
 
 @[deprecated mk_add_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
 theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} :
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 73822040a3..c97dc112ab 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -532,7 +532,7 @@ theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
   | zero => simp
   | succ n =>
     suffices 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m by
-      simpa [rotateRight]
+      simp [rotateRight]
     intro h
     have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
     rw [Nat.min_eq_left (by omega)]
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index c806cf3487..e8da67af7f 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -407,7 +407,7 @@ theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l
     refine ((IH fun b => ?_).cons a).trans (perm_cons_erase this).symm
     specialize H b
     rw [(perm_cons_erase this).count_eq] at H
-    by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj'] using H
+    by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj] using H
 
 theorem isPerm_iff : ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
   | [], [] => by simp [isPerm, isEmpty]
diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean
index 0ce5797059..28e3fce0fc 100644
--- a/src/Init/Data/List/Range.lean
+++ b/src/Init/Data/List/Range.lean
@@ -69,7 +69,7 @@ theorem mem_range' : ∀ {n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step
   | 0 => by simp [range', Nat.not_lt_zero]
   | n + 1 => by
     have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by
-      cases i <;> simp [Nat.succ_le, Nat.succ_inj']
+      cases i <;> simp [Nat.succ_le, Nat.succ_inj]
     simp [range', mem_range', Nat.lt_succ, h]; simp only [← exists_and_right, and_assoc]
     rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
 
diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean
index a6e0cc58a7..883ead986d 100644
--- a/src/Init/Data/List/Zip.lean
+++ b/src/Init/Data/List/Zip.lean
@@ -220,7 +220,7 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
           · simp_all
         · obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₃
           · simp_all
-          · simp_all [zipWith_append, Nat.succ_inj']
+          · simp_all [zipWith_append, Nat.succ_inj]
 
 /-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
 @[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 67c2a6d51a..77e80cb9c4 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -546,6 +546,10 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a 
 
 /-! ### le/lt -/
 
+attribute [simp] not_lt_zero
+
+example : (default : Nat) = 0 := rfl
+
 protected theorem lt_asymm {a b : Nat} (h : a < b) : ¬ b < a := Nat.not_lt.2 (Nat.le_of_lt h)
 /-- Alias for `Nat.lt_asymm`. -/
 protected abbrev not_lt_of_gt := @Nat.lt_asymm
@@ -618,7 +622,7 @@ protected theorem eq_zero_of_not_pos (h : ¬0 < n) : n = 0 :=
 
 attribute [simp] zero_lt_succ
 
-theorem succ_ne_self (n) : succ n ≠ n := Nat.ne_of_gt (lt_succ_self n)
+@[simp] theorem succ_ne_self (n) : succ n ≠ n := Nat.ne_of_gt (lt_succ_self n)
 
 theorem add_one_ne_self (n) : n + 1 ≠ n := Nat.ne_of_gt (lt_succ_self n)
 
@@ -641,13 +645,20 @@ theorem eq_zero_or_eq_succ_pred : ∀ n, n = 0 ∨ n = succ (pred n)
   | 0 => .inl rfl
   | _+1 => .inr rfl
 
-theorem succ_inj' : succ a = succ b ↔ a = b := (Nat.succ.injEq a b).to_iff
+theorem succ_inj : succ a = succ b ↔ a = b := (Nat.succ.injEq a b).to_iff
+
+@[deprecated succ_inj (since := "2025-04-14")]
+theorem succ_inj' : succ a = succ b ↔ a = b := succ_inj
 
 theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_succ, succ_le_succ⟩
 
 theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, succ_lt_succ⟩
 
-theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj'
+theorem succ_ne_succ_iff : succ a ≠ succ b ↔ a ≠ b := by simp [Nat.succ.injEq]
+
+theorem succ_succ_ne_one (a : Nat) : succ (succ a) ≠ 1 := nofun
+
+theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj
 
 theorem ne_add_one (n : Nat) : n ≠ n + 1 := fun h => by cases h
 
@@ -657,6 +668,10 @@ theorem add_one_le_add_one_iff : a + 1 ≤ b + 1 ↔ a ≤ b := succ_le_succ_iff
 
 theorem add_one_lt_add_one_iff : a + 1 < b + 1 ↔ a < b := succ_lt_succ_iff
 
+theorem add_one_ne_add_one_iff : a + 1 ≠ b + 1 ↔ a ≠ b := succ_ne_succ_iff
+
+theorem add_one_add_one_ne_one : a + 1 + 1 ≠ 1 := nofun
+
 theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b
   | _+1, _+1, _, _ => congrArg _
 
@@ -714,16 +729,18 @@ theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n =
 theorem ctor_eq_zero : Nat.zero = 0 :=
   rfl
 
-protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
+@[simp] protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
   fun h => Nat.noConfusion h
 
-protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
+@[simp] protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
   fun h => Nat.noConfusion h
 
-theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
+@[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
 instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩
 
+@[simp] theorem default_eq_zero : default = 0 := rfl
+
 /-! # mul + order -/
 
 theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
@@ -1003,7 +1020,7 @@ protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m :=
   suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption
   by rw [Nat.add_sub_add_right, Nat.sub_zero]
 
-protected theorem add_sub_cancel_left (n m : Nat) : n + m - n = m :=
+@[simp] protected theorem add_sub_cancel_left (n m : Nat) : n + m - n = m :=
   show n + m - (n + 0) = m from
   by rw [Nat.add_sub_add_left, Nat.sub_zero]
 
@@ -1054,7 +1071,7 @@ protected theorem sub_self_add (n m : Nat) : n - (n + m) = 0 := by
   show (n + 0) - (n + m) = 0
   rw [Nat.add_sub_add_left, Nat.zero_sub]
 
-protected theorem sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) : n - m = 0 := by
+@[simp] protected theorem sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) : n - m = 0 := by
   match le.dest h with
   | ⟨k, hk⟩ => rw [← hk, Nat.sub_self_add]
 
diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean
index 5b76ca844b..69b7b5e155 100644
--- a/src/Init/Data/Nat/Div/Basic.lean
+++ b/src/Init/Data/Nat/Div/Basic.lean
@@ -473,7 +473,8 @@ Nat.le_antisymm
   (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi))
   ((Nat.le_div_iff_mul_le npos).2 lo)
 
-theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by
+/-- See also `sub_mul_div` for a strictly more general version. -/
+theorem sub_mul_div_of_le (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by
   match eq_zero_or_pos n with
   | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
   | .inr h₀ => induction p with
@@ -551,7 +552,7 @@ protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k
 @[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
   rw [Nat.mul_comm, mul_div_right _ H]
 
-protected theorem div_self (H : 0 < n) : n / n = 1 := by
+@[simp] protected theorem div_self (H : 0 < n) : n / n = 1 := by
   let t := add_div_right 0 H
   rwa [Nat.zero_add, Nat.zero_div] at t
 
diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean
index e92b0ccae5..219b8c5799 100644
--- a/src/Init/Data/Nat/Div/Lemmas.lean
+++ b/src/Init/Data/Nat/Div/Lemmas.lean
@@ -84,6 +84,10 @@ theorem div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
   (Nat.le_div_iff_mul_le hc).2 <|
     Nat.le_trans (Nat.mul_le_mul_left _ hcb) (Nat.div_mul_le_self a b)
 
+protected theorem div_le_div {a b c d : Nat} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) : a / c ≤ b / d :=
+  calc a / c ≤ b / c := Nat.div_le_div_right h1
+    _ ≤ b / d := Nat.div_le_div_left h2 (Nat.pos_of_ne_zero h3)
+
 theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
     x / (y + z) ≤ x / z :=
   div_le_div_left (Nat.le_add_left z y) h
@@ -104,7 +108,7 @@ theorem succ_div_of_dvd {a b : Nat} (h : b ∣ a + 1) :
           Nat.add_right_cancel_iff] at h
         subst h
         rw [Nat.add_sub_cancel, ← Nat.add_one_mul, mul_div_right _ (zero_lt_succ _), Nat.add_comm,
-          Nat.add_mul_div_left _ _ (zero_lt_succ _), Nat.self_eq_add_left, div_eq_of_lt le.refl]
+          Nat.add_mul_div_left _ _ (zero_lt_succ _), Nat.right_eq_add, div_eq_of_lt le.refl]
     · simp only [Nat.not_le] at h'
       replace h' : a + 1 < b + 1 := Nat.add_lt_add_right h' 1
       rw [Nat.mod_eq_of_lt h'] at h
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 33bae71df9..725d890c64 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1,21 +1,22 @@
 /-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn
 -/
 prelude
 import Init.Data.Nat.MinMax
 import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
+import Init.Data.Nat.Mod
 import Init.Omega
 
-/-! # Basic lemmas about natural numbers
+/-! # Basic theorems about natural numbers
 
-The primary purpose of the lemmas in this file is to assist with reasoning
+The primary purpose of the theorems in this file is to assist with reasoning
 about sizes of objects, array indices and such.
 
-This file was upstreamed from Std,
-and later these lemmas should be organised into other files more systematically.
+The content of this file was upstreamed from Batteries and mathlib,
+and later these theorems should be organised into other files more systematically.
 -/
 
 namespace Nat
@@ -100,13 +101,94 @@ theorem exists_lt_succ_left {p : Nat → Prop} :
     (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1)) := by
   simpa using exists_lt_succ_left' (p := fun m _ => p m)
 
+/-! ## succ/pred -/
+
+protected theorem sub_one (n) : n - 1 = pred n := rfl
+
+theorem one_add (n) : 1 + n = succ n := Nat.add_comm ..
+
+theorem succ_ne_succ : succ m ≠ succ n ↔ m ≠ n :=
+  ⟨mt (congrArg Nat.succ ·), mt succ.inj⟩
+
+theorem one_lt_succ_succ (n : Nat) : 1 < n.succ.succ := succ_lt_succ <| succ_pos _
+
+theorem not_succ_lt_self : ¬ succ n < n := Nat.not_lt_of_ge n.le_succ
+
+theorem succ_le_iff : succ m ≤ n ↔ m < n := ⟨lt_of_succ_le, succ_le_of_lt⟩
+
+theorem le_succ_iff {m n : Nat} : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ := by
+  refine ⟨fun hmn ↦ (Nat.lt_or_eq_of_le hmn).imp_left le_of_lt_succ, ?_⟩
+  rintro (hmn | rfl)
+  · exact le_succ_of_le hmn
+  · exact Nat.le_refl _
+
+theorem lt_iff_le_pred : ∀ {n}, 0 < n → (m < n ↔ m ≤ n - 1) | _ + 1, _ => Nat.lt_succ_iff
+
+-- TODO: state LHS using `- 1` instead?
+theorem le_of_pred_lt : ∀ {m}, pred m < n → m ≤ n
+  | 0 => Nat.le_of_lt
+  | _ + 1 => id
+
+theorem lt_iff_add_one_le : m < n ↔ m + 1 ≤ n := by rw [succ_le_iff]
+
+theorem lt_one_add_iff : m < 1 + n ↔ m ≤ n := by simp only [Nat.add_comm, Nat.lt_succ_iff]
+
+theorem one_add_le_iff : 1 + m ≤ n ↔ m < n := by simp only [Nat.add_comm, add_one_le_iff]
+
+theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 := Nat.pos_iff_ne_zero
+
+theorem one_lt_iff_ne_zero_and_ne_one : ∀ {n : Nat}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
+  | 0 => by decide
+  | 1 => by decide
+  | n + 2 => by omega
+
+theorem le_one_iff_eq_zero_or_eq_one : ∀ {n : Nat}, n ≤ 1 ↔ n = 0 ∨ n = 1 := by simp [le_succ_iff]
+
+theorem one_le_of_lt (h : a < b) : 1 ≤ b := Nat.lt_of_le_of_lt (Nat.zero_le _) h
+
+theorem pred_one_add (n : Nat) : pred (1 + n) = n := by rw [Nat.add_comm, add_one, Nat.pred_succ]
+
+theorem pred_eq_self_iff : n.pred = n ↔ n = 0 := by cases n <;> simp [(Nat.succ_ne_self _).symm]
+
+theorem pred_eq_of_eq_succ {m n : Nat} (H : m = n.succ) : m.pred = n := by simp [H]
+
+@[simp] theorem pred_eq_succ_iff : n - 1 = m + 1 ↔ n = m + 2 := by
+  cases n <;> constructor <;> rintro ⟨⟩ <;> rfl
+
+@[simp] theorem add_succ_sub_one (m n : Nat) : m + succ n - 1 = m + n := rfl
+
+@[simp]
+theorem succ_add_sub_one (n m : Nat) : succ m + n - 1 = m + n := by rw [succ_add, Nat.add_one_sub_one]
+
+theorem pred_sub (n m : Nat) : pred n - m = pred (n - m) := by
+  rw [← Nat.sub_one, Nat.sub_sub, one_add, sub_succ]
+
+theorem self_add_sub_one : ∀ n, n + (n - 1) = 2 * n - 1
+  | 0 => rfl
+  | n + 1 => by rw [Nat.two_mul]; exact (add_succ_sub_one (Nat.succ _) _).symm
+
+theorem sub_one_add_self (n : Nat) : (n - 1) + n = 2 * n - 1 := Nat.add_comm _ n ▸ self_add_sub_one n
+
+theorem self_add_pred (n : Nat) : n + pred n = (2 * n).pred := self_add_sub_one n
+theorem pred_add_self (n : Nat) : pred n + n = (2 * n).pred := sub_one_add_self n
+
+theorem pred_le_iff : pred m ≤ n ↔ m ≤ succ n :=
+  ⟨le_succ_of_pred_le, by
+    cases m
+    · exact fun _ ↦ zero_le n
+    · exact le_of_succ_le_succ⟩
+
+theorem lt_of_lt_pred (h : m < n - 1) : m < n := by omega
+
+theorem le_add_pred_of_pos (a : Nat) (hb : b ≠ 0) : a ≤ b + (a - 1) := by omega
+
+theorem lt_pred_iff : a < pred b ↔ succ a < b := by simp; omega
+
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
   rw [Nat.add_assoc, Nat.add_assoc, Nat.add_left_comm b]
 
-theorem one_add (n) : 1 + n = succ n := Nat.add_comm ..
-
 theorem succ_eq_one_add (n) : succ n = 1 + n := (one_add _).symm
 
 theorem succ_add_eq_add_succ (a b) : succ a + b = a + succ b := Nat.succ_add ..
@@ -114,19 +196,31 @@ 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
 
-@[simp] protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
+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 :=
+@[simp high] protected theorem add_left_cancel_iff {n : Nat} : n + m = n + k ↔ m = k :=
   ⟨Nat.add_left_cancel, fun | rfl => rfl⟩
 
-@[simp] protected theorem add_right_cancel_iff {n : Nat} : m + n = k + n ↔ m = k :=
+@[simp high] 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
+protected theorem add_left_inj {n : Nat} : m + n = k + n ↔ m = k := Nat.add_right_cancel_iff
+protected theorem add_right_inj {n : Nat} : n + m = n + k ↔ m = k := Nat.add_left_cancel_iff
+
+@[simp high] protected theorem add_eq_left {a b : Nat} : a + b = a ↔ b = 0 := by omega
+@[simp high] protected theorem add_eq_right {a b : Nat} : a + b = b ↔ a = 0 := by omega
+@[simp high] protected theorem left_eq_add {a b : Nat} : a = a + b ↔ b = 0 := by omega
+@[simp high] protected theorem right_eq_add {a b : Nat} : b = a + b ↔ a = 0 := by omega
+
+@[deprecated Nat.add_eq_right (since := "2025-04-15")]
+protected theorem add_left_eq_self  {a b : Nat} : a + b = b ↔ a = 0 := Nat.add_eq_right
+@[deprecated Nat.add_eq_left (since := "2025-04-15")]
+protected theorem add_right_eq_self {a b : Nat} : a + b = a ↔ b = 0 := Nat.add_eq_left
+@[deprecated Nat.left_eq_add (since := "2025-04-15")]
+protected theorem self_eq_add_right {a b : Nat} : a = a + b ↔ b = 0 := Nat.left_eq_add
+@[deprecated Nat.right_eq_add (since := "2025-04-15")]
+protected theorem self_eq_add_left  {a b : Nat} : a = b + a ↔ b = 0 := Nat.right_eq_add
 
 protected theorem lt_of_add_lt_add_right : ∀ {n : Nat}, k + n < m + n → k < m
   | 0, h => h
@@ -173,9 +267,28 @@ protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
 theorem le_iff_lt_add_one : x ≤ y ↔ x < y + 1 := by
   omega
 
-/-! ## sub -/
+@[simp high] protected theorem add_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by omega
 
-protected theorem sub_one (n) : n - 1 = pred n := rfl
+theorem add_pos_iff_pos_or_pos : 0 < m + n ↔ 0 < m ∨ 0 < n := by omega
+
+theorem add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 := by omega
+
+theorem add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0 := by
+  omega
+
+theorem add_eq_three_iff :
+    m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0 := by
+  omega
+
+theorem le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 := by omega
+
+theorem le_and_le_add_one_iff : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1 := by omega
+
+theorem add_succ_lt_add (hab : a < b) (hcd : c < d) : a + c + 1 < b + d := by omega
+
+theorem le_or_le_of_add_eq_add_pred (h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c := by omega
+
+/-! ## sub -/
 
 protected theorem one_sub : ∀ n, 1 - n = if n = 0 then 1 else 0
   | 0 => rfl
@@ -213,7 +326,7 @@ protected theorem sub_eq_zero_iff_le : n - m = 0 ↔ n ≤ m :=
 protected theorem sub_pos_iff_lt : 0 < n - m ↔ m < n :=
   ⟨Nat.lt_of_sub_pos, Nat.sub_pos_of_lt⟩
 
-protected theorem sub_le_iff_le_add {a b c : Nat} : a - b ≤ c ↔ a ≤ c + b :=
+@[simp] protected theorem sub_le_iff_le_add {a b c : Nat} : a - b ≤ c ↔ a ≤ c + b :=
   ⟨Nat.le_add_of_sub_le, sub_le_of_le_add⟩
 
 protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c := by
@@ -274,6 +387,25 @@ protected theorem exists_eq_add_of_le' (h : m ≤ n) : ∃ k : Nat, n = k + m :=
 protected theorem exists_eq_add_of_lt (h : m < n) : ∃ k : Nat, n = m + k + 1 :=
   ⟨n - (m + 1), by rw [Nat.add_right_comm, add_sub_of_le h]⟩
 
+/-- A version of `Nat.sub_succ` in the form `_ - 1` instead of `Nat.pred _`. -/
+theorem sub_succ' (m n : Nat) : m - n.succ = m - n - 1 := rfl
+
+protected theorem sub_eq_of_eq_add' {a b c : Nat} (h : a = b + c) : a - b = c := by omega
+protected theorem eq_sub_of_add_eq {a b c : Nat} (h : c + b = a) : c = a - b := by omega
+protected theorem eq_sub_of_add_eq' {a b c : Nat} (h : b + c = a) : c = a - b := by omega
+
+protected theorem lt_sub_iff_add_lt {a b c : Nat} : a < c - b ↔ a + b < c := ⟨add_lt_of_lt_sub, lt_sub_of_add_lt⟩
+protected theorem lt_sub_iff_add_lt' {a b c : Nat} : a < c - b ↔ b + a < c := by omega
+protected theorem sub_lt_iff_lt_add {a b c : Nat} (hba : b ≤ a) : a - b < c ↔ a < c + b := by omega
+protected theorem sub_lt_iff_lt_add' {a b c : Nat} (hba : b ≤ a) : a - b < c ↔ a < b + c := by omega
+
+-- TODO: variants
+protected theorem sub_sub_sub_cancel_right {a b c : Nat} (h : c ≤ b) : a - c - (b - c) = a - b := by omega
+protected theorem add_sub_sub_cancel {a b c : Nat} (h : c ≤ a) : a + b - (a - c) = b + c := by omega
+protected theorem sub_add_sub_cancel {a b c : Nat} (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c := by omega
+
+protected theorem sub_lt_sub_iff_right {a b c : Nat} (h : c ≤ a) : a - c < b - c ↔ a < b := by omega
+
 /-! ### min/max -/
 
 theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
@@ -417,6 +549,24 @@ protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max
 protected theorem sub_max_sub_left (a b c : Nat) : max (a - b) (a - c) = a - min b c := by
   omega
 
+protected theorem min_left_comm (a b c : Nat) : min a (min b c) = min b (min a c) := by
+  rw [← Nat.min_assoc, ← Nat.min_assoc, b.min_comm]
+
+protected theorem max_left_comm (a b c : Nat) : max a (max b c) = max b (max a c) := by
+  rw [← Nat.max_assoc, ← Nat.max_assoc, b.max_comm]
+
+protected theorem min_right_comm (a b c : Nat) : min (min a b) c = min (min a c) b := by
+  rw [Nat.min_assoc, Nat.min_assoc, b.min_comm]
+
+protected theorem max_right_comm (a b c : Nat) : max (max a b) c = max (max a c) b := by
+  rw [Nat.max_assoc, Nat.max_assoc, b.max_comm]
+
+@[simp] theorem min_eq_zero_iff : min m n = 0 ↔ m = 0 ∨ n = 0 := by omega
+@[simp] theorem max_eq_zero_iff : max m n = 0 ↔ m = 0 ∧ n = 0 := by omega
+
+theorem add_eq_max_iff : m + n = max m n ↔ m = 0 ∨ n = 0 := by omega
+theorem add_eq_min_iff : m + n = min m n ↔ m = 0 ∧ n = 0 := by omega
+
 /-! ### mul -/
 
 protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by
@@ -538,6 +688,101 @@ protected theorem mul_dvd_mul_iff_left {a b c : Nat} (h : 0 < a) : a * b ∣ a *
 protected theorem mul_dvd_mul_iff_right {a b c : Nat} (h : 0 < c) : a * c ∣ b * c ↔ a ∣ b := by
   rw [Nat.mul_comm _ c, Nat.mul_comm _ c, Nat.mul_dvd_mul_iff_left h]
 
+protected theorem zero_eq_mul : 0 = m * n ↔ m = 0 ∨ n = 0 := by rw [eq_comm, Nat.mul_eq_zero]
+
+-- TODO: Replace `Nat.mul_right_cancel_iff` with `Nat.mul_left_inj`
+protected theorem mul_left_inj (ha : a ≠ 0) : b * a = c * a ↔ b = c :=
+  Nat.mul_right_cancel_iff (Nat.pos_iff_ne_zero.2 ha)
+
+-- TODO: Replace `Nat.mul_left_cancel_iff` with `Nat.mul_right_inj`
+protected theorem mul_right_inj (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
+  Nat.mul_left_cancel_iff (Nat.pos_iff_ne_zero.2 ha)
+
+protected theorem mul_ne_mul_left (ha : a ≠ 0) : b * a ≠ c * a ↔ b ≠ c :=
+  not_congr (Nat.mul_left_inj ha)
+
+protected theorem mul_ne_mul_right (ha : a ≠ 0) : a * b ≠ a * c ↔ b ≠ c :=
+  not_congr (Nat.mul_right_inj ha)
+
+theorem mul_eq_left (ha : a ≠ 0) : a * b = a ↔ b = 1 := by simpa using Nat.mul_right_inj ha (c := 1)
+theorem mul_eq_right (hb : b ≠ 0) : a * b = b ↔ a = 1 := by simpa using Nat.mul_left_inj hb (c := 1)
+
+/-- The product of two natural numbers is greater than 1 if and only if
+  at least one of them is greater than 1 and both are positive. -/
+theorem one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by
+  constructor <;> intro h
+  · refine Decidable.by_contra (fun h' => ?_)
+    simp only [Nat.le_zero, Decidable.not_and_iff_not_or_not, not_or, Nat.not_lt] at h'
+    obtain rfl | rfl | h' := h'
+    · simp at h
+    · simp at h
+    · exact Nat.not_lt_of_le (Nat.mul_le_mul h'.1 h'.2) h
+  · obtain hm | hn := h.2.2
+    · exact Nat.mul_lt_mul_of_lt_of_le' hm h.2.1 Nat.zero_lt_one
+    · exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1
+
+theorem eq_one_of_mul_eq_one_right (H : m * n = 1) : m = 1 := eq_one_of_dvd_one ⟨n, H.symm⟩
+
+theorem eq_one_of_mul_eq_one_left (H : m * n = 1) : n = 1 :=
+  eq_one_of_mul_eq_one_right (n := m) (by rwa [Nat.mul_comm])
+
+@[simp] protected theorem lt_mul_iff_one_lt_left (hb : 0 < b) : b < a * b ↔ 1 < a := by
+  simpa using Nat.mul_lt_mul_right (b := 1) hb
+
+@[simp] protected theorem lt_mul_iff_one_lt_right (ha : 0 < a) : a < a * b ↔ 1 < b := by
+  simpa using Nat.mul_lt_mul_left (b := 1) ha
+
+theorem eq_zero_of_two_mul_le (h : 2 * n ≤ n) : n = 0 := by omega
+
+theorem eq_zero_of_mul_le (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0 :=
+  eq_zero_of_two_mul_le <| Nat.le_trans (Nat.mul_le_mul_right _ hb) h
+
+theorem succ_mul_pos (m : Nat) (hn : 0 < n) : 0 < succ m * n := Nat.mul_pos m.succ_pos hn
+
+theorem mul_self_le_mul_self {m n : Nat} (h : m ≤ n) : m * m ≤ n * n := Nat.mul_le_mul h h
+
+-- This name is consistent with mathlib's top level definitions for groups with zero, where there
+-- are `mul_lt_mul`, `mul_lt_mul'` and `mul_lt_mul''`, all with different sets of hypotheses.
+theorem mul_lt_mul'' {a b c d : Nat} (hac : a < c) (hbd : b < d) : a * b < c * d :=
+  Nat.mul_lt_mul_of_lt_of_le hac (Nat.le_of_lt hbd) <| by omega
+
+protected theorem lt_iff_lt_of_mul_eq_mul (ha : a ≠ 0) (hbd : a = b * d) (hce : a = c * e) :
+    c < b ↔ d < e where
+  mp hcb := Nat.lt_of_not_le fun hed ↦ Nat.not_lt_of_le (Nat.le_of_eq <| hbd.symm.trans hce) <|
+    Nat.mul_lt_mul_of_lt_of_le hcb hed <| by simp [hbd, Nat.mul_eq_zero] at ha; omega
+  mpr hde := Nat.lt_of_not_le fun hbc ↦ Nat.not_lt_of_le (Nat.le_of_eq <| hce.symm.trans hbd) <|
+    Nat.mul_lt_mul_of_le_of_lt hbc hde <| by simp [hce, Nat.mul_eq_zero] at ha; omega
+
+theorem mul_self_lt_mul_self {m n : Nat} (h : m < n) : m * m < n * n := mul_lt_mul'' h h
+
+theorem mul_self_le_mul_self_iff {m n : Nat} : m * m ≤ n * n ↔ m ≤ n :=
+  ⟨fun h => Nat.le_of_not_lt fun h' => Nat.not_le_of_gt (mul_self_lt_mul_self h') h,
+   mul_self_le_mul_self⟩
+
+theorem mul_self_lt_mul_self_iff {m n : Nat} : m * m < n * n ↔ m < n := by
+  simp only [← Nat.not_le, mul_self_le_mul_self_iff]
+
+theorem le_mul_self : ∀ n : Nat, n ≤ n * n
+  | 0 => Nat.le_refl _
+  | n + 1 => by simp [Nat.mul_add]
+
+theorem mul_self_inj {m n : Nat} : m * m = n * n ↔ m = n := by
+  simp [Nat.le_antisymm_iff, mul_self_le_mul_self_iff]
+
+@[simp] theorem lt_mul_self_iff : ∀ {n : Nat}, n < n * n ↔ 1 < n
+  | 0 => by simp
+  | n + 1 => Nat.lt_mul_iff_one_lt_left n.succ_pos
+
+theorem add_sub_one_le_mul (ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b := by
+  cases a
+  · cases ha rfl
+  · rw [succ_add, Nat.add_one_sub_one, succ_mul]
+    exact Nat.add_le_add_right (Nat.le_mul_of_pos_right _ <| Nat.pos_iff_ne_zero.2 hb) _
+
+protected theorem add_le_mul {a : Nat} (ha : 2 ≤ a) : ∀ {b : Nat} (_ : 2 ≤ b), a + b ≤ a * b
+  | 2, _ => by omega
+  | b + 3, _ => by have := Nat.add_le_mul ha (Nat.le_add_left _ b); rw [mul_succ]; omega
+
 /-! ### div/mod -/
 
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
@@ -629,6 +874,203 @@ theorem div_eq_self {m n : Nat} : m / n = m ↔ m = 0 ∨ n = 1 := by
   · exact hn
   · exact False.elim (absurd h (Nat.ne_of_lt (Nat.div_lt_self hm hn)))
 
+@[simp] protected theorem div_eq_zero_iff : a / b = 0 ↔ b = 0 ∨ a < b where
+  mp h := by
+    rw [← mod_add_div a b, h, Nat.mul_zero, Nat.add_zero, Decidable.or_iff_not_imp_left]
+    exact mod_lt _ ∘ Nat.pos_iff_ne_zero.2
+  mpr := by
+    obtain rfl | hb := Decidable.em (b = 0)
+    · simp
+    simp only [hb, false_or]
+    rw [← Nat.mul_right_inj hb, ← Nat.add_left_cancel_iff, mod_add_div]
+    simp +contextual [mod_eq_of_lt]
+
+protected theorem div_ne_zero_iff : a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a := by simp
+
+@[simp] protected theorem div_pos_iff : 0 < a / b ↔ 0 < b ∧ b ≤ a := by
+  simp [Nat.pos_iff_ne_zero]
+
+theorem lt_mul_of_div_lt (h : a / c < b) (hc : 0 < c) : a < b * c :=
+  Nat.lt_of_not_ge <| Nat.not_le_of_gt h ∘ (Nat.le_div_iff_mul_le hc).2
+
+theorem mul_div_le_mul_div_assoc (a b c : Nat) : a * (b / c) ≤ a * b / c :=
+  if hc0 : c = 0 then by simp [hc0] else
+    (Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero hc0)).2
+      (by rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _))
+
+protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
+    a = b * c := by
+  rw [← H2, Nat.mul_div_cancel' H1]
+
+protected theorem eq_mul_of_div_eq_left {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) : a = c * b := by
+  rw [Nat.mul_comm, Nat.eq_mul_of_div_eq_right H1 H2]
+
+protected theorem mul_div_cancel_left' {a b : Nat} (Hd : a ∣ b) : a * (b / a) = b := by
+  rw [Nat.mul_comm, Nat.div_mul_cancel Hd]
+
+theorem lt_div_mul_add {a b : Nat} (hb : 0 < b) : a < a / b * b + b := by
+  rw [← Nat.succ_mul, ← Nat.div_lt_iff_lt_mul hb]; exact Nat.lt_succ_self _
+
+@[simp]
+protected theorem div_left_inj {a b d : Nat} (hda : d ∣ a) (hdb : d ∣ b) :
+    a / d = b / d ↔ a = b := by
+  refine ⟨fun h ↦ ?_, congrArg fun b ↦ b / d⟩
+  rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]
+
+theorem div_le_iff_le_mul_add_pred (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1) := by
+  rw [← Nat.lt_succ_iff, div_lt_iff_lt_mul hb, succ_mul, Nat.mul_comm]
+  cases hb <;> exact Nat.lt_succ_iff
+
+theorem one_le_div_iff {a b : Nat} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by
+  rw [le_div_iff_mul_le hb, Nat.one_mul]
+
+theorem div_lt_one_iff (hb : 0 < b) : a / b < 1 ↔ a < b := by
+  simp only [← Nat.not_le, one_le_div_iff hb]
+
+protected theorem div_le_div_right {a b c : Nat} (h : a ≤ b) : a / c ≤ b / c :=
+  (c.eq_zero_or_pos.elim fun hc ↦ by simp [hc]) fun hc ↦
+    (le_div_iff_mul_le hc).2 <| Nat.le_trans (Nat.div_mul_le_self _ _) h
+
+theorem lt_of_div_lt_div {a b c : Nat} (h : a / c < b / c) : a < b :=
+  Nat.lt_of_not_le fun hab ↦ Nat.not_le_of_lt h <| Nat.div_le_div_right hab
+
+theorem sub_mul_div (a b c : Nat) : (a - b * c) / b = a / b - c := by
+  obtain h | h := Nat.le_total (b * c) a
+  · rw [Nat.sub_mul_div_of_le _ _ _ h]
+  · rw [Nat.sub_eq_zero_of_le h, Nat.zero_div]
+    by_cases hn : b = 0
+    · simp only [hn, Nat.div_zero, zero_le, Nat.sub_eq_zero_of_le]
+    · have h2 : a / b ≤ (b * c) / b := Nat.div_le_div_right h
+      rw [Nat.mul_div_cancel_left _ (zero_lt_of_ne_zero hn)] at h2
+      rw [Nat.sub_eq_zero_of_le h2]
+
+theorem mul_sub_div_of_dvd {b c : Nat} (hc : c ≠ 0) (hcb : c ∣ b) (a : Nat) : (c * a - b) / c = a - b / c := by
+  obtain ⟨_, hx⟩ := hcb
+  simp only [hx, ← Nat.mul_sub_left_distrib, Nat.mul_div_right, zero_lt_of_ne_zero hc]
+
+theorem mul_add_mul_div_of_dvd (hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) :
+    (a * d + b * c) / (b * d) = a / b + c / d := by
+  obtain ⟨n, hn⟩ := hba
+  obtain ⟨_, hm⟩ := hdc
+  rw [hn, hm, Nat.mul_assoc b n d, Nat.mul_comm n d, ← Nat.mul_assoc, ← Nat.mul_assoc,
+    ← Nat.mul_add,
+    Nat.mul_div_right _ (zero_lt_of_ne_zero hb),
+    Nat.mul_div_right _ (zero_lt_of_ne_zero hd),
+    Nat.mul_div_right _ (zero_lt_of_ne_zero <| Nat.mul_ne_zero hb hd)]
+
+theorem mul_sub_mul_div_of_dvd (hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) :
+    (a * d - b * c) / (b * d)  = a / b - c / d := by
+  obtain ⟨n, hn⟩ := hba
+  obtain ⟨m, hm⟩ := hdc
+  rw [hn, hm]
+  rw [Nat.mul_assoc,Nat.mul_comm n d, ← Nat.mul_assoc,← Nat.mul_assoc, ← Nat.mul_sub_left_distrib,
+    Nat.mul_div_right _ (zero_lt_of_ne_zero hb), Nat.mul_div_right _ (zero_lt_of_ne_zero hd),
+    Nat.mul_div_right _ (zero_lt_of_ne_zero <| Nat.mul_ne_zero hb hd)]
+
+protected theorem div_mul_right_comm {a b : Nat} (hba : b ∣ a) (c : Nat) : a / b * c = a * c / b := by
+  rw [Nat.mul_comm, ← Nat.mul_div_assoc _ hba, Nat.mul_comm]
+
+protected theorem mul_div_right_comm {a b : Nat} (hba : b ∣ a) (c : Nat) : a * c / b = a / b * c :=
+  (Nat.div_mul_right_comm hba _).symm
+
+protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
+    a / b = c ↔ a = b * c :=
+  ⟨Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H⟩
+
+protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
+    a / b = c ↔ a = c * b := by
+  rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
+
+theorem eq_div_iff_mul_eq_left (hc : c ≠ 0) (hcb : c ∣ b) : a = b / c ↔ b = a * c := by
+  rw [eq_comm, Nat.div_eq_iff_eq_mul_left (zero_lt_of_ne_zero hc) hcb]
+
+theorem div_mul_div_comm {a b c d : Nat} : b ∣ a → d ∣ c → (a / b) * (c / d) = (a * c) / (b * d) := by
+  rintro ⟨x, rfl⟩ ⟨y, rfl⟩
+  obtain rfl | hb := b.eq_zero_or_pos
+  · simp
+  obtain rfl | hd := d.eq_zero_or_pos
+  · simp
+  rw [Nat.mul_div_cancel_left _ hb, Nat.mul_div_cancel_left _ hd, Nat.mul_assoc b,
+    Nat.mul_left_comm x, ← Nat.mul_assoc b, Nat.mul_div_cancel_left _ (Nat.mul_pos hb hd)]
+
+protected theorem mul_div_mul_comm {a b c d : Nat} (hba : b ∣ a) (hdc : d ∣ c) : a * c / (b * d) = a / b * (c / d) :=
+  (div_mul_div_comm hba hdc).symm
+
+theorem eq_zero_of_le_div (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0 :=
+  eq_zero_of_mul_le hn <| by
+    rw [Nat.mul_comm]; exact (Nat.le_div_iff_mul_le (Nat.lt_of_lt_of_le (by decide) hn)).1 h
+
+theorem div_mul_div_le_div (a b c : Nat) : a / c * b / a ≤ b / c := by
+  obtain rfl | ha := Nat.eq_zero_or_pos a
+  · simp
+  · calc
+      a / c * b / a ≤ b * a / c / a :=
+        Nat.div_le_div_right (by rw [Nat.mul_comm]; exact mul_div_le_mul_div_assoc _ _ _)
+      _ = b / c := by rw [Nat.div_div_eq_div_mul, Nat.mul_comm b, Nat.mul_comm c,
+          Nat.mul_div_mul_left _ _ ha]
+
+theorem eq_zero_of_le_div_two (h : n ≤ n / 2) : n = 0 := eq_zero_of_le_div (Nat.le_refl _) h
+
+theorem le_div_two_of_div_two_lt_sub (h : a / 2 < a - b) : b ≤ a / 2 := by
+  omega
+
+theorem div_two_le_of_sub_le_div_two (h : a - b ≤ a / 2) : a / 2 ≤ b := by
+  omega
+
+protected theorem div_le_div_of_mul_le_mul (hd : d ≠ 0) (hdc : d ∣ c) (h : a * d ≤ c * b) :
+    a / b ≤ c / d :=
+  Nat.div_le_of_le_mul <| by
+    rwa [← Nat.mul_div_assoc _ hdc, Nat.le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hd), b.mul_comm]
+
+theorem div_eq_sub_mod_div {m n : Nat} : m / n = (m - m % n) / n := by
+  obtain rfl | hn := n.eq_zero_or_pos
+  · rw [Nat.div_zero, Nat.div_zero]
+  · have : m - m % n = n * (m / n) := by
+      rw [Nat.sub_eq_iff_eq_add (Nat.mod_le _ _), Nat.add_comm, mod_add_div]
+    rw [this, mul_div_right _ hn]
+
+protected theorem eq_div_of_mul_eq_left (hc : c ≠ 0) (h : a * c = b) : a = b / c := by
+  rw [← h, Nat.mul_div_cancel _ (Nat.pos_iff_ne_zero.2 hc)]
+
+protected theorem eq_div_of_mul_eq_right (hc : c ≠ 0) (h : c * a = b) : a = b / c := by
+  rw [← h, Nat.mul_div_cancel_left _ (Nat.pos_iff_ne_zero.2 hc)]
+
+protected theorem mul_le_of_le_div (k x y : Nat) (h : x ≤ y / k) : x * k ≤ y := by
+  if hk : k = 0 then
+    rw [hk, Nat.mul_zero]; exact zero_le _
+  else
+    rwa [← le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hk)]
+
+theorem div_le_iff_le_mul_of_dvd (hb : b ≠ 0) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ c * b := by
+  obtain ⟨_, hx⟩ := hba
+  simp only [hx]
+  rw [Nat.mul_div_right _ (zero_lt_of_ne_zero hb), Nat.mul_comm]
+  exact ⟨mul_le_mul_right b, fun h ↦ Nat.le_of_mul_le_mul_right h (zero_lt_of_ne_zero hb)⟩
+
+protected theorem div_lt_div_right (ha : a ≠ 0) : a ∣ b → a ∣ c → (b / a < c / a ↔ b < c) := by
+  rintro ⟨d, rfl⟩ ⟨e, rfl⟩; simp [Nat.mul_div_cancel, Nat.pos_iff_ne_zero.2 ha]
+
+protected theorem div_lt_div_left (ha : a ≠ 0) (hba : b ∣ a) (hca : c ∣ a) :
+    a / b < a / c ↔ c < b := by
+  obtain ⟨d, hd⟩ := hba
+  obtain ⟨e, he⟩ := hca
+  rw [Nat.div_eq_of_eq_mul_right _ hd, Nat.div_eq_of_eq_mul_right _ he,
+    Nat.lt_iff_lt_of_mul_eq_mul ha hd he] <;>
+    rw [Nat.pos_iff_ne_zero] <;> rintro rfl <;> simp at * <;> contradiction
+
+theorem lt_div_iff_mul_lt_of_dvd (hc : c ≠ 0) (hcb : c ∣ b) : a < b / c ↔ a * c < b := by
+  simp [← Nat.div_lt_div_right _ _ hcb, hc, Nat.pos_iff_ne_zero, Nat.dvd_mul_left]
+
+protected theorem div_mul_div_le (a b c d : Nat) :
+    (a / b) * (c / d) ≤ (a * c) / (b * d) := by
+  if hb : b = 0 then simp [hb] else
+  if hd : d = 0 then simp [hd] else
+  have hbd : b * d ≠ 0 := Nat.mul_ne_zero hb hd
+  rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)]
+  refine Nat.le_trans (m := ((a / b) * b) * ((c / d) * d)) ?_ ?_
+  · apply Nat.le_of_eq; simp only [Nat.mul_assoc, Nat.mul_left_comm]
+  · apply Nat.mul_le_mul <;> apply div_mul_le_self
+
 /-! ### pow -/
 
 theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
@@ -802,6 +1244,74 @@ theorem le_pow {a b : Nat} (h : 0 < b) : a ≤ a ^ b := by
   rw [(show b = b - 1 + 1 by omega), Nat.pow_succ]
   exact Nat.le_mul_of_pos_left _ (Nat.pow_pos ha)
 
+protected theorem pow_lt_pow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
+  (Nat.pow_lt_pow_iff_right ha).2 h
+
+protected theorem pow_le_pow_iff_left {a b n : Nat} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b where
+  mp := by simpa only [← Nat.not_le, Decidable.not_imp_not] using (Nat.pow_lt_pow_left · hn)
+  mpr h := Nat.pow_le_pow_left h _
+
+protected theorem pow_lt_pow_iff_left {a b n : Nat} (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b := by
+  simp only [← Nat.not_le, Nat.pow_le_pow_iff_left hn]
+
+@[simp high] protected theorem pow_eq_zero {a : Nat} : ∀ {n : Nat}, a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
+  | 0 => by simp
+  | n + 1 => by rw [Nat.pow_succ, mul_eq_zero, Nat.pow_eq_zero]; omega
+
+theorem le_self_pow (hn : n ≠ 0) : ∀ a : Nat, a ≤ a ^ n
+  | 0 => zero_le _
+  | a + 1 => by simpa using Nat.pow_le_pow_right a.succ_pos (Nat.one_le_iff_ne_zero.2 hn)
+
+theorem one_le_pow (n m : Nat) (h : 0 < m) : 1 ≤ m ^ n := by simpa using Nat.pow_le_pow_left h n
+
+theorem one_lt_pow (hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n := by simpa using Nat.pow_lt_pow_left ha hn
+
+theorem two_pow_succ (n : Nat) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n := by simp [Nat.pow_succ, Nat.mul_two]
+
+theorem one_lt_pow' (n m : Nat) : 1 < (m + 2) ^ (n + 1) :=
+  one_lt_pow n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl)
+
+@[simp] theorem one_lt_pow_iff {n : Nat} (hn : n ≠ 0) : ∀ {a}, 1 < a ^ n ↔ 1 < a
+ | 0 => by simp [Nat.zero_pow (Nat.pos_of_ne_zero hn)]
+ | 1 => by simp
+ | a + 2 => by simp [one_lt_pow hn]
+
+theorem one_lt_two_pow' (n : Nat) : 1 < 2 ^ (n + 1) := one_lt_pow n.succ_ne_zero (by decide)
+
+theorem mul_lt_mul_pow_succ (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1) := by
+  rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_lt_mul_right (Nat.lt_trans Nat.zero_lt_one hb)]
+  exact Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left _ ha)
+    ((Nat.mul_lt_mul_left ha).2 <| Nat.lt_pow_self hb)
+
+
+theorem pow_two_sub_pow_two (a b : Nat) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
+  simpa [Nat.pow_succ] using Nat.mul_self_sub_mul_self_eq a b
+
+protected theorem pow_pos_iff : 0 < a ^ n ↔ 0 < a ∨ n = 0 := by
+  simp [Nat.pos_iff_ne_zero, Decidable.imp_iff_not_or]
+
+theorem pow_self_pos : 0 < n ^ n := by simp [Nat.pow_pos_iff, n.eq_zero_or_pos.symm]
+
+theorem pow_self_mul_pow_self_le : m ^ m * n ^ n ≤ (m + n) ^ (m + n) := by
+  rw [Nat.pow_add]
+  exact Nat.mul_le_mul (Nat.pow_le_pow_left (le_add_right ..) _)
+    (Nat.pow_le_pow_left (le_add_left ..) _)
+
+protected theorem pow_right_inj (ha : 1 < a) : a ^ m = a ^ n ↔ m = n := by
+  simp [Nat.le_antisymm_iff, Nat.pow_le_pow_iff_right ha]
+
+@[simp] protected theorem pow_eq_one : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
+  obtain rfl | hn := Decidable.em (n = 0)
+  · simp
+  · simpa [hn] using Nat.pow_left_inj hn (b := 1)
+
+/-- For `a > 1`, `a ^ b = a` iff `b = 1`. -/
+theorem pow_eq_self_iff {a b : Nat} (ha : 1 < a) : a ^ b = a ↔ b = 1 := by
+  rw [← Nat.pow_right_inj (m := b) ha, Nat.pow_one]
+
+@[simp] protected theorem pow_le_one_iff (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1 := by
+  rw [← Nat.not_lt, one_lt_pow_iff hn, Nat.not_lt]
+
 /-! ### log2 -/
 
 @[simp]
@@ -835,19 +1345,7 @@ theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
   | 0 => by simp
   | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
 
-/-! ### dvd -/
-
-protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
-    a = b * c := by
-  rw [← H2, Nat.mul_div_cancel' H1]
-
-protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
-    a / b = c ↔ a = b * c :=
-  ⟨Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H⟩
-
-protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
-    a / b = c ↔ a = c * b := by
-  rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
+/-! ### mod, dvd -/
 
 theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
     ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
@@ -903,48 +1401,151 @@ protected theorem div_pow {a b c : Nat} (h : a ∣ b) : (b / a) ^ c = b ^ c / a
     rw [Nat.pow_succ (b / a), Nat.pow_succ a, Nat.mul_comm _ a, Nat.mul_assoc, ← Nat.mul_assoc _ a,
       Nat.div_mul_cancel h, Nat.mul_comm b, ← Nat.mul_assoc, ← ih, Nat.pow_succ]
 
-/-! ### shiftLeft and shiftRight -/
+@[simp] theorem mod_two_not_eq_one : ¬n % 2 = 1 ↔ n % 2 = 0 := by
+  cases mod_two_eq_zero_or_one n <;> simp [*]
 
-@[simp] theorem shiftLeft_zero : n <<< 0 = n := rfl
+@[simp] theorem mod_two_not_eq_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by
+  cases mod_two_eq_zero_or_one n <;> simp [*]
 
-/-- Shiftleft on successor with multiple moved inside. -/
-theorem shiftLeft_succ_inside (m n : Nat) : m <<< (n+1) = (2*m) <<< n := rfl
+theorem mod_two_ne_one : n % 2 ≠ 1 ↔ n % 2 = 0 := mod_two_not_eq_one
+theorem mod_two_ne_zero : n % 2 ≠ 0 ↔ n % 2 = 1 := mod_two_not_eq_zero
 
-/-- Shiftleft on successor with multiple moved to outside. -/
-theorem shiftLeft_succ : ∀(m n), m <<< (n + 1) = 2 * (m <<< n)
-| _, 0 => rfl
-| _, k + 1 => by
-  rw [shiftLeft_succ_inside _ (k+1)]
-  rw [shiftLeft_succ _ k, shiftLeft_succ_inside]
+/-- Variant of `Nat.lt_div_iff_mul_lt` that assumes `d ∣ n`. -/
+protected theorem lt_div_iff_mul_lt' (hdn : d ∣ n) (a : Nat) : a < n / d ↔ d * a < n := by
+  obtain rfl | hd := d.eq_zero_or_pos
+  · simp [Nat.zero_dvd.1 hdn]
+  · rw [← Nat.mul_lt_mul_left hd, ← Nat.eq_mul_of_div_eq_right hdn rfl]
 
-/-- Shiftright on successor with division moved inside. -/
-theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
-| _, 0 => rfl
-| _, k + 1 => by
-  rw [shiftRight_succ _ (k+1)]
-  rw [shiftRight_succ_inside _ k, shiftRight_succ]
+theorem mul_div_eq_iff_dvd {n d : Nat} : d * (n / d) = n ↔ d ∣ n :=
+  calc
+    d * (n / d) = n ↔ d * (n / d) = d * (n / d) + (n % d) := by rw [div_add_mod]
+    _ ↔ d ∣ n := by rw [eq_comm, Nat.add_eq_left, dvd_iff_mod_eq_zero]
 
-@[simp] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0
-  | 0 => by simp [shiftLeft]
-  | n + 1 => by simp [shiftLeft, zero_shiftLeft n, shiftLeft_succ]
+theorem mul_div_lt_iff_not_dvd {n d : Nat} : d * (n / d) < n ↔ ¬ d ∣ n := by
+  simp [Nat.lt_iff_le_and_ne, mul_div_eq_iff_dvd, mul_div_le]
 
-@[simp] theorem zero_shiftRight : ∀ n, 0 >>> n = 0
-  | 0 => by simp [shiftRight]
-  | n + 1 => by simp [shiftRight, zero_shiftRight n, shiftRight_succ]
+theorem div_eq_iff_eq_of_dvd_dvd (hn : n ≠ 0) (ha : a ∣ n) (hb : b ∣ n) : n / a = n / b ↔ a = b := by
+  constructor <;> intro h
+  · rw [← Nat.mul_right_inj hn]
+    apply Nat.eq_mul_of_div_eq_left (Nat.dvd_trans hb (Nat.dvd_mul_right _ _))
+    rw [eq_comm, Nat.mul_comm, Nat.mul_div_assoc _ hb]
+    exact Nat.eq_mul_of_div_eq_right ha h
+  · rw [h]
 
-theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
-  | 0 => rfl
-  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]
+theorem le_iff_ne_zero_of_dvd (ha : a ≠ 0) (hab : a ∣ b) : a ≤ b ↔ b ≠ 0 where
+  mp := by rw [← Nat.pos_iff_ne_zero] at ha ⊢; exact Nat.lt_of_lt_of_le ha
+  mpr hb := Nat.le_of_dvd (Nat.pos_iff_ne_zero.2 hb) hab
 
-@[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
-  rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
+theorem div_ne_zero_iff_of_dvd (hba : b ∣ a) : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
+  obtain rfl | hb := Decidable.em (b = 0) <;>
+    simp [Nat.div_ne_zero_iff, Nat.le_iff_ne_zero_of_dvd, *]
+
+theorem pow_mod (a b n : Nat) : a ^ b % n = (a % n) ^ b % n := by
+  induction b with
+  | zero => rfl
+  | succ b ih => simp [Nat.pow_succ, Nat.mul_mod, ih]
+
+theorem lt_of_pow_dvd_right (hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b := by
+  rw [← Nat.pow_lt_pow_iff_right (succ_le_iff.1 ha)]
+  exact Nat.lt_of_le_of_lt (le_of_dvd (Nat.pos_iff_ne_zero.2 hb) h) (Nat.lt_pow_self ha)
+
+theorem div_dvd_of_dvd {n m : Nat} (h : n ∣ m) : m / n ∣ m := ⟨n, (Nat.div_mul_cancel h).symm⟩
+
+protected theorem div_div_self (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n := by
+  rcases h with ⟨_, rfl⟩
+  rw [Nat.mul_ne_zero_iff] at hm
+  rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]
+
+theorem not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
+  rintro ⟨k, rfl⟩
+  rcases Nat.eq_zero_or_pos k with (rfl | hk)
+  · exact Nat.lt_irrefl 0 h1
+  · exact Nat.not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2
+
+theorem eq_of_dvd_of_lt_two_mul (ha : a ≠ 0) (hdvd : b ∣ a) (hlt : a < 2 * b) : a = b := by
+  obtain ⟨_ | _ | c, rfl⟩ := hdvd
+  · simp at ha
+  · exact Nat.mul_one _
+  · rw [Nat.mul_comm] at hlt
+    cases Nat.not_le_of_lt hlt (Nat.mul_le_mul_right _ (by omega))
+
+theorem mod_eq_iff_lt (hn : n ≠ 0) : m % n = m ↔ m < n :=
+  ⟨fun h ↦ by rw [← h]; exact mod_lt _ <| Nat.pos_iff_ne_zero.2 hn, mod_eq_of_lt⟩
+
+@[simp]
+theorem mod_succ_eq_iff_lt {m n : Nat} : m % n.succ = m ↔ m < n.succ :=
+  mod_eq_iff_lt (succ_ne_zero _)
+
+@[simp] theorem mod_succ (n : Nat) : n % n.succ = n := mod_eq_of_lt n.lt_succ_self
+
+theorem mod_add_div' (a b : Nat) : a % b + a / b * b = a := by rw [Nat.mul_comm]; exact mod_add_div _ _
+
+theorem div_add_mod' (a b : Nat) : a / b * b + a % b = a := by rw [Nat.mul_comm]; exact div_add_mod _ _
+
+/-- See also `Nat.divModEquiv` for a similar statement as an `Equiv`. -/
+protected theorem div_mod_unique (h : 0 < b) :
+    a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b :=
+  ⟨fun ⟨e₁, e₂⟩ ↦ e₁ ▸ e₂ ▸ ⟨mod_add_div _ _, mod_lt _ h⟩, fun ⟨h₁, h₂⟩ ↦ h₁ ▸ by
+    rw [add_mul_div_left _ _ h, add_mul_mod_self_left]; simp [div_eq_of_lt, mod_eq_of_lt, h₂]⟩
+
+/-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/
+theorem sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by
+  rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, ← Nat.sub_sub,
+    Nat.add_sub_cancel_left, ← k.mul_sub, Nat.mul_mod_right]
+
+@[simp] theorem one_mod (n : Nat) : 1 % (n + 2) = 1 :=
+  Nat.mod_eq_of_lt (Nat.add_lt_add_right n.succ_pos 1)
+
+theorem one_mod_eq_one : ∀ {n : Nat}, 1 % n = 1 ↔ n ≠ 1
+  | 0 | 1 | n + 2 => by simp; try omega
+
+theorem dvd_sub_mod (k : Nat) : n ∣ k - k % n :=
+  ⟨k / n, Nat.sub_eq_of_eq_add (Nat.div_add_mod k n).symm⟩
+
+theorem add_mod_eq_ite {m n : Nat} :
+    (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k := by
+  cases k with
+  | zero => simp
+  | succ k =>
+    rw [Nat.add_mod]
+    by_cases h : k + 1 ≤ m % (k + 1) + n % (k + 1)
+    · rw [if_pos h, Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
+      exact (Nat.sub_lt_iff_lt_add h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
+        (n.mod_lt (zero_lt_succ _)))
+    · rw [if_neg h]
+      exact Nat.mod_eq_of_lt (Nat.lt_of_not_ge h)
+
+-- TODO: Replace `Nat.dvd_add_iff_left`
+protected theorem dvd_add_left {a b c : Nat} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b := (Nat.dvd_add_iff_left h).symm
+
+protected theorem dvd_add_right {a b c : Nat} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c := (Nat.dvd_add_iff_right h).symm
+
+theorem add_mod_eq_add_mod_right (c : Nat) (H : a % d = b % d) : (a + c) % d = (b + c) % d := by
+  rw [← mod_add_mod, ← mod_add_mod b, H]
+
+theorem add_mod_eq_add_mod_left (c : Nat) (H : a % d = b % d) : (c + a) % d = (c + b) % d := by
+  rw [Nat.add_comm, add_mod_eq_add_mod_right _ H, Nat.add_comm]
+
+theorem mul_dvd_of_dvd_div {a b c : Nat} (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b :=
+  have ⟨d, hd⟩ := h
+  ⟨d, by simpa [Nat.mul_comm, Nat.mul_left_comm] using Nat.eq_mul_of_div_eq_left hcb hd⟩
+
+theorem eq_of_dvd_of_div_eq_one (hab : a ∣ b) (h : b / a = 1) : a = b := by
+  rw [← Nat.div_mul_cancel hab, h, Nat.one_mul]
+
+theorem eq_zero_of_dvd_of_div_eq_zero (hab : a ∣ b) (h : b / a = 0) : b = 0 := by
+  rw [← Nat.div_mul_cancel hab, h, Nat.zero_mul]
+
+theorem lt_mul_div_succ (a : Nat) (hb : 0 < b) : a < b * (a / b + 1) := by
+  rw [Nat.mul_comm, ← Nat.div_lt_iff_lt_mul hb]
+  exact lt_succ_self _
 
 theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
   match x with
   | 0 => simp
   | x + 1 =>
     rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
-    simp +arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
+    simp +arith [m_pos]
 
 theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   match x with
@@ -952,6 +1553,13 @@ theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   | x + 1 =>
     simp [Nat.mul_succ, Nat.add_assoc _ m, mul_add_mod _ x]
 
+-- TODO: make naming and statements consistent across all variations of `mod`, `gcd` etc. across
+-- `Nat` and `Int`.
+theorem mul_add_mod' (a b c : Nat) : (a * b + c) % b = c % b := by rw [Nat.mul_comm, Nat.mul_add_mod]
+
+theorem mul_add_mod_of_lt {a b c : Nat} (h : c < b) : (a * b + c) % b = c := by
+  rw [Nat.mul_add_mod', Nat.mod_eq_of_lt h]
+
 @[simp] theorem mod_div_self (m n : Nat) : m % n / n = 0 := by
   cases n
   · exact (m % 0).div_zero
@@ -1009,6 +1617,113 @@ theorem succ_mod_succ_eq_zero_iff {a b : Nat} :
       subst h
       simp [Nat.add_mul]
 
+
+theorem dvd_iff_div_mul_eq (n d : Nat) : d ∣ n ↔ n / d * d = n :=
+  ⟨fun h => Nat.div_mul_cancel h, fun h => by rw [← h]; exact Nat.dvd_mul_left _ _⟩
+
+theorem dvd_iff_le_div_mul (n d : Nat) : d ∣ n ↔ n ≤ n / d * d :=
+  ((dvd_iff_div_mul_eq _ _).trans Nat.le_antisymm_iff).trans (and_iff_right (div_mul_le_self n d))
+
+theorem dvd_iff_dvd_dvd (n d : Nat) : d ∣ n ↔ ∀ k : Nat, k ∣ d → k ∣ n :=
+  ⟨fun h _ hkd => Nat.dvd_trans hkd h, fun h => h _ (Nat.dvd_refl _)⟩
+
+theorem dvd_div_of_mul_dvd {a b c : Nat} (h : a * b ∣ c) : b ∣ c / a :=
+  if ha : a = 0 then by simp [ha]
+  else
+    have ha : 0 < a := Nat.pos_of_ne_zero ha
+    have h1 : ∃ d, c = a * b * d := h
+    let ⟨d, hd⟩ := h1
+    have h2 : c / a = b * d := Nat.div_eq_of_eq_mul_right ha (by simpa [Nat.mul_assoc] using hd)
+    show ∃ d, c / a = b * d from ⟨d, h2⟩
+
+@[simp] theorem dvd_div_iff_mul_dvd {a b c : Nat} (hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b :=
+  ⟨fun h => mul_dvd_of_dvd_div hbc h, fun h => dvd_div_of_mul_dvd h⟩
+
+theorem dvd_mul_of_div_dvd {a b c : Nat} (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c := by
+  obtain ⟨e, rfl⟩ := hdiv
+  rw [← Nat.mul_assoc, Nat.mul_comm _ (a / b), Nat.div_mul_cancel h]
+  exact Nat.dvd_mul_right a e
+
+@[simp] theorem div_div_div_eq_div {a b c : Nat} (dvd : b ∣ a) (dvd2 : a ∣ c) : c / (a / b) / b = c / a :=
+  match a, b, c with
+  | 0, _, _ => by simp
+  | a + 1, 0, _ => by simp at dvd
+  | a + 1, c + 1, _ => by
+    have a_split : a + 1 ≠ 0 := succ_ne_zero a
+    have c_split : c + 1 ≠ 0 := succ_ne_zero c
+    rcases dvd2 with ⟨k, rfl⟩
+    rcases dvd with ⟨k2, pr⟩
+    have k2_nonzero : k2 ≠ 0 := fun k2_zero => by simp [k2_zero] at pr
+    rw [Nat.mul_div_cancel_left k (Nat.pos_of_ne_zero a_split), pr,
+      Nat.mul_div_cancel_left k2 (Nat.pos_of_ne_zero c_split), Nat.mul_comm ((c + 1) * k2) k, ←
+      Nat.mul_assoc k (c + 1) k2, Nat.mul_div_cancel _ (Nat.pos_of_ne_zero k2_nonzero),
+      Nat.mul_div_cancel _ (Nat.pos_of_ne_zero c_split)]
+
+/-- If a small natural number is divisible by a larger natural number,
+the small number is zero. -/
+theorem eq_zero_of_dvd_of_lt (w : a ∣ b) (h : b < a) : b = 0 :=
+  Nat.eq_zero_of_dvd_of_div_eq_zero w (by simp [h])
+
+theorem le_of_lt_add_of_dvd {a b : Nat} (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b := by
+  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
+  rw [← mul_succ] at h
+  exact Nat.mul_le_mul_left _ (Nat.lt_succ_iff.1 <| Nat.lt_of_mul_lt_mul_left h)
+
+/-- `m` is not divisible by `n` if it is between `n * k` and `n * (k + 1)` for some `k`. -/
+theorem not_dvd_of_lt_of_lt_mul_succ (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m := by
+  rintro ⟨d, rfl⟩
+  have := Nat.lt_of_mul_lt_mul_left h1
+  have := Nat.lt_of_mul_lt_mul_left h2
+  omega
+
+/-- `n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`. -/
+theorem not_dvd_iff_lt_mul_succ (n : Nat) {a : Nat} (ha : 0 < a) :
+    ¬a ∣ n ↔ (∃ k : Nat, a * k < n ∧ n < a * (k + 1)) := by
+  refine Iff.symm
+    ⟨fun ⟨k, hk1, hk2⟩ => not_dvd_of_lt_of_lt_mul_succ hk1 hk2, fun han =>
+      ⟨n / a, ⟨Nat.lt_of_le_of_ne (mul_div_le n a) ?_, lt_mul_div_succ _ ha⟩⟩⟩
+  exact mt (⟨n / a, Eq.symm ·⟩) han
+
+theorem div_lt_div_of_lt_of_dvd {a b d : Nat} (hdb : d ∣ b) (h : a < b) : a / d < b / d := by
+  rw [Nat.lt_div_iff_mul_lt' hdb]
+  exact Nat.lt_of_le_of_lt (mul_div_le a d) h
+
+/-! ### shiftLeft and shiftRight -/
+
+@[simp] theorem shiftLeft_zero : n <<< 0 = n := rfl
+
+/-- Shiftleft on successor with multiple moved inside. -/
+theorem shiftLeft_succ_inside (m n : Nat) : m <<< (n+1) = (2*m) <<< n := rfl
+
+/-- Shiftleft on successor with multiple moved to outside. -/
+theorem shiftLeft_succ : ∀(m n), m <<< (n + 1) = 2 * (m <<< n)
+| _, 0 => rfl
+| _, k + 1 => by
+  rw [shiftLeft_succ_inside _ (k+1)]
+  rw [shiftLeft_succ _ k, shiftLeft_succ_inside]
+
+/-- Shiftright on successor with division moved inside. -/
+theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
+| _, 0 => rfl
+| _, k + 1 => by
+  rw [shiftRight_succ _ (k+1)]
+  rw [shiftRight_succ_inside _ k, shiftRight_succ]
+
+@[simp] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0
+  | 0 => by simp [shiftLeft]
+  | n + 1 => by simp [shiftLeft, zero_shiftLeft n, shiftLeft_succ]
+
+@[simp] theorem zero_shiftRight : ∀ n, 0 >>> n = 0
+  | 0 => by simp [shiftRight]
+  | n + 1 => by simp [shiftRight, zero_shiftRight n, shiftRight_succ]
+
+theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
+  | 0 => rfl
+  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]
+
+@[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
+  rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
+
 /-! ### Decidability of predicates -/
 
 instance decidableBallLT :
diff --git a/src/Init/Data/Nat/MinMax.lean b/src/Init/Data/Nat/MinMax.lean
index 878447ab4c..608520fd93 100644
--- a/src/Init/Data/Nat/MinMax.lean
+++ b/src/Init/Data/Nat/MinMax.lean
@@ -52,8 +52,8 @@ protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
 protected theorem min_le_left (a b : Nat) : min a b ≤ a :=
   Nat.min_comm .. ▸ Nat.min_le_right ..
 
-protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
-protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b :=
+@[simp] protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
+@[simp] protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b :=
   Nat.min_comm .. ▸ Nat.min_eq_left h
 
 protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
@@ -111,9 +111,9 @@ protected theorem le_max_left (a b : Nat) : a ≤ max a b := by
 protected theorem le_max_right (a b : Nat) : b ≤ max a b :=
    Nat.max_comm .. ▸ Nat.le_max_left ..
 
-protected theorem max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b := if_pos h
+@[simp] protected theorem max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b := if_pos h
 
-protected theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a :=
+@[simp] protected theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a :=
   Nat.max_comm .. ▸ Nat.max_eq_right h
 
 protected theorem max_le_of_le_of_le {a b c : Nat} : a ≤ c → b ≤ c → max a b ≤ c := by
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index e192d11c7c..8e759da832 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -1666,7 +1666,7 @@ theorem USize.toUInt32_eq (a b : USize) : a.toUInt32 = b.toUInt32 ↔ a % 429496
   simp [← UInt32.toNat_inj, ← USize.toNat_inj, USize.toNat_ofNat]
   have := Nat.mod_eq_of_lt a.toNat_lt_two_pow_numBits
   have := Nat.mod_eq_of_lt b.toNat_lt_two_pow_numBits
-  cases System.Platform.numBits_eq <;> simp_all
+  cases System.Platform.numBits_eq <;> simp_all [Nat.mod_eq_of_lt]
 
 theorem UInt8.toUInt16_eq_mod_256_iff (a : UInt8) (b : UInt16) : a.toUInt16 = b % 256 ↔ a = b.toUInt8 := by
   simp [← UInt8.toNat_inj, ← UInt16.toNat_inj]
@@ -1689,7 +1689,7 @@ theorem UInt32.toUInt64_eq_mod_4294967296_iff (a : UInt32) (b : UInt64) : a.toUI
 theorem UInt32.toUSize_eq_mod_4294967296_iff (a : UInt32) (b : USize) : a.toUSize = b % 4294967296 ↔ a = b.toUInt32 := by
   simp [← UInt32.toNat_inj, ← USize.toNat_inj, USize.toNat_ofNat]
   have := Nat.mod_eq_of_lt b.toNat_lt_two_pow_numBits
-  cases System.Platform.numBits_eq <;> simp_all
+  cases System.Platform.numBits_eq <;> simp_all [Nat.mod_eq_of_lt]
 
 theorem USize.toUInt64_eq_mod_usizeSize_iff (a : USize) (b : UInt64) : a.toUInt64 = b % UInt64.ofNat USize.size ↔ a = b.toUSize := by
   simp [← USize.toNat_inj, ← UInt64.toNat_inj, USize.size_eq_two_pow]
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 2573a27009..283841a427 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -1717,12 +1717,12 @@ theorem append_eq_append_iff {ws : Vector α n} {xs : Vector α m} {ys : Vector
   constructor
   · rintro (⟨as, rfl, rfl⟩ | ⟨cs, rfl, rfl⟩)
     · rw [dif_pos (by simp)]
-      exact ⟨as.toVector.cast (by simp; omega), by simp⟩
+      exact ⟨as.toVector.cast (by simp), by simp⟩
     · split <;> rename_i h
       · have hc : cs.size = 0 := by simp at h; omega
         simp at hc
-        exact ⟨#v[].cast (by simp; omega), by simp_all⟩
-      · exact ⟨cs.toVector.cast (by simp; omega), by simp⟩
+        exact ⟨#v[].cast (by simp), by simp_all⟩
+      · exact ⟨cs.toVector.cast (by simp), by simp⟩
   · split <;> rename_i h
     · rintro ⟨as, hc, rfl⟩
       left
diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean
index 52e4cf7776..dd1e58517e 100644
--- a/src/Init/Data/Vector/Range.lean
+++ b/src/Init/Data/Vector/Range.lean
@@ -101,9 +101,8 @@ theorem range'_eq_append_iff : range' s (n + m) = xs ++ ys ↔ xs = range' s n 
       simp_all
     subst w
     simp_all
-    omega
   · rintro ⟨h₁, h₂⟩
-    exact ⟨n, by omega, by simp_all; omega⟩
+    exact ⟨n, by omega, by simp_all⟩
 
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean
index 5ed3e54047..dee14797ca 100644
--- a/src/Lean/Data/RArray.lean
+++ b/src/Lean/Data/RArray.lean
@@ -54,7 +54,7 @@ theorem RArray.size_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) :
 where
   go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
     induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n)
-    case case1 => simp [ofFn.go, size]; omega
+    case case1 => simp [ofFn.go, size]
     case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
 
 section Meta
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 70adc16292..5cea7afb31 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -78,7 +78,7 @@ private theorem invert_eq_testBit (f : Fanin) : f.invert = f.val.testBit 0 := by
 
 @[simp]
 theorem invert_flip (f : Fanin) : (f.flip v).invert = f.invert ^^ v := by
-  cases v <;> simp [flip, invert_eq_testBit]
+  cases v <;> simp [flip, invert_eq_testBit, -Nat.mod_two_not_eq_one]
 
 end Fanin
 
diff --git a/tests/lean/run/2669.lean b/tests/lean/run/2669.lean
index acaab3c0af..75d6e505bc 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, -Nat.add_left_eq_self] -- Should not succeed
+    fail_if_success simp (config := { zeta := false }) [Nat.zero_add, -Nat.add_eq_right] -- Should not succeed
     simp [g]
   sorry
 
diff --git a/tests/lean/run/4290.lean b/tests/lean/run/4290.lean
index 1c69f49fbb..a54329c9d5 100644
--- a/tests/lean/run/4290.lean
+++ b/tests/lean/run/4290.lean
@@ -1,4 +1,4 @@
-attribute [-simp] Nat.self_eq_add_right -- This was later added to the simp set and interfere with the test.
+attribute [-simp] Nat.left_eq_add -- 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/array_simp.lean b/tests/lean/run/array_simp.lean
index 51e772b27d..ad5c6da7df 100644
--- a/tests/lean/run/array_simp.lean
+++ b/tests/lean/run/array_simp.lean
@@ -1,3 +1,5 @@
+attribute [-simp] Nat.default_eq_zero -- undo changes to simp set after this test was written
+
 #check_simp #[1,2,3,4,5][2]  ~> 3
 #check_simp #[1,2,3,4,5][2]? ~> some 3
 #check_simp #[1,2,3,4,5][7]? ~> none
diff --git a/tests/lean/run/grind_eval_suggest.lean b/tests/lean/run/grind_eval_suggest.lean
index dced961fbc..31676466ad 100644
--- a/tests/lean/run/grind_eval_suggest.lean
+++ b/tests/lean/run/grind_eval_suggest.lean
@@ -26,7 +26,7 @@ example (x : Nat) : 1 + 1 + f x = x + 2 := by
 info: Try these:
 • rfl
 • simp
-• simp only [Nat.succ_eq_add_one]
+• simp only [Nat.succ_eq_add_one, Nat.add_left_cancel_iff]
 • grind
 • grind only
 -/
@@ -38,7 +38,7 @@ example (x : Nat) : x + 1 = Nat.succ x := by
 info: Try these:
 • · intros; rfl
 • · intros; simp
-• · intros; simp only [Nat.succ_eq_add_one]
+• · intros; simp only [Nat.succ_eq_add_one, Nat.add_left_cancel_iff]
 • · intros; grind
 • · intros; grind only
 -/
diff --git a/tests/lean/run/implicitRflProofs.lean b/tests/lean/run/implicitRflProofs.lean
index aecadfbb8c..bdc3ee73a2 100644
--- a/tests/lean/run/implicitRflProofs.lean
+++ b/tests/lean/run/implicitRflProofs.lean
@@ -3,7 +3,7 @@ def f (x : Nat) := x + 1
 theorem f_eq (x : Nat) : f (x + 1) = x + 2 := rfl
 
 theorem ex1 : f (f (x + 1)) = x + 3 := by
-  simp -implicitDefEqProofs [f_eq]
+  simp -implicitDefEqProofs only [f_eq]
 
 /--
 info: theorem ex1 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
@@ -15,7 +15,7 @@ fun {x} =>
 #print ex1
 
 theorem ex2 : f (f (x + 1)) = x + 3 := by
-  simp +implicitDefEqProofs [f_eq]
+  simp +implicitDefEqProofs only [f_eq]
 
 /--
 info: theorem ex2 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
diff --git a/tests/lean/run/letDeclSimp.lean b/tests/lean/run/letDeclSimp.lean
index 9284f3fc24..d226461323 100644
--- a/tests/lean/run/letDeclSimp.lean
+++ b/tests/lean/run/letDeclSimp.lean
@@ -1,4 +1,4 @@
-attribute [-simp] Nat.add_left_eq_self -- This was later added to the simp set and interfere with the test.
+attribute [-simp] Nat.add_eq_right -- 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
diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean
index cce6c8cdf7..dc7773a204 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 [-Nat.add_eq_zero_iff]
+  fail_if_success simp [-Nat.add_eq_zero]
   intro h₁ h₂
   simp [h₁] at h₂
   simp [h₂]
diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean
index d39ba1dd14..669dd3988e 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 [*, -Nat.add_eq_zero_iff] at *
+  simp [*, -Nat.add_eq_zero] at *
   trace_state
   have aux₁ : f x x = g x := h₁
   have aux₂ : g x < 5     := h₂
diff --git a/tests/lean/simp_trace.lean b/tests/lean/simp_trace.lean
index 71e7df49e5..cc7f202640 100644
--- a/tests/lean/simp_trace.lean
+++ b/tests/lean/simp_trace.lean
@@ -1,6 +1,9 @@
 set_option tactic.simp.trace true
 set_option trace.Meta.Tactic.simp.rewrite true
 
+-- These lemmas were subsequently added to the simp set and confuse the test.
+attribute [-simp] Nat.add_left_cancel_iff Nat.add_right_cancel_iff Nat.sub_eq_zero_of_le Nat.add_eq_left Nat.add_eq_right
+
 def f (x : α) := x
 
 example (a : α) (b : List α) : f (a::b = []) = False :=
@@ -84,8 +87,6 @@ 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
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 76052c680e..d8552c4d0d 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -96,7 +96,7 @@ Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
     ==>
       x
 [Meta.Tactic.simp.rewrite] eq_self:1000: x = x ==> True
-simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
+simp_trace.lean:86:0-86:7: warning: declaration uses 'sorry'
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
@@ -108,7 +108,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:102:101-103:40: error: unsolved goals
+simp_trace.lean:103:101-104:40: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α
@@ -121,7 +121,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:106:101-107:53: error: unsolved goals
+simp_trace.lean:107:101-108:53: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α
diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean
index 60e603dd4d..9b3862f403 100644
--- a/tests/pkg/user_attr/UserAttr/Tst.lean
+++ b/tests/pkg/user_attr/UserAttr/Tst.lean
@@ -1,6 +1,8 @@
 import Lean
 import UserAttr.BlaAttr
 
+attribute [-simp] Nat.add_left_cancel_iff Nat.add_right_cancel_iff
+
 @[bla] def f (x : Nat) := x + 2
 @[bla] def g (x : Nat) := x + 1