diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
index f494896c8babcc..4487c276edcb9e 100644
--- a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -6,6 +6,9 @@ Authors: Mario Carneiro
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Data.List.BigOperators.Basic
 import Mathlib.Data.Multiset.Basic
+import Mathlib.Algebra.GroupPower.Hom
+import Mathlib.Algebra.GroupWithZero.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 
 #align_import algebra.big_operators.multiset.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
 
diff --git a/Mathlib/Computability/Ackermann.lean b/Mathlib/Computability/Ackermann.lean
index fdbea9d4bfbce2..c0cd631f9d903d 100644
--- a/Mathlib/Computability/Ackermann.lean
+++ b/Mathlib/Computability/Ackermann.lean
@@ -7,6 +7,7 @@ import Mathlib.Computability.Primrec
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Linarith
 import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Data.Nat.Pow
 
 #align_import computability.ackermann from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
 
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
index 475ca454d2151f..2679fbca093f44 100644
--- a/Mathlib/Data/Finset/Basic.lean
+++ b/Mathlib/Data/Finset/Basic.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Multiset.FinsetOps
 import Mathlib.Data.Set.Lattice
+import Mathlib.Algebra.Order.WithZero
 
 #align_import data.finset.basic from "leanprover-community/mathlib"@"442a83d738cb208d3600056c489be16900ba701d"
 
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index 313e0ffc71abc6..2fad4b05004ea2 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/Basic.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Fin.OrderHom
+import Mathlib.Algebra.Ring.Hom.Defs
 
 #align_import data.fintype.basic from "leanprover-community/mathlib"@"d78597269638367c3863d40d45108f52207e03cf"
 
diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
index 1a5f6574dedcfd..621d2cdfa17495 100644
--- a/Mathlib/Data/Multiset/Basic.lean
+++ b/Mathlib/Data/Multiset/Basic.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Data.Set.List
 import Mathlib.Data.List.Perm
 import Mathlib.Init.Quot -- Porting note: added import
+import Mathlib.Order.Hom.Basic
 
 #align_import data.multiset.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
diff --git a/Mathlib/Data/Multiset/Nodup.lean b/Mathlib/Data/Multiset/Nodup.lean
index 4cbd6db9a39db9..c557adea48fcd2 100644
--- a/Mathlib/Data/Multiset/Nodup.lean
+++ b/Mathlib/Data/Multiset/Nodup.lean
@@ -7,6 +7,7 @@ import Mathlib.Data.List.Nodup
 import Mathlib.Data.Multiset.Bind
 import Mathlib.Data.Multiset.Range
 import Mathlib.Data.List.Range
+import Mathlib.Init.Classical
 
 #align_import data.multiset.nodup from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
 
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 6c35936e40bd6e..e538702f8de2ca 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Bhavik Mehta, Stuart Presnell
 -/
 import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Algebra.Divisibility.Basic
+import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Data.Nat.Order.Basic
 
 #align_import data.nat.choose.basic from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
 
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
index 3505c8e19010f1..0149d754ec8cd4 100644
--- a/Mathlib/Data/Nat/Defs.lean
+++ b/Mathlib/Data/Nat/Defs.lean
@@ -91,13 +91,7 @@ alias ⟨of_le_succ, _⟩ := le_succ_iff
 #align nat.of_le_succ Nat.of_le_succ
 
 #align nat.lt_succ_iff_lt_or_eq Nat.lt_succ_iff_lt_or_eq
-
-lemma eq_of_lt_succ_of_not_lt (hmn : m < n + 1) (h : ¬ m < n) : m = n :=
-  (Nat.lt_succ_iff_lt_or_eq.1 hmn).resolve_left h
 #align nat.eq_of_lt_succ_of_not_lt Nat.eq_of_lt_succ_of_not_lt
-
-lemma eq_of_le_of_lt_succ (h₁ : n ≤ m) (h₂ : m < n + 1) : m = n :=
-  Nat.le_antisymm (le_of_succ_le_succ h₂) h₁
 #align nat.eq_of_le_of_lt_succ Nat.eq_of_le_of_lt_succ
 
 lemma lt_iff_le_pred : ∀ {n}, 0 < n → (m < n ↔ m ≤ n - 1) | _ + 1, _ => Nat.lt_succ_iff
@@ -219,14 +213,8 @@ lemma pred_add_self (n : ℕ) : pred n + n = (2 * n).pred := sub_one_add_self n
 @[simp] lemma add_def : Nat.add m n = m + n := rfl
 #align nat.add_def Nat.add_def
 
