diff --git a/Mathlib/Data/BitVec/Defs.lean b/Mathlib/Data/BitVec/Defs.lean
index ae6f555ce378b..d42b5be99a64e 100644
--- a/Mathlib/Data/BitVec/Defs.lean
+++ b/Mathlib/Data/BitVec/Defs.lean
@@ -58,9 +58,11 @@ namespace Std.BitVec
 /-! ### Arithmetic operators -/
 
 #align bitvec.neg Std.BitVec.neg
-/-- Add with carry (no overflow) -/
-def adc {n} (x y : BitVec n) (c : Bool) : BitVec (n+1) :=
-  ofFin (x.toNat + y.toNat + c.toNat)
+/-- Add with carry (no overflow)
+
+See also `Std.BitVec.adc`, which stores the carry bit separately. -/
+def adc' {n} (x y : BitVec n) (c : Bool) : BitVec (n+1) :=
+  let a := x.adc y c; .cons a.1 a.2
 #align bitvec.adc Std.BitVec.adc
 
 #align bitvec.add Std.BitVec.add
diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean
index ec8ffe729035e..97f2353f1d29f 100644
--- a/Mathlib/Data/BitVec/Lemmas.lean
+++ b/Mathlib/Data/BitVec/Lemmas.lean
@@ -31,20 +31,10 @@ theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y :=
 theorem toNat_lt_toNat {x y : BitVec w} : x.toNat < y.toNat ↔ x < y :=
   Iff.rfl
 
-@[simp]
-lemma ofNat_eq_mod_two_pow (n : Nat) : (BitVec.ofNat w n).toNat = n % 2^w := rfl
-
-lemma toNat_ofNat {m} (h : m < 2^w) : (BitVec.ofNat w m).toNat = m := Fin.val_cast_of_lt h
-
-@[simp]
-lemma toNat_ofFin (x : Fin (2^w)) : (ofFin x).toNat = x.val := rfl
+attribute [simp] toNat_ofNat toNat_ofFin
 
-theorem toNat_append (msbs : BitVec w) (lsbs : BitVec v) :
-    (msbs ++ lsbs).toNat = msbs.toNat <<< v ||| lsbs.toNat := by
-  rcases msbs with ⟨msbs, hm⟩
-  rcases lsbs with ⟨lsbs, hl⟩
-  simp only [HAppend.hAppend, append, toNat_ofFin]
-  rw [toNat_ofNat (Nat.add_comm w v ▸ append_lt hl hm)]
+lemma toNat_ofNat_of_lt {m} (h : m < 2^w) : (BitVec.ofNat w m).toNat = m := by
+  simp only [toNat_ofNat, mod_eq_of_lt h]
 
 #noalign bitvec.bits_to_nat_to_bool
 
