diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
index 3defa207c49ee..e47f1d86a40f2 100644
--- a/Mathlib/Computability/Primrec.lean
+++ b/Mathlib/Computability/Primrec.lean
@@ -796,7 +796,7 @@ instance sum : Primcodable (α ⊕ β) :=
                 to₂ <| nat_double.comp (Primrec.encode.comp snd)))).of_eq
         fun n =>
         show _ = encode (decodeSum n) by
-          simp only [decodeSum, Nat.boddDiv2_eq]
+          simp only [decodeSum]
           cases Nat.bodd n <;> simp [decodeSum]
           · cases @decode α _ n.div2 <;> rfl
           · cases @decode β _ n.div2 <;> rfl⟩
diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index e0bc3e616150f..0c2caf13fd02d 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -219,9 +219,7 @@ theorem bodd_bit (b n) : bodd (bit b n) = b := by
 theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
   | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
   | -[n+1] => by
-    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero
-    cases b <;>
-      rfl
+    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero, Bool.not_not]
 
 @[simp]
 theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 0edc733fa68b0..8fed9078d0603 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -20,8 +20,10 @@ universe u
 
 namespace Nat
 
-/-- `bit b` appends the digit `b` to the binary representation of its natural number input. -/
-def bit (b : Bool) : Nat → Nat := cond b (2 * · + 1) (2 * ·)
+/-- `bit b` appends the digit `b` to the little end of the binary representation of
+  its natural number input. -/
+def bit (b : Bool) (n : Nat) : Nat :=
+  cond b (n <<< 1 + 1) (n <<< 1)
 
 theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
 
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index bdcc8d87a6a7c..0067e836b372d 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -5,8 +5,8 @@ Authors: Praneeth Kolichala
 -/
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat
-import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Nat.BinaryRec
+import Mathlib.Data.Nat.Defs
 import Mathlib.Data.List.Defs
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs
@@ -34,7 +34,7 @@ variable {m n : ℕ}
 
 /-- `boddDiv2 n` returns a 2-tuple of type `(Bool, Nat)` where the `Bool` value indicates whether
 `n` is odd or not and the `Nat` value returns `⌊n/2⌋` -/
-def boddDiv2 : ℕ → Bool × ℕ
+@[deprecated (since := "2024-06-09")] def boddDiv2 : ℕ → Bool × ℕ
   | 0 => (false, 0)
   | succ n =>
     match boddDiv2 n with
@@ -42,10 +42,12 @@ def boddDiv2 : ℕ → Bool × ℕ
     | (true, m) => (false, succ m)
 
 /-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
-def div2 (n : ℕ) : ℕ := (boddDiv2 n).2
+def div2 (n : ℕ) : ℕ := n >>> 1
+
+theorem div2_val (n) : div2 n = n / 2 := rfl
 
 /-- `bodd n` returns `true` if `n` is odd -/
-def bodd (n : ℕ) : Bool := (boddDiv2 n).1
+def bodd (n : ℕ) : Bool := 1 &&& n != 0
 
 @[simp] lemma bodd_zero : bodd 0 = false := rfl
 
@@ -55,9 +57,8 @@ lemma bodd_two : bodd 2 = false := rfl
 
 @[simp]
 lemma bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
-  simp only [bodd, boddDiv2]
-  let ⟨b,m⟩ := boddDiv2 n
-  cases b <;> rfl
+  simp only [bodd, succ_eq_add_one, one_and_eq_mod_two]
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]
 
 @[simp]
 lemma bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by
@@ -73,19 +74,13 @@ lemma bodd_mul (m n : ℕ) : bodd (m * n) = (bodd m && bodd n) := by
     simp only [mul_succ, bodd_add, IH, bodd_succ]
     cases bodd m <;> cases bodd n <;> rfl
 
