diff --git a/Std/Data/BitVec/Basic.lean b/Std/Data/BitVec/Basic.lean
index 900a8aa486..3dade7fdb3 100644
--- a/Std/Data/BitVec/Basic.lean
+++ b/Std/Data/BitVec/Basic.lean
@@ -44,7 +44,7 @@ namespace BitVec
 /-- The `BitVec` with value `i mod 2^n`. Treated as an operation on bitvectors,
 this is truncation of the high bits when downcasting and zero-extension when upcasting. -/
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin := Fin.ofNat' i (Nat.pow_two_pos n)
+  toFin := Fin.ofNat' i (Nat.two_pow_pos n)
 
 /-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a
 (zero-cost) wrapper around a `Nat`. -/
@@ -67,7 +67,7 @@ protected def toInt (a : BitVec n) : Int :=
   if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
 
 /-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
-protected def zero (n : Nat) : BitVec n := ⟨0, Nat.pow_two_pos n⟩
+protected def zero (n : Nat) : BitVec n := ⟨0, Nat.two_pow_pos n⟩
 
 instance : Inhabited (BitVec n) where default := .zero n
 
@@ -341,9 +341,9 @@ SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value.
 def ushiftRight (a : BitVec n) (s : Nat) : BitVec n :=
   ⟨a.toNat >>> s, by
   let ⟨a, lt⟩ := a
-  simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.pow_two_pos s)]
+  simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)]
   rw [←Nat.mul_one a]
-  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.pow_two_pos s) (Nat.le_refl 1)⟩
+  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1)⟩
 
 instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩
 
@@ -397,7 +397,7 @@ def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) :=
   let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by
         simp [Nat.shiftLeft_eq, Nat.pow_add]
         apply Nat.mul_lt_mul_of_pos_right p
-        exact (Nat.pow_two_pos m)
+        exact (Nat.two_pow_pos m)
   ⟨msbs.toNat <<< m, shiftLeftLt msbs.isLt m⟩
 
 /--
diff --git a/Std/Data/BitVec/Bitblast.lean b/Std/Data/BitVec/Bitblast.lean
index fab15a0279..323754a84c 100644
--- a/Std/Data/BitVec/Bitblast.lean
+++ b/Std/Data/BitVec/Bitblast.lean
@@ -58,7 +58,7 @@ private theorem mod_two_pow_succ (x i : Nat) :
   apply Nat.eq_of_testBit_eq
   intro j
   simp only [Nat.mul_add_lt_is_or, testBit_or, testBit_mod_two_pow, testBit_shiftLeft,
-    Nat.testBit_bool_to_nat, Nat.sub_eq_zero_iff_le, Nat.mod_lt, Nat.pow_two_pos,
+    Nat.testBit_bool_to_nat, Nat.sub_eq_zero_iff_le, Nat.mod_lt, Nat.two_pow_pos,
     testBit_mul_pow_two]
   rcases Nat.lt_trichotomy i j with i_lt_j | i_eq_j | j_lt_i
   · have i_le_j : i ≤ j := Nat.le_of_lt i_lt_j
@@ -73,7 +73,7 @@ private theorem mod_two_pow_succ (x i : Nat) :
     have not_j_ge_i : ¬(j ≥ i) := Nat.not_le_of_lt j_lt_i
     simp [j_lt_i, j_le_i, not_j_ge_i, j_le_i_succ]
 
-private theorem mod_two_pow_lt (x i : Nat) : x % 2 ^ i < 2^i := Nat.mod_lt _ (Nat.pow_two_pos _)
+private theorem mod_two_pow_lt (x i : Nat) : x % 2 ^ i < 2^i := Nat.mod_lt _ (Nat.two_pow_pos _)
 
 /-! ### Addition -/
 
@@ -96,7 +96,7 @@ theorem adc_overflow_limit (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toN
   apply Nat.add_le_add (mod_two_pow_lt _ _)
   apply Nat.le_trans
   exact (Nat.add_le_add_left (Bool.toNat_le_one c) _)
-  exact Nat.mod_lt _ (Nat.pow_two_pos i)
+  exact Nat.mod_lt _ (Nat.two_pow_pos i)
 
 theorem carry_succ (w x y : Nat) (c : Bool) : carry (succ w) x y c =
     decide ((x.testBit w).toNat + (y.testBit w).toNat + (carry w x y c).toNat ≥ 2) := by
diff --git a/Std/Data/BitVec/Lemmas.lean b/Std/Data/BitVec/Lemmas.lean
index ef8e977184..6c003cd355 100644
--- a/Std/Data/BitVec/Lemmas.lean
+++ b/Std/Data/BitVec/Lemmas.lean
@@ -235,7 +235,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
   · simp
     rw [Nat.mod_eq_of_lt]
     rw [Nat.shiftLeft_eq, Nat.pow_add]
-    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.pow_two_pos _)
+    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
   · omega
 
 @[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index 91e347e1bc..a3fc3a7a13 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -24,7 +24,7 @@ private theorem two_pow_succ_sub_one_div : (2 ^ (n+1) - 1) / 2 = 2^n - 1 := by
   apply fun x => (Nat.sub_eq_of_eq_add x).symm
   apply Eq.trans _
   apply Nat.add_mul_div_left _ _ Nat.zero_lt_two
-  rw [Nat.mul_one, ←Nat.sub_add_comm (Nat.pow_two_pos _)]
+  rw [Nat.mul_one, ←Nat.sub_add_comm (Nat.two_pow_pos _)]
   rw [ Nat.add_sub_assoc Nat.zero_lt_two ]
   simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_div]
 