@@ -60,14 +50,9 @@ lemma extractLsb_eq {w : ℕ} (hi lo : ℕ) (a : BitVec w) :
 
 theorem toNat_extractLsb' {i j} {x : BitVec w} :
     (extractLsb' i j x).toNat = x.toNat / 2 ^ i % (2 ^ j) := by
-  simp only [extractLsb', ofNat_eq_mod_two_pow, shiftRight_eq_div_pow]
-
-theorem getLsb_eq_testBit {i} {x : BitVec w} : getLsb x i = x.toNat.testBit i := by
-  simp only [getLsb, Nat.shiftLeft_eq, one_mul, Nat.and_two_pow]
-  cases' testBit (BitVec.toNat x) i
-  <;> simp [pos_iff_ne_zero.mp (two_pow_pos i)]
+  simp only [extractLsb', toNat_ofNat, shiftRight_eq_div_pow]
 
-theorem ofFin_val {n : ℕ} (i : Fin <| 2 ^ n) : (ofFin i).toNat = i.val := by
+theorem ofFin_val {n : ℕ} (i : Fin <| 2 ^ n) : (ofFin i).toNat = i.val :=
   rfl
 #align bitvec.of_fin_val Std.BitVec.ofFin_val
 
@@ -91,16 +76,12 @@ theorem decide_addLsb_mod_two {x b} : decide (addLsb x b % 2 = 1) = b := by
   simp [addLsb]
 #align bitvec.to_bool_add_lsb_mod_two Std.BitVec.decide_addLsb_mod_two
 
-@[simp]
-lemma ofNat_toNat (x : BitVec w) : BitVec.ofNat w x.toNat = x := by
-  rcases x with ⟨x⟩
-  simp [BitVec.ofNat]
-  apply Fin.cast_val_eq_self x
-#align bitvec.of_nat_to_nat Std.BitVec.ofNat_toNat
+lemma ofNat_toNat' (x : BitVec w) : (x.toNat)#w = x := by
+  rw [ofNat_toNat, truncate_eq]
 
-lemma ofNat_toNat' (x : BitVec w) (h : w = v):
+lemma ofNat_toNat_of_eq (x : BitVec w) (h : w = v):
     BitVec.ofNat v x.toNat = x.cast h := by
-  cases h; rw [ofNat_toNat, cast_eq]
+  cases h; rw [ofNat_toNat', cast_eq]
 
 theorem toFin_val {n : ℕ} (v : BitVec n) : (toFin v : ℕ) = v.toNat := by
   rfl
diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean
index 451b1f5470010..50bddc60ebbe1 100644
--- a/Mathlib/Data/Bool/Basic.lean
+++ b/Mathlib/Data/Bool/Basic.lean
@@ -47,14 +47,7 @@ theorem of_decide_iff {p : Prop} [Decidable p] : decide p ↔ p :=
   coe_decide p
 #align bool.of_to_bool_iff Bool.of_decide_iff
 
-@[simp]
-theorem true_eq_decide_iff {p : Prop} [Decidable p] : true = decide p ↔ p :=
-  eq_comm.trans of_decide_iff
 #align bool.tt_eq_to_bool_iff Bool.true_eq_decide_iff
-
-@[simp]
-theorem false_eq_decide_iff {p : Prop} [Decidable p] : false = decide p ↔ ¬p :=
-  eq_comm.trans (decide_false_iff _)
 #align bool.ff_eq_to_bool_iff Bool.false_eq_decide_iff
 
 theorem decide_not (p : Prop) [Decidable p] : (decide ¬p) = !(decide p) := by
@@ -308,22 +301,13 @@ theorem right_le_or : ∀ x y : Bool, y ≤ (x || y) := by decide
 theorem or_le : ∀ {x y z}, x ≤ z → y ≤ z → (x || y) ≤ z := by decide
 #align bool.bor_le Bool.or_le
 
-/-- convert a `Bool` to a `ℕ`, `false -> 0`, `true -> 1` -/
-def toNat (b : Bool) : Nat :=
-  cond b 1 0
 #align bool.to_nat Bool.toNat
 
-lemma toNat_le_one (b : Bool) : b.toNat ≤ 1 := by
-  cases b <;> decide
-
 /-- convert a `ℕ` to a `Bool`, `0 -> false`, everything else -> `true` -/
 def ofNat (n : Nat) : Bool :=
   decide (n ≠ 0)
 #align bool.of_nat Bool.ofNat
 
-@[simp] lemma toNat_true  : toNat true = 1  := rfl
-@[simp] lemma toNat_false : toNat false = 0 := rfl
-
 @[simp] lemma toNat_beq_zero (b : Bool) : (b.toNat == 0) = !b := by cases b <;> rfl
 @[simp] lemma toNat_bne_zero (b : Bool) : (b.toNat != 0) =  b := by simp [bne]
 @[simp] lemma toNat_beq_one  (b : Bool) : (b.toNat == 1) =  b := by cases b <;> rfl
diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index f776c5598e108..0808371b3a931 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -407,15 +407,15 @@ attribute [local simp] Int.zero_div
 
 theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<< (n : ℤ)) <<< k
   | (m : ℕ), n, (k : ℕ) =>
-    congr_arg ofNat (by simp [Nat.pow_add, mul_assoc])
+    congr_arg ofNat (by simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc])
   | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftLeft'_add _ _ _ _)
   | (m : ℕ), n, -[k+1] =>
     subNatNat_elim n k.succ (fun n k i => (↑m) <<< i = (Nat.shiftLeft' false m n) >>> k)
       (fun (i n : ℕ) =>
-        by dsimp; simp [- Nat.shiftLeft_eq, ← Nat.shiftLeft_sub _ , add_tsub_cancel_left])
+        by dsimp; simp [← Nat.shiftLeft_sub _ , add_tsub_cancel_left])
       fun i n => by
         dsimp
-        simp [- Nat.shiftLeft_eq, Nat.shiftLeft_zero, Nat.shiftRight_add, ← Nat.shiftLeft_sub]
+        simp [Nat.shiftLeft_zero, Nat.shiftRight_add, ← Nat.shiftLeft_sub]
         rfl
   | -[m+1], n, -[k+1] =>
     subNatNat_elim n k.succ
@@ -433,7 +433,7 @@ theorem shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (n - k) = (m <<< (n
 #align int.shiftl_sub Int.shiftLeft_sub
 
 theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2 ^ n : ℕ)
-  | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp)
+  | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq])
   | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _)
 #align int.shiftl_eq_mul_pow Int.shiftLeft_eq_mul_pow
 