-lemma mod_two_of_bodd (n : ℕ) : n % 2 = (bodd n).toNat := by
-  have := congr_arg bodd (mod_add_div n 2)
-  simp? [not] at this says
-    simp only [bodd_add, bodd_mul, bodd_succ, not, bodd_zero, Bool.false_and, Bool.bne_false]
-      at this
-  have _ : ∀ b, and false b = false := by
-    intro b
-    cases b <;> rfl
-  have _ : ∀ b, bxor b false = b := by
-    intro b
-    cases b <;> rfl
-  rw [← this]
-  rcases mod_two_eq_zero_or_one n with h | h <;> rw [h] <;> rfl
+@[simp]
+lemma bodd_bit (b n) : bodd (bit b n) = b := by
+  simp [bodd]
+
+lemma mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
+  cases n using bitCasesOn with
+  | h b n => cases b <;> simp
 
 @[simp] lemma div2_zero : div2 0 = 0 := rfl
 
@@ -95,24 +90,18 @@ lemma div2_two : div2 2 = 1 := rfl
 
 @[simp]
 lemma div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n) := by
-  simp only [bodd, boddDiv2, div2]
-  rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp
+  cases n using bitCasesOn with
+  | h b n => cases b <;> simp [bit_val, div2_val, succ_div]
+
+@[simp]
+lemma div2_bit (b n) : div2 (bit b n) = n := by
+  rw [div2_val, bit_div_two]
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
 
-lemma bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
-  | 0 => rfl
-  | succ n => by
-    simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]
-    refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))
-    cases bodd n
-    · simp
-    · simp; omega
-
-lemma div2_val (n) : div2 n = n / 2 := by
-  refine Nat.eq_of_mul_eq_mul_left (by decide)
-    (Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))
-  rw [mod_two_of_bodd, bodd_add_div2]
+lemma bodd_add_div2 (n : ℕ) : cond (bodd n) 1 0 + 2 * div2 n = n := by
+  cases n using bitCasesOn with
+  | h b n => simpa using (bit_val b n).symm
 
 lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
   (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
@@ -139,12 +128,10 @@ lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
 @[simp] 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
 
-lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
-  rw [div2_val]
-  apply (div_lt_iff_lt_mul <| succ_pos 1).2
-  have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
-    (lt_of_le_of_ne n.zero_le h.symm)
-  rwa [Nat.mul_one] at this
+lemma div2_lt_self (h : n ≠ 0) : div2 n < n :=
+  div_lt_self (Nat.pos_iff_ne_zero.mpr h) Nat.one_lt_two
+
+@[deprecated (since := "2024-10-22")] alias binaryRec_decreasing := div2_lt_self
 
 /-- `size n` : Returns the size of a natural number in
 bits i.e. the length of its binary representation -/
@@ -164,17 +151,6 @@ def ldiff : ℕ → ℕ → ℕ :=
 
 /-! bitwise ops -/
 
-lemma bodd_bit (b n) : bodd (bit b n) = b := by
-  rw [bit_val]
-  simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false,
-    Bool.not_true, Bool.and_false, Bool.xor_false]
-  cases b <;> cases bodd n <;> rfl
-
-lemma div2_bit (b n) : div2 (bit b n) = n := by
-  rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
-  <;> cases b
-  <;> decide
-
 lemma shiftLeft'_add (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k
   | 0 => rfl
   | k + 1 => congr_arg (bit b) (shiftLeft'_add b m n k)
@@ -205,8 +181,14 @@ lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
 /-! ### `boddDiv2_eq` and `bodd` -/
 
 
-@[simp]
-theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := rfl
+set_option linter.deprecated false in
+@[deprecated (since := "2024-10-22")]
+theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [boddDiv2, ih]
+    cases hn : n.bodd <;> simp [hn]
 
 @[simp]
 theorem div2_bit0 (n) : div2 (2 * n) = n :=
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 3c394416fac8e..9a575eadb4208 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -59,22 +59,16 @@ lemma bitwise_zero : bitwise f 0 0 = 0 := by
   simp only [bitwise_zero_right, ite_self]
 
 lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
-    bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2)) := by
+    bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f n.div2 m.div2) := by
   conv_lhs => unfold bitwise
   have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
     simp only [mod_two_of_bodd, cond]; cases bodd x <;> rfl
-  simp only [hn, hm, mod_two_iff_bod, ite_false, bit, two_mul, Bool.cond_eq_ite]
-  split_ifs <;> rfl
+  simp [hn, hm, mod_two_iff_bod, bit, div2_val, Nat.shiftLeft_succ, two_mul]
 
 theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
     (h : n ≠ 0) :