@@ -144,7 +144,7 @@ theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) :
 theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
   induction x using div2Induction generalizing n with
   | ind x hyp =>
-    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.pow_two_pos n) p
+    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p
     have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
     match n with
     | zero =>
@@ -198,7 +198,7 @@ private theorem testBit_succ_zero : testBit (x + 1) 0 = not (testBit x 0) := by
     simp [p]
 
 theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = not (testBit x i) := by
-  simp [testBit_to_div_mod, add_div_left, Nat.pow_two_pos, succ_mod_two]
+  simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]
   cases mod_two_eq_zero_or_one (x / 2 ^ i) with
   | _ p => simp [p]
 
@@ -219,7 +219,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
   have i_def : i = j + (i-j) := (Nat.add_sub_cancel' (Nat.le_of_lt j_lt_i)).symm
   rw [i_def]
   simp only [testBit_to_div_mod, Nat.pow_add,
-        Nat.add_comm x, Nat.mul_add_div (Nat.pow_two_pos _)]
+        Nat.add_comm x, Nat.mul_add_div (Nat.two_pow_pos _)]
   match i_sub_j_eq : i - j with
   | 0 =>
     exfalso
@@ -244,10 +244,10 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
         simp [Nat.testBit_lt_two x_lt]
     · generalize y_eq : x - 2^j = y
       have x_eq : x = y + 2^j := Nat.eq_add_of_sub_eq x_ge_j y_eq
-      simp only [Nat.pow_two_pos, x_eq, Nat.le_add_left, true_and, ite_true]
+      simp only [Nat.two_pow_pos, x_eq, Nat.le_add_left, true_and, ite_true]
       have y_lt_x : y < x := by
             simp [x_eq]
-            exact Nat.lt_add_of_pos_right (Nat.pow_two_pos j)
+            exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
       simp only [hyp y y_lt_x]
       if i_lt_j : i < j then
         rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
@@ -264,7 +264,7 @@ private theorem testBit_one_zero : testBit 1 0 = true := by trivial
     | 0 =>
       simp
     | n+1 =>
-      simp [Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
+      simp [Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.two_pow_pos]
   | succ i hyp =>
     simp only [testBit_succ]
     match n with
@@ -430,7 +430,7 @@ theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat)
                  rw [← congrArg (j+·) (Nat.succ_pred i_sub_j_nez)]
     rw [i_def]
     simp only [testBit_to_div_mod, Nat.pow_add, Nat.mul_assoc]
-    simp only [Nat.mul_add_div (Nat.pow_two_pos _), Nat.mul_add_mod]
+    simp only [Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]
     simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_assoc, Nat.mul_add_mod]
   | inr j_ge =>
     have j_def : j = i + (j-i) := (Nat.add_sub_cancel' j_ge).symm
@@ -443,11 +443,11 @@ theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat)
           ←Nat.div_div_eq_div_mul,
           Nat.mul_add_div,
           Nat.div_eq_of_lt b_lt,
-          Nat.pow_two_pos i]
+          Nat.two_pow_pos i]
 
 theorem testBit_mul_pow_two :
     testBit (2 ^ i * a) j = (decide (j ≥ i) && testBit a (j-i)) := by
-  have gen := testBit_mul_pow_two_add a (Nat.pow_two_pos i) j
+  have gen := testBit_mul_pow_two_add a (Nat.two_pow_pos i) j
   simp at gen
   rw [gen]
   cases Nat.lt_or_ge j i with
diff --git a/Std/Data/Nat/Init/Lemmas.lean b/Std/Data/Nat/Init/Lemmas.lean
index 20876de423..5c8bbfc379 100644
--- a/Std/Data/Nat/Init/Lemmas.lean
+++ b/Std/Data/Nat/Init/Lemmas.lean
@@ -52,7 +52,8 @@ protected theorem le_max_left (a b : Nat) : a ≤ max a b := by rw [Nat.max_def]
 
 protected theorem le_max_right (a b : Nat) : b ≤ max a b := Nat.max_comm .. ▸ Nat.le_max_left ..
 
-protected theorem pow_two_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+@[deprecated] alias pow_two_pos := Nat.two_pow_pos -- deprecated 2024-02-09
 
 @[simp] protected theorem not_le {a b : Nat} : ¬ a ≤ b ↔ b < a :=
   ⟨Nat.gt_of_not_le, Nat.not_le_of_gt⟩
diff --git a/Std/Data/UInt.lean b/Std/Data/UInt.lean
index a860f3a045..fe87ee037a 100644
--- a/Std/Data/UInt.lean
+++ b/Std/Data/UInt.lean
@@ -80,7 +80,7 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 @[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl
 
 theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
-  have : 1 ≤ 2 ^ System.Platform.numBits := Nat.succ_le_of_lt (Nat.pow_two_pos _)
+  have : 1 ≤ 2 ^ System.Platform.numBits := Nat.succ_le_of_lt (Nat.two_pow_pos _)
   rw [USize.size, Nat.succ_eq_add_one, Nat.sub_eq, Nat.sub_add_cancel this]
 
 theorem USize.le_size : 2 ^ 32 ≤ USize.size := by