-lemma exists_eq_add_of_le (h : m ≤ n) : ∃ k : ℕ, n = m + k := ⟨n - m, (add_sub_of_le h).symm⟩
 #align nat.exists_eq_add_of_le Nat.exists_eq_add_of_le
-
-lemma exists_eq_add_of_le' (h : m ≤ n) : ∃ k : ℕ, n = k + m := ⟨n - m, (Nat.sub_add_cancel h).symm⟩
 #align nat.exists_eq_add_of_le' Nat.exists_eq_add_of_le'
-
-lemma exists_eq_add_of_lt (h : m < n) : ∃ k : ℕ, n = m + k + 1 :=
-  ⟨n - (m + 1), by rw [Nat.add_right_comm, add_sub_of_le h]⟩
 #align nat.exists_eq_add_of_lt Nat.exists_eq_add_of_lt
 
 /-! ### `mul` -/
@@ -632,11 +620,6 @@ protected lemma mul_dvd_mul_iff_right (hc : 0 < c) : a * c ∣ b * c ↔ a ∣ b
 #align nat.mul_dvd_mul_iff_right Nat.mul_dvd_mul_iff_right
 
 #align nat.dvd_one Nat.dvd_one
-
-@[simp] lemma mod_mod_of_dvd (a : ℕ) (h : c ∣ b) : a % b % c = a % c := by
-  conv_rhs => rw [← mod_add_div a b]
-  obtain ⟨x, rfl⟩ := h
-  rw [Nat.mul_assoc, add_mul_mod_self_left]
 #align nat.mod_mod_of_dvd Nat.mod_mod_of_dvd
 
 -- Moved to Std
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index 510cc860956c26..bce764404fec3b 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -136,13 +136,13 @@ theorem digits_def' :
 @[simp]
 theorem digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : digits b x = [x] := by
   rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
-  rcases exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
+  rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
   rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
 #align nat.digits_of_lt Nat.digits_of_lt
 
 theorem digits_add (b : ℕ) (h : 1 < b) (x y : ℕ) (hxb : x < b) (hxy : x ≠ 0 ∨ y ≠ 0) :
     digits b (x + b * y) = x :: digits b y := by
-  rcases exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
+  rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
   cases y
   · simp [hxb, hxy.resolve_right (absurd rfl)]
   dsimp [digits]
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 0a2e5efffc86fd..6336b2867b8196 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -3,9 +3,9 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Chris Hughes, Floris van Doorn, Yaël Dillies
 -/
-import Mathlib.Data.Nat.Pow
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.Common
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import data.nat.factorial.basic from "leanprover-community/mathlib"@"d012cd09a9b256d870751284dd6a29882b0be105"
 
diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean
index 22ca772ae4e4ef..0f32d6746429f2 100644
--- a/Mathlib/Data/Nat/Pow.lean
+++ b/Mathlib/Data/Nat/Pow.lean
@@ -24,8 +24,6 @@ variable {m n x y : ℕ}
 
 -- The global `pow_le_pow_left` needs an extra hypothesis `0 ≤ x`.
 
-protected alias pow_le_pow_left := pow_le_pow_of_le_left
-protected alias pow_le_pow_right := pow_le_pow_of_le_right
 #align nat.pow_le_pow_of_le_left Nat.pow_le_pow_left
 #align nat.pow_le_pow_of_le_right Nat.pow_le_pow_right
 
@@ -34,9 +32,6 @@ protected theorem pow_lt_pow_left (h : x < y) (hn : n ≠ 0) : x ^ n < y ^ n :=
 #align nat.pow_lt_pow_of_lt_left Nat.pow_lt_pow_left
 
 #align nat.pow_lt_pow_of_lt_right pow_lt_pow_right
-
-theorem pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) : p ^ n < p ^ (n + 1) :=
-  pow_lt_pow_right h n.lt_succ_self
 #align nat.pow_lt_pow_succ Nat.pow_lt_pow_succ
 
 theorem le_self_pow {n : ℕ} (hn : n ≠ 0) : ∀ m : ℕ, m ≤ m ^ n
@@ -49,7 +44,7 @@ theorem lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n
   | n + 1 =>
     calc
       n + 1 < p ^ n + 1 := Nat.add_lt_add_right (lt_pow_self h _) _
-      _ ≤ p ^ (n + 1) := pow_lt_pow_succ h _
+      _ ≤ p ^ (n + 1) := Nat.pow_lt_pow_succ h
 #align nat.lt_pow_self Nat.lt_pow_self
 
 theorem lt_two_pow (n : ℕ) : n < 2 ^ n :=