@@ -445,7 +445,7 @@ theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / (
 #align int.shiftr_eq_div_pow Int.shiftRight_eq_div_pow
 
 theorem one_shiftLeft (n : ℕ) : 1 <<< (n : ℤ) = (2 ^ n : ℕ) :=
-  congr_arg ((↑) : ℕ → ℤ) (by simp)
+  congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq])
 #align int.one_shiftl Int.one_shiftLeft
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index 5f999e12a50f9..24a63bd7e349f 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -838,11 +838,12 @@ theorem lt_mul_div_succ (m : ℕ) {n : ℕ} (n0 : 0 < n) : m < n * (m / n + 1) :
   exact lt_succ_self _
 #align nat.lt_mul_div_succ Nat.lt_mul_div_succ
 
-theorem mul_add_mod (a b c : ℕ) : (a * b + c) % b = c % b := by simp [Nat.add_mod]
-#align nat.mul_add_mod Nat.mul_add_mod
+-- TODO: Std4 claimed this name but flipped the order of multiplication
+theorem mul_add_mod' (a b c : ℕ) : (a * b + c) % b = c % b := by rw [mul_comm, Nat.mul_add_mod]
+#align nat.mul_add_mod Nat.mul_add_mod'
 
 theorem mul_add_mod_of_lt {a b c : ℕ} (h : c < b) : (a * b + c) % b = c := by