-    binaryRec z f n = bit_decomp n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n)) := by
-  cases n using bitCasesOn with
-  | h b n =>
-    rw [binaryRec_eq' _ _ (by right; simpa [bit_eq_zero_iff] using h)]
-    generalize_proofs h; revert h
-    rw [bodd_bit, div2_bit]
-    simp
+    binaryRec z f n = n.bit_decomp ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
+  rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]; rfl
 
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
@@ -82,7 +76,7 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by
   conv_lhs => unfold bitwise
   #adaptation_note /-- nightly-2024-03-16: simp was
   -- simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, Bool.cond_eq_ite] -/
-  simp only [bit, ite_apply, Bool.cond_eq_ite]
+  simp only [bit_val, ite_apply, Bool.cond_eq_ite]
   have h2 x : (x + x + 1) % 2 = 1 := by rw [← two_mul, add_comm]; apply add_mul_mod_self_left
   have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
   cases a <;> cases b <;> simp [h2, h4] <;> split_ifs
@@ -151,8 +145,7 @@ lemma bitwise_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool)
   rw [← bit_ne_zero_iff] at ham hbn
   simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit, ne_eq,
     ite_false]
-  conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]
-  split_ifs with hf <;> rfl
+  conv_rhs => simp [bit, Bool.cond_eq_ite, Nat.shiftLeft_succ, two_mul]
 
 lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
     bitwise f =
@@ -168,8 +161,8 @@ lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
     | z => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
     | f yb y hyb =>
       rw [← bit_ne_zero_iff] at hyb
-      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, ← div2_val,
-        div2_bit, eq_rec_constant, ih]
+      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
+        eq_rec_constant, ih]
 
 theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n = 0 := by
   induction' n using Nat.binaryRec with b n hn
@@ -241,12 +234,9 @@ theorem bitwise_swap {f : Bool → Bool → Bool} :
     bitwise (Function.swap f) = Function.swap (bitwise f) := by
   funext m n
   simp only [Function.swap]
-  induction' m using Nat.strongRecOn with m ih generalizing n
-  cases' m with m
-  <;> cases' n with n
-  <;> try rw [bitwise_zero_left, bitwise_zero_right]
-  · specialize ih ((m+1) / 2) (div_lt_self' ..)
-    simp [bitwise_of_ne_zero, ih]
+  induction' m using Nat.binaryRec' with bm m hm ihm generalizing n; · simp
+  induction' n using Nat.binaryRec' with bn n hn; · simp
+  rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
 
 /-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
     is also commutative. -/
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index 23cd40d657cba..7482eb191db76 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -574,9 +574,9 @@ theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1
   rw [bits_append_bit _ _ fun hn => absurd hn h]
   cases b
   · rw [digits_def' one_lt_two]
-    · simpa [Nat.bit]
-    · simpa [Nat.bit, pos_iff_ne_zero]
-  · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
+    · simpa [bit_val]
+    · simpa [pos_iff_ne_zero, bit_eq_zero_iff]
+  · simpa [bit_val, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
 
 /-! ### Modular Arithmetic -/
 
diff --git a/Mathlib/Data/Nat/Fib/Basic.lean b/Mathlib/Data/Nat/Fib/Basic.lean
index 399cabbe6107f..f669067901eb6 100644
--- a/Mathlib/Data/Nat/Fib/Basic.lean
+++ b/Mathlib/Data/Nat/Fib/Basic.lean
@@ -206,7 +206,7 @@ theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1)) := by
   · rintro (_|_) n' ih <;>
       simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih,
         congr_arg Prod.snd ih, Prod.mk.inj_iff] <;>
-      simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]
+      simp [bit_val, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]
 
 theorem fast_fib_eq (n : ℕ) : fastFib n = fib n := by rw [fastFib, fast_fib_aux_eq]
 
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 2808a6ef83358..21ca910272910 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -215,7 +215,7 @@ theorem ofNat'_succ : ∀ {n}, ofNat' (n + 1) = ofNat' n + 1 :=
     cases b
     · erw [ofNat'_bit true n, ofNat'_bit]
       simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]