@@ -171,26 +166,8 @@ theorem mod_pow_succ {b : ℕ} (w m : ℕ) : m % b ^ succ w = b * (m / b % b ^ w
         rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
 #align nat.mod_pow_succ Nat.mod_pow_succ
 
-theorem pow_dvd_pow_iff_pow_le_pow {k l : ℕ} : ∀ {x : ℕ}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
-  | x + 1, w => by
-    constructor
-    · intro a
-      exact le_of_dvd (pow_pos (succ_pos x) l) a
-    · intro a
-      cases' x with x
-      · simp
-      · have le := (pow_le_pow_iff_right <| by simp).mp a
-        use (x + 2) ^ (l - k)
-        rw [← pow_add, add_comm k, tsub_add_cancel_of_le le]
 #align nat.pow_dvd_pow_iff_pow_le_pow Nat.pow_dvd_pow_iff_pow_le_pow
-
-/-- If `1 < x`, then `x^k` divides `x^l` if and only if `k` is at most `l`. -/
-theorem pow_dvd_pow_iff_le_right {x k l : ℕ} (w : 1 < x) : x ^ k ∣ x ^ l ↔ k ≤ l := by
-  rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), pow_le_pow_iff_right w]
 #align nat.pow_dvd_pow_iff_le_right Nat.pow_dvd_pow_iff_le_right
-
-theorem pow_dvd_pow_iff_le_right' {b k l : ℕ} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l :=
-  pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl)
 #align nat.pow_dvd_pow_iff_le_right' Nat.pow_dvd_pow_iff_le_right'
 
 theorem not_pos_pow_dvd : ∀ {p k : ℕ} (_ : 1 < p) (_ : 1 < k), ¬p ^ k ∣ p
diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean
index 6f6756661dcf35..781edc1a500cac 100644
--- a/Mathlib/NumberTheory/Padics/Hensel.lean
+++ b/Mathlib/NumberTheory/Padics/Hensel.lean
@@ -321,7 +321,7 @@ private theorem newton_seq_dist_aux (n : ℕ) :
 
 private theorem newton_seq_dist {n k : ℕ} (hnk : n ≤ k) :
     ‖newton_seq k - newton_seq n‖ ≤ ‖F.derivative.eval a‖ * T ^ 2 ^ n := by
-  have hex : ∃ m, k = n + m := exists_eq_add_of_le hnk
+  have hex : ∃ m, k = n + m := Nat.exists_eq_add_of_le hnk
   let ⟨_, hex'⟩ := hex
   rw [hex']; apply newton_seq_dist_aux
 
diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean
index 3f34b8c13bd7ea..5570e03a5ae828 100644
--- a/Mathlib/NumberTheory/Padics/RingHoms.lean
+++ b/Mathlib/NumberTheory/Padics/RingHoms.lean
@@ -272,7 +272,7 @@ This coercion is only a ring homomorphism if it coerces into a ring whose charac
 theorem toZMod_spec : x - (ZMod.cast (toZMod x) : ℤ_[p]) ∈ maximalIdeal ℤ_[p] := by
   convert sub_zmodRepr_mem x using 2
   dsimp [toZMod, toZModHom]
-  rcases exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
+  rcases Nat.exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
   change ↑((_ : ZMod (0 + p' + 1)).val) = (_ : ℤ_[0 + p' + 1])
   simp only [ZMod.val_nat_cast, add_zero, add_def, Nat.cast_inj, zero_add]
   apply mod_eq_of_lt
diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean
index d51b91d51b1f7d..f2adc86a68df11 100644
--- a/Mathlib/RingTheory/Multiplicity.lean
+++ b/Mathlib/RingTheory/Multiplicity.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Associated
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Nat.PartENat
 import Mathlib.Tactic.Linarith
+import Mathlib.Data.Nat.Pow
 
 #align_import ring_theory.multiplicity from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 09eabe1856b373..fd41c2f6dec4bb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "5ab4d12ec8b6fc5292e325a9eed81a4bdb984464",
+   "rev": "ab1d0228d1f6769f25aa6af0d9c7ce45109d07ee",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/scripts/noshake.json b/scripts/noshake.json
index 637f77703d6e2b..4fc79910cf2234 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -320,4 +320,5 @@
   "Mathlib.Algebra.Module.LinearMap": ["Mathlib.Algebra.Star.Basic"],
   "Mathlib.Algebra.Homology.ModuleCat": ["Mathlib.Algebra.Homology.Homotopy"],
   "Mathlib.Algebra.Category.Ring.Basic":
-  ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"]}}
+  ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],
+  "Mathlib.Init.Data.Int.Basic": ["Std.Data.Int.Order"]}}