chore: move into the right files

src/Init/Data/BitVec/Lemmas.lean

@@ -1451,51 +1451,6 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
 
 /-! ### intMin -/
 
-@[simp]
-theorem pow_pred_mul {x w : Nat} (h : 0 < w) :
-    x ^ (w - 1) * x = x ^ w := by
-  simp [← Nat.pow_succ, Nat.succ_eq_add_one, Nat.sub_add_cancel h]
-
-@[simp]
-theorem Nat.two_pow_pred_add_two_pow_pred (h : 0 < w) :
-    2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w:= by
-  rw [← pow_pred_mul h]
-  omega
-
-@[simp]
-theorem Nat.two_pow_sub_two_pow_pred (h : 0 < w) :
-    2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1) := by
-  simp [← two_pow_pred_add_two_pow_pred h]
-
-theorem pow_pred_lt_pow {x w : Nat} (h1 : 1 < x) (h2 : 0 < w) :
-    x ^ (w - 1) < x ^ w :=
-  @Nat.pow_lt_pow_of_lt x (w - 1) w  h1 (by omega)
-
-@[simp]
-theorem two_pow_pred_mod_two_pow (h : 0 < w):
-    2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1) := by
-  rw [Nat.mod_eq_of_lt]
-  apply pow_pred_lt_pow (by omega) h
-
-@[simp]
-theorem Nat.testBit_two_pow_self {n : Nat} : Nat.testBit (2 ^ n) n = true := by
-  rw [Nat.testBit, Nat.shiftRight_eq_div_pow, Nat.div_self (Nat.pow_pos Nat.zero_lt_two)]
-  simp
-
-theorem Nat.pow_lt_pow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
-  (Nat.pow_lt_pow_iff_right ha).2 h
-
-theorem Nat.testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : Nat.testBit (2 ^ n) m = false := by
-  rw [Nat.testBit, Nat.shiftRight_eq_div_pow]
-  have x := Nat.lt_or_lt_of_ne hm
-  cases x
-  · rw [Nat.div_eq_of_lt (Nat.pow_lt_pow_right (by omega) (by omega))]
-    simp
-  · rw [Nat.pow_div _ Nat.two_pos,
-       ← Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.sub_pos_of_lt (by omega))]
-    simp [Nat.pow_succ, Nat.and_one_is_mod, Nat.mul_mod_left]
-    omega
-
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
 def intMin (w : Nat) : BitVec w := BitVec.ofNat w (2^(w - 1))
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -315,6 +315,22 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
   cases i <;> simp
 
+@[simp]
+theorem testBit_two_pow_self {n : Nat} : Nat.testBit (2 ^ n) n = true := by
+  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (Nat.pow_pos Nat.zero_lt_two)]
+  simp
+
+@[simp]
+theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : Nat.testBit (2 ^ n) m = false := by
+  rw [testBit, shiftRight_eq_div_pow]
+  cases Nat.lt_or_lt_of_ne hm
+  · rw [div_eq_of_lt (Nat.pow_lt_pow_right (by omega) (by omega))]
+    simp
+  · rw [Nat.pow_div _ Nat.two_pos,
+       ← Nat.sub_add_cancel (succ_le_of_lt <| Nat.sub_pos_of_lt (by omega))]
+    simp [Nat.pow_succ, and_one_is_mod, mul_mod_left]
+    omega
+
 /-! ### bitwise -/
 
 theorem testBit_bitwise

src/Init/Data/Nat/Lemmas.lean

@@ -700,6 +700,35 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
   · intro w
     exact Nat.pow_lt_pow_of_lt h w
 
+@[simp]
+protected theorem pow_pred_mul {x w : Nat} (h : 0 < w) :
+    x ^ (w - 1) * x = x ^ w := by
+  simp [← Nat.pow_succ, succ_eq_add_one, Nat.sub_add_cancel h]
+
+protected theorem pow_pred_lt_pow {x w : Nat} (h1 : 1 < x) (h2 : 0 < w) :
+    x ^ (w - 1) < x ^ w :=
+  @Nat.pow_lt_pow_of_lt x (w - 1) w  h1 (by omega)
+
+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
+
+@[simp]
+protected theorem two_pow_pred_add_two_pow_pred (h : 0 < w) :
+    2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w:= by
+  rw [← Nat.pow_pred_mul h]
+  omega
+
+@[simp]
+protected theorem two_pow_sub_two_pow_pred (h : 0 < w) :
+    2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1) := by
+  simp [← Nat.two_pow_pred_add_two_pow_pred h]
+
+@[simp]
+protected theorem two_pow_pred_mod_two_pow (h : 0 < w):
+    2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1) := by
+  rw [mod_eq_of_lt]
+  apply Nat.pow_pred_lt_pow (by omega) h
+
 /-! ### log2 -/
 
 @[simp]