-    · rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
+    · rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit_val, mul_add],
         ofNat'_bit, ofNat'_bit, ih]
       simp only [cond, add_one, bit1_succ])
 
@@ -663,9 +663,7 @@ theorem ofNat'_eq : ∀ n, Num.ofNat' n = n :=
     rw [ofNat'] at IH ⊢
     rw [Nat.binaryRec_eq, IH]
     -- Porting note: `Nat.cast_bit0` & `Nat.cast_bit1` are not `simp` theorems anymore.
-    · cases b <;> simp only [cond_false, cond_true, Nat.bit, two_mul, Nat.cast_add, Nat.cast_one]
-      · rw [bit0_of_bit0]
-      · rw [bit1_of_bit1]
+    · cases b <;> simp [Nat.bit_val, two_mul, ← bit0_of_bit0, ← bit1_of_bit1]
     · rfl
 
 theorem zneg_toZNum (n : Num) : -n.toZNum = n.toZNumNeg := by cases n <;> rfl
diff --git a/Mathlib/Logic/Denumerable.lean b/Mathlib/Logic/Denumerable.lean
index cf0e64c97bd1d..12c947d5e85bc 100644
--- a/Mathlib/Logic/Denumerable.lean
+++ b/Mathlib/Logic/Denumerable.lean
@@ -126,9 +126,8 @@ set_option linter.deprecated false in
 instance sum : Denumerable (α ⊕ β) :=
   ⟨fun n => by
     suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
-    simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some',
-      Option.mem_def, Sum.exists]
-    cases bodd n <;> simp [decodeSum, bit, encodeSum, Nat.two_mul]⟩
+    simp only [decodeSum, decode_eq_ofNat, Option.map_some', Option.mem_def, Sum.exists]
+    cases bodd n <;> simp [bit_val, encodeSum]⟩
 
 section Sigma
 
diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index 60412ec201292..9f6991abcaf39 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -232,9 +232,9 @@ def encodeSum : α ⊕ β → ℕ
 
 /-- Explicit decoding function for the sum of two encodable types. -/
 def decodeSum (n : ℕ) : Option (α ⊕ β) :=
-  match boddDiv2 n with
-  | (false, m) => (decode m : Option α).map Sum.inl
-  | (_, m) => (decode m : Option β).map Sum.inr
+  match bodd n, div2 n with
+  | false, m => (decode m : Option α).map Sum.inl
+  | _, m => (decode m : Option β).map Sum.inr
 
 /-- If `α` and `β` are encodable, then so is their sum. -/
 instance _root_.Sum.encodable : Encodable (α ⊕ β) :=
@@ -284,7 +284,7 @@ theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none := by
     rw [Nat.le_div_iff_mul_le]
     exacts [h, by decide]
   cases' exists_eq_succ_of_ne_zero (_root_.ne_of_gt this) with m e
-  simp only [decodeSum, boddDiv2_eq, div2_val]; cases bodd n <;> simp [e]
+  simp only [decodeSum, div2_val]; cases bodd n <;> simp [e]
 
 noncomputable instance _root_.Prop.encodable : Encodable Prop :=
   ofEquiv Bool Equiv.propEquivBool
diff --git a/Mathlib/Logic/Equiv/Nat.lean b/Mathlib/Logic/Equiv/Nat.lean
index 0bc17024d2609..1bce172d54b69 100644
--- a/Mathlib/Logic/Equiv/Nat.lean
+++ b/Mathlib/Logic/Equiv/Nat.lean
@@ -25,9 +25,9 @@ variable {α : Type*}
 @[simps]
 def boolProdNatEquivNat : Bool × ℕ ≃ ℕ where
   toFun := uncurry bit
-  invFun := boddDiv2
-  left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair, boddDiv2_eq]
-  right_inv n := by simp only [bit_decomp, boddDiv2_eq, uncurry_apply_pair]
+  invFun n := ⟨n.bodd, n.div2⟩
+  left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair]
+  right_inv n := by simp only [bit_decomp, uncurry_apply_pair]
 
 /-- An equivalence between `ℕ ⊕ ℕ` and `ℕ`, by mapping `(Sum.inl x)` to `2 * x` and `(Sum.inr x)` to
 `2 * x + 1`.