-  rw [Nat.mul_add_mod, Nat.mod_eq_of_lt h]
+  rw [Nat.mul_add_mod', Nat.mod_eq_of_lt h]
 #align nat.mul_add_mod_of_lt Nat.mul_add_mod_of_lt
 
 theorem pred_eq_self_iff {n : ℕ} : n.pred = n ↔ n = 0 := by
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 7e63942b5660b..cfa0f629fc037 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -126,15 +126,7 @@ theorem xor_bit : ∀ a m b n, bit a m ^^^ bit b n = bit (bne a b) (m ^^^ n) :=
   bitwise_bit
 #align nat.lxor_bit Nat.xor_bit
 
-@[simp]
-theorem testBit_bitwise {f : Bool → Bool → Bool} (h : f false false = false) (m n k) :
-    testBit (bitwise f m n) k = f (testBit m k) (testBit n k) := by
-  induction' k with k ih generalizing m n
-  <;> cases' m using bitCasesOn with a m
-  <;> cases' n using bitCasesOn with b n
-  <;> rw [bitwise_bit h]
-  · simp [testBit_zero]
-  · simp [testBit_succ, ih]
+attribute [simp] Nat.testBit_bitwise
 #align nat.test_bit_bitwise Nat.testBit_bitwise
 
 @[simp]
@@ -152,9 +144,7 @@ theorem testBit_ldiff : ∀ m n k, testBit (ldiff m n) k = (testBit m k && not (
   testBit_bitwise rfl
 #align nat.test_bit_ldiff Nat.testBit_ldiff
 
-@[simp]
-theorem testBit_xor : ∀ m n k, testBit (m ^^^ n) k = bne (testBit m k) (testBit n k) :=
-  testBit_bitwise rfl
+attribute [simp] testBit_xor
 #align nat.test_bit_lxor Nat.testBit_xor
 
 end
@@ -217,31 +207,19 @@ theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n
 theorem testBit_eq_false_of_lt {n i} (h : n < 2 ^ i) : n.testBit i = false := by
   simp [testBit, shiftRight_eq_div_pow, Nat.div_eq_of_lt h]
 
-@[simp]
-theorem zero_testBit (i : ℕ) : testBit 0 i = false := by
-  simp only [testBit, zero_shiftRight, bodd_zero]
 #align nat.zero_test_bit Nat.zero_testBit
 
 /-- The ith bit is the ith element of `n.bits`. -/
 theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i := by
   induction' i with i ih generalizing n
-  · simp [testBit, bodd_eq_bits_head, List.getI_zero_eq_headI]
+  · simp only [testBit, zero_eq, shiftRight_zero, and_one_is_mod, mod_two_of_bodd,
+      bodd_eq_bits_head, List.getI_zero_eq_headI]
+    cases List.headI (bits n) <;> rfl
   conv_lhs => rw [← bit_decomp n]
   rw [testBit_succ, ih n.div2, div2_bits_eq_tail]
   cases n.bits <;> simp
 #align nat.test_bit_eq_inth Nat.testBit_eq_inth
 
-/-- Bitwise extensionality: Two numbers agree if they agree at every bit position. -/
-theorem eq_of_testBit_eq {n m : ℕ} (h : ∀ i, testBit n i = testBit m i) : n = m := by
-  induction' n using Nat.binaryRec with b n hn generalizing m
-  · simp only [zero_testBit] at h
-    exact (zero_of_testBit_eq_false fun i => (h i).symm).symm
-  induction' m using Nat.binaryRec with b' m
-  · simp only [zero_testBit] at h
-    exact zero_of_testBit_eq_false h
-  suffices h' : n = m by
-    rw [h', show b = b' by simpa using h 0]
-  exact hn fun i => by convert h (i + 1) using 1 <;> rw [testBit_succ]
 #align nat.eq_of_test_bit_eq Nat.eq_of_testBit_eq
 
 theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
@@ -295,20 +273,20 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
 
 @[simp]
 theorem testBit_two_pow_self (n : ℕ) : testBit (2 ^ n) n = true := by
-  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n), bodd_one]
+  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n)]
+  simp
 #align nat.test_bit_two_pow_self Nat.testBit_two_pow_self
 
 theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = false := by
   rw [testBit, shiftRight_eq_div_pow]
   cases' hm.lt_or_lt with hm hm
-  · rw [Nat.div_eq_of_lt, bodd_zero]
-    exact Nat.pow_lt_pow_of_lt_right one_lt_two hm
+  · rw [Nat.div_eq_of_lt]
+    · simp
+    · exact Nat.pow_lt_pow_of_lt_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)]
     -- Porting note: XXX why does this make it work?
     rw [(rfl : succ 0 = 1)]
-    simp only [ge_iff_le, tsub_le_iff_right, pow_succ, bodd_mul,
-      Bool.and_eq_false_eq_eq_false_or_eq_false, or_true]
-    exact Or.inr rfl
+    simp [pow_succ, and_one_is_mod, mul_mod_left]
 #align nat.test_bit_two_pow_of_ne Nat.testBit_two_pow_of_ne
 
 theorem testBit_two_pow (n m : ℕ) : testBit (2 ^ n) m = (n = m) := by
