diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean
index fc6187cf6af54..6a703ff69fc2f 100644
--- a/Mathlib/Data/BitVec/Lemmas.lean
+++ b/Mathlib/Data/BitVec/Lemmas.lean
@@ -161,19 +161,6 @@ variable (x y : BitVec w)
 @[simp] lemma toFin_neg : toFin (-x) = -(toFin x) := by
   rw [neg_eq_zero_sub]; rfl
 
-@[simp] lemma toFin_and : toFin (x &&& y) = toFin x &&& toFin y := by
-  apply toFin_inj.mpr; simp only [ofFin_and]
-
-@[simp] lemma toFin_or  : toFin (x ||| y) = toFin x ||| toFin y := by
-  apply toFin_inj.mpr; simp only [ofFin_or]
-
-@[simp] lemma toFin_xor : toFin (x ^^^ y) = toFin x ^^^ toFin y := by
-  apply toFin_inj.mpr; simp only [ofFin_xor]
-
-@[simp] lemma toFin_add : toFin (x + y)   = toFin x + toFin y   := rfl
-@[simp] lemma toFin_sub : toFin (x - y)   = toFin x - toFin y   := rfl
-@[simp] lemma toFin_mul : toFin (x * y)   = toFin x * toFin y   := rfl
-
 -- These should be simp, but Std's simp-lemmas do not allow this yet.
 lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl
 lemma toFin_one  : toFin (1 : BitVec w) = 1 := by
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index d9efed9d0bb97..33ae4df889c10 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -5,7 +5,7 @@ Authors: Markus Himmel, Alex Keizer
 -/
 import Mathlib.Data.List.GetD
 import Mathlib.Data.Nat.Bits
-import Mathlib.Data.Nat.Pow
+import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Tactic.Set
 
 #align_import data.nat.bitwise from "leanprover-community/mathlib"@"6afc9b06856ad973f6a2619e3e8a0a8d537a58f2"
@@ -281,7 +281,7 @@ theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = f
   · rw [Nat.div_eq_of_lt]
     · simp
     · exact pow_lt_pow_right one_lt_two hm
-  · rw [pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)]
+  · rw [Nat.pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)]
     -- Porting note: XXX why does this make it work?
     rw [(rfl : succ 0 = 1)]
     simp [pow_succ, and_one_is_mod, mul_mod_left]
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
index 0149d754ec8cd..546c5aaca13eb 100644
--- a/Mathlib/Data/Nat/Defs.lean
+++ b/Mathlib/Data/Nat/Defs.lean
@@ -323,16 +323,8 @@ lemma mul_div_le_mul_div_assoc (a b c : ℕ) : a * (b / c) ≤ a * b / c :=
       (by rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _))
 #align nat.mul_div_le_mul_div_assoc Nat.mul_div_le_mul_div_assoc
 
-protected lemma eq_mul_of_div_eq_right (H1 : b ∣ a) (H2 : a / b = c) : a = b * c := by
-  rw [← H2, Nat.mul_div_cancel' H1]
 #align nat.eq_mul_of_div_eq_right Nat.eq_mul_of_div_eq_right
-
-protected lemma div_eq_iff_eq_mul_right (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⟩
 #align nat.div_eq_iff_eq_mul_right Nat.div_eq_iff_eq_mul_right
-
-protected lemma div_eq_iff_eq_mul_left (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'
 #align nat.div_eq_iff_eq_mul_left Nat.div_eq_iff_eq_mul_left
 
 protected lemma eq_mul_of_div_eq_left (H1 : b ∣ a) (H2 : a / b = c) : a = c * b := by
diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean
index 0f32d6746429f..84e935ef4729f 100644
--- a/Mathlib/Data/Nat/Pow.lean
+++ b/Mathlib/Data/Nat/Pow.lean
@@ -182,16 +182,8 @@ theorem not_pos_pow_dvd : ∀ {p k : ℕ} (_ : 1 < p) (_ : 1 < k), ¬p ^ k ∣ p
     absurd this (by decide)
 #align nat.not_pos_pow_dvd Nat.not_pos_pow_dvd
 
-theorem pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n ∣ k) : p ^ m ∣ k :=
-  (pow_dvd_pow _ hmn).trans hdiv
 #align nat.pow_dvd_of_le_of_pow_dvd Nat.pow_dvd_of_le_of_pow_dvd
-
-theorem dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣ m := by
-  rw [← pow_one p]; exact pow_dvd_of_le_of_pow_dvd hk hpk
 #align nat.dvd_of_pow_dvd Nat.dvd_of_pow_dvd
-
-theorem pow_div {x m n : ℕ} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n) := by
-  rw [Nat.div_eq_iff_eq_mul_left (pow_pos hx n) (pow_dvd_pow _ h), pow_sub_mul_pow _ h]
 #align nat.pow_div Nat.pow_div
 
 theorem lt_of_pow_dvd_right {p i n : ℕ} (hn : n ≠ 0) (hp : 2 ≤ p) (h : p ^ i ∣ n) : i < n := by
diff --git a/lake-manifest.json b/lake-manifest.json
index 394ae53b75a34..7b7c35725f36e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ab1d0228d1f6769f25aa6af0d9c7ce45109d07ee",
+   "rev": "868bf6609ed0598105a3ff07e89394244ab1fa15",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "34ec89eb1c757f6f74329697d8bc4dc55377a7bb",
+   "rev": "e4660fa21444bcfe5c70d37b09cc0517accd8ad7",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",