@@ -372,25 +350,10 @@ theorem zero_xor (n : ℕ) : 0 ^^^ n = n := by simp [HXor.hXor, Xor.xor, xor]
 theorem xor_zero (n : ℕ) : n ^^^ 0 = n := by simp [HXor.hXor, Xor.xor, xor]
 #align nat.lxor_zero Nat.xor_zero
 
-@[simp]
-theorem zero_land (n : ℕ) : 0 &&& n = 0 := by
-  simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_left, ite_false, Bool.and_true];
-#align nat.zero_land Nat.zero_land
-
-@[simp]
-theorem land_zero (n : ℕ) : n &&& 0 = 0 := by
-  simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_right, ite_false, Bool.and_false]
-#align nat.land_zero Nat.land_zero
-
-@[simp]
-theorem zero_lor (n : ℕ) : 0 ||| n = n := by
-  simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_left, ite_true, Bool.or_true]
-#align nat.zero_lor Nat.zero_lor
-
-@[simp]
-theorem lor_zero (n : ℕ) : n ||| 0 = n := by
-  simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_right, ite_true, Bool.or_false]
-#align nat.lor_zero Nat.lor_zero
+#align nat.zero_land Nat.zero_and
+#align nat.land_zero Nat.and_zero
+#align nat.zero_lor Nat.zero_or
+#align nat.lor_zero Nat.or_zero
 
 
 /-- Proving associativity of bitwise operations in general essentially boils down to a huge case
@@ -488,11 +451,11 @@ theorem xor_trichotomy {a b c : ℕ} (h : a ≠ b ^^^ c) :
   all_goals
     exact lt_of_testBit i (by
       -- Porting note: this was originally `simp [h, hi]`
-      rw [Nat.testBit_xor, h, Bool.bne_eq_xor, Bool.true_xor,hi]
+      rw [Nat.testBit_xor, h, Bool.xor, Bool.true_xor, hi]
       rfl
     ) h fun j hj => by
       -- Porting note: this was originally `simp [hi' _ hj]`
-      rw [Nat.testBit_xor, hi' _ hj, Bool.bne_eq_xor, Bool.xor_false, eq_self_iff_true]
+      rw [Nat.testBit_xor, hi' _ hj, Bool.xor, Bool.xor_false, eq_self_iff_true]
       trivial
 #align nat.lxor_trichotomy Nat.xor_trichotomy
 
diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
index 347d22795547b..53533ef5aaddf 100644
--- a/Mathlib/Data/Nat/Order/Lemmas.lean
+++ b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -223,11 +223,6 @@ theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b :=
   exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
 #align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd
 
-@[simp]
-theorem mod_div_self (m n : ℕ) : m % n / n = 0 := by
-  cases n
-  · exact (m % 0).div_zero
-  · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)
 #align nat.mod_div_self Nat.mod_div_self
 
 /-- `n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`. -/
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 3a9c95879822e..0feaee57900ea 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -32,10 +32,7 @@ theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1)
 end
 
 #align nat.one_shiftl Nat.one_shiftLeft
-
-theorem zero_shiftLeft (n) : 0 <<< n = 0 := by simp
 #align nat.zero_shiftl Nat.zero_shiftLeft
-
 #align nat.shiftr_eq_div_pow Nat.shiftRight_eq_div_pow
 
 theorem shiftLeft'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftLeft' b m n ≠ 0 := by
@@ -118,7 +115,7 @@ theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
   by_cases h : bit b n = 0
   · apply this h
   rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul, ← bit0_val]
-  exact bit_lt_bit0 _ (by simpa [shiftRight_eq_div_pow] using IH)
+  exact bit_lt_bit0 _ (by simpa [shiftLeft_eq, shiftRight_eq_div_pow] using IH)
 #align nat.lt_size_self Nat.lt_size_self
 
 theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index dc9ced5fbb7cf..7c38cc08ec81e 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -970,28 +970,19 @@ theorem castNum_shiftRight (m : Num) (n : Nat) : ↑(m >>> n) = (m : ℕ) >>> (n
 @[simp]
 theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by
   -- Porting note: `unfold` → `dsimp only`
-  cases m <;> dsimp only [testBit, Nat.testBit]
+  cases m <;> dsimp only [testBit]
   case zero =>
-    change false = Nat.bodd (0 >>> n)
-    rw [Nat.zero_shiftRight]
-    rfl
+    rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]
   case pos m =>
-    induction' n with n IH generalizing m <;> cases' m with m m <;> dsimp only [PosNum.testBit]
+    rw [cast_pos]
+    induction' n with n IH generalizing m <;> cases' m with m m
+        <;> dsimp only [PosNum.testBit, Nat.zero_eq]
     · rfl
-    · exact (Nat.bodd_bit _ _).symm
-    · exact (Nat.bodd_bit _ _).symm
-    · change false = Nat.bodd (1 >>> (n + 1))
-      rw [add_comm, Nat.shiftRight_add]
-      change false = Nat.bodd (0 >>> n)
-      rw [Nat.zero_shiftRight]; rfl
-    · change PosNum.testBit m n = Nat.bodd ((Nat.bit true m) >>> (n + 1))
-      rw [add_comm, Nat.shiftRight_add]
-      simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit]
-      apply IH
-    · change PosNum.testBit m n = Nat.bodd ((Nat.bit false m) >>> (n + 1))
-      rw [add_comm, Nat.shiftRight_add]
-      simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit]
-      apply IH
+    · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_zero]
+    · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_zero]
+    · rw [PosNum.cast_one', ← bit1_zero, ← Nat.bit_true, Nat.testBit_succ, Nat.zero_testBit]
+    · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_succ, IH]
+    · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_succ, IH]
 #align num.test_bit_to_nat Num.castNum_testBit
 
 end Num
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 5d8d5c74da67e..cf70f850eda3f 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -190,7 +190,7 @@ theorem shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
   | n + 1 => by
     have : 2 * (m * 2^n) = 2^(n+1)*m := by
       rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp
-    simp [shiftLeft', bit_val, shiftLeft'_false, this]
+    simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]
 
 /-- Std4 takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/
 @[simp]
@@ -199,14 +199,6 @@ lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl
 @[simp]
 lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl
 
-theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
-
-theorem shiftLeft_succ (m n) : m <<< (n + 1) = 2 * (m <<< n) := by
-  simp only [shiftLeft_eq, Nat.pow_add, Nat.pow_one, ← Nat.mul_assoc, Nat.mul_comm]
-
-/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
-def testBit (m n : ℕ) : Bool :=
-  bodd (m >>> n)
 #align nat.test_bit Nat.testBit
 
 lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
@@ -301,15 +293,28 @@ theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<<
   fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]
 
 @[simp]
-theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
-  bodd_bit _ _
+theorem testBit_zero (b n) : testBit (bit b n) 0 = b := by
+  rw [testBit, bit]
+  cases b
+  · simp [bit0, ← Nat.mul_two]
+  · simp only [cond_true, bit1, bit0, shiftRight_zero, and_one_is_mod, bne_iff_ne]
+    simp only [← Nat.mul_two]
+    rw [Nat.add_mod]
+    simp
+
 #align nat.test_bit_zero Nat.testBit_zero
 
+theorem bodd_eq_and_one_ne_zero : ∀ n, bodd n = (n &&& 1 != 0)
+  | 0 => rfl
+  | 1 => rfl
+  | n + 2 => by simpa using bodd_eq_and_one_ne_zero n
+
 theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
   have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
-    dsimp [shiftRight]
+    simp only [shiftRight_eq_div_pow]
     simp [← div2_val, div2_bit]
   rw [← shiftRight_add, Nat.add_comm] at this
+  simp only [bodd_eq_and_one_ne_zero] at this
   exact this
 #align nat.test_bit_succ Nat.testBit_succ
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 5e630d988708b..55118b35150c1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "415a6731db08f4d98935e5d80586d5a5499e02af",
+   "rev": "a93d4aab761b7962a6aab845b24837e192eaabc5",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",