From c047c646d66e915f27c3e7f159bef508bfc8dd10 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sun, 9 Jun 2024 08:48:03 +0800
Subject: [PATCH 01/37] chore: redefine `Nat.binaryRec` `Nat.div2` `Nat.bodd`

---
 Mathlib/Computability/Primrec.lean |   2 +-
 Mathlib/Data/Int/Bitwise.lean      |  12 +--
 Mathlib/Data/Nat/BinaryRec.lean    | 136 ++++++++++++++++++++++++
 Mathlib/Data/Nat/Bits.lean         | 165 +++++------------------------
 Mathlib/Data/Nat/Bitwise.lean      |  41 ++-----
 Mathlib/Data/Nat/Digits.lean       |   6 +-
 Mathlib/Data/Nat/EvenOddRec.lean   |   4 +-
 Mathlib/Data/Nat/Fib/Basic.lean    |  10 +-
 Mathlib/Data/Nat/Multiplicity.lean |   2 +-
 Mathlib/Data/Nat/Size.lean         |  26 ++---
 Mathlib/Data/Num/Basic.lean        |   3 +-
 Mathlib/Data/Num/Lemmas.lean       |   6 +-
 Mathlib/Logic/Denumerable.lean     |   5 +-
 Mathlib/Logic/Encodable/Basic.lean |   8 +-
 Mathlib/Logic/Equiv/Nat.lean       |   6 +-
 15 files changed, 217 insertions(+), 215 deletions(-)
 create mode 100644 Mathlib/Data/Nat/BinaryRec.lean

diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
index 775ea877129f8..71da7d39307d4 100644
--- a/Mathlib/Computability/Primrec.lean
+++ b/Mathlib/Computability/Primrec.lean
@@ -943,7 +943,7 @@ instance sum : Primcodable (Sum α β) :=
                 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 c8a7d19ec32d1..a6695aaedf8aa 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -292,13 +292,13 @@ theorem bit1_ne_zero (m : ℤ) : bit1 m ≠ 0 := by simpa only [bit0_zero] using
 end deprecated
 
 @[simp]
-theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
-  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
+theorem bit_testBit_zero (b) : ∀ n, testBit (bit b n) 0 = b
+  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.bit_testBit_zero
   | -[n+1] => by
-    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero;
-        cases b <;>
-      rfl
-#align int.test_bit_zero Int.testBit_bit_zero
+    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.bit_testBit_zero, Bool.not_not]
+#align int.test_bit_zero Int.bit_testBit_zero
+
+@[deprecated (since := "2024-06-09")] alias testBit_bit_zero := bit_testBit_zero
 
 @[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
new file mode 100644
index 0000000000000..a49066806abfa
--- /dev/null
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Praneeth Kolichala, Yuyang Zhao
+-/
+
+/-!
+# Binary recursion on `Nat`
+
+This file defines binary recursion on `Nat`.
+
+## Main results
+* `Nat.binaryRec`: A recursion principle for `bit` representations of natural numbers.
+* `Nat.binaryRec'`: The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`.
+* `Nat.binaryRecFromOne`: The same as `binaryRec`, but special casing both 0 and 1 as base cases.
+-/
+
+universe u
+
+namespace Nat
+
+/-- `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 + n + 1) (n + n)
+
+theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
+
+theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
+  simp only [bit, testBit_zero]
+  cases mod_two_eq_zero_or_one n with | _ h =>
+    simpa [h, shiftRight_one] using Eq.trans (by simp [h, Nat.two_mul]) (Nat.div_add_mod n 2)
+
+theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
+  cases n <;> cases b <;> simp [bit, ← Nat.add_assoc]
+
+/-- For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for any given natural number. -/
+@[inline]
+def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n :=
+  -- `1 &&& n != 0` is faster than `n.testBit 0`. This may change when we have faster `testBit`.
+  let x := h (1 &&& n != 0) (n >>> 1)
+  -- `congrArg C _` is `rfl` in non-dependent case
+  congrArg C n.bit_testBit_zero_shiftRight_one ▸ x
+
+/-- A recursion principle for `bit` representations of natural numbers.
+  For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[elab_as_elim, specialize]
+def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) (n : Nat) : C n :=
+  if n0 : n = 0 then congrArg C n0 ▸ z
+  else
+    let x := f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))
+    congrArg C n.bit_testBit_zero_shiftRight_one ▸ x
+decreasing_by exact bitwise_rec_lemma n0
+
+/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`-/
+@[elab_as_elim, specialize]
+def binaryRec' {C : Nat → Sort u} (z : C 0)
+    (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec z fun b n ih =>
+    if h : n = 0 → b = true then f b n h ih
+    else
+      have : bit b n = 0 := by
+        rw [bit_eq_zero_iff]
+        cases n <;> cases b <;> simp at h <;> simp [h]
+      congrArg C this ▸ z
+
+/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
+@[elab_as_elim, specialize]
+def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
+    (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec' z₀ fun b n h ih =>
+    if h' : n = 0 then
+      have : bit b n = bit true 0 := by
+        rw [h', h h']
+      congrArg C this ▸ z₁
+    else f b n h' ih
+
+theorem bit_val (b n) : bit b n = 2 * n + b.toNat := by
+  rw [Nat.mul_comm]
+  induction b with
+  | false => exact congrArg (· + n) n.zero_add.symm
+  | true => exact congrArg (· + n + 1) n.zero_add.symm
+
+@[simp]
+theorem bit_div_two (b n) : bit b n / 2 = n := by
+  rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
+  · cases b <;> decide
+  · decide
+
+@[simp]
+theorem bit_mod_two (b n) : bit b n % 2 = b.toNat := by
+  cases b <;> simp [bit_val, mul_add_mod]
+
+@[simp] theorem bit_shiftRight_one (b n) : bit b n >>> 1 = n :=
+  bit_div_two b n
+
+theorem bit_testBit_zero (b n) : (bit b n).testBit 0 = b := by
+  simp
+
+@[simp]
+theorem bitCasesOn_bit {C : Nat → Sort u} (h : ∀ b n, C (bit b n)) (b : Bool) (n : Nat) :
+    bitCasesOn (bit b n) h = h b n := by
+  change congrArg C (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
+  generalize congrArg C (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
+  rw [bit_testBit_zero, bit_shiftRight_one]
+  intros; rfl
+
+unseal binaryRec in
+@[simp]
+theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) :
+    binaryRec z f 0 = z :=
+  rfl
+
+theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
+    (h : f false 0 z = z ∨ (n = 0 → b = true)) :
+    binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
+  by_cases h' : bit b n = 0
+  case pos =>
+    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
+    simp only [forall_const, or_false] at h
+    unfold binaryRec
+    exact h.symm
+  case neg =>
+    rw [binaryRec, dif_neg h']
+    change congrArg C (bit b n).bit_testBit_zero_shiftRight_one ▸ f _ _ _ = _
+    generalize congrArg C (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
+    rw [bit_testBit_zero, bit_shiftRight_one]
+    intros; rfl
+
+end Nat
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 592fc4964f3c0..d4ec980159854 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -6,6 +6,7 @@ Authors: Praneeth Kolichala
 import Mathlib.Init.Data.List.Basic
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat
+import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.Nat.Defs
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs
@@ -39,7 +40,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
@@ -48,13 +49,24 @@ def boddDiv2 : ℕ → Bool × ℕ
 #align nat.bodd_div2 Nat.boddDiv2
 
 /-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
-def div2 (n : ℕ) : ℕ := (boddDiv2 n).2
+def div2 (n : ℕ) : ℕ := n >>> 1
 #align nat.div2 Nat.div2
 
+theorem div2_val (n) : div2 n = n / 2 := rfl
+#align nat.div2_val Nat.div2_val
+
 /-- `bodd n` returns `true` if `n` is odd-/
-def bodd (n : ℕ) : Bool := (boddDiv2 n).1
+def bodd (n : ℕ) : Bool := 1 &&& n != 0
 #align nat.bodd Nat.bodd
 
+theorem bit_decomp (n : Nat) : bit n.bodd n.div2 = n :=
+  n.bit_testBit_zero_shiftRight_one
+
+theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
+    (h : n ≠ 0) :
+    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 bodd_zero : bodd 0 = false := rfl
 #align nat.bodd_zero Nat.bodd_zero
 
@@ -66,9 +78,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]
 #align nat.bodd_succ Nat.bodd_succ
 
 @[simp]
@@ -101,6 +112,9 @@ lemma mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
   cases' mod_two_eq_zero_or_one n with h h <;> rw [h] <;> rfl
 #align nat.mod_two_of_bodd Nat.mod_two_of_bodd
 
+theorem div2_add_bodd (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
+  rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
+
 @[simp] lemma div2_zero : div2 0 = 0 := rfl
 #align nat.div2_zero Nat.div2_zero
 
@@ -112,8 +126,10 @@ lemma div2_two : div2 2 = 1 := rfl
 
 @[simp]
 lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
-  simp only [bodd, boddDiv2, div2]
-  rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp
+  apply Nat.eq_of_mul_eq_mul_left (by decide : 0 < 2)
+  apply Nat.add_right_cancel (m := cond (bodd (succ n)) 1 0)
+  rw (config := { occs := .pos [1] }) [div2_add_bodd, bodd_succ, ← div2_add_bodd n]
+  cases bodd n <;> simp [succ_eq_add_one, Nat.add_comm 1, Nat.mul_add]
 #align nat.div2_succ Nat.div2_succ
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
@@ -128,14 +144,6 @@ lemma bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
     · simp; omega
 #align nat.bodd_add_div2 Nat.bodd_add_div2
 
-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]
-#align nat.div2_val Nat.div2_val
-
-/-- `bit b` appends the digit `b` to the binary representation of its natural number input. -/
-def bit (b : Bool) : ℕ → ℕ := cond b bit1 bit0
 #align nat.bit Nat.bit
 
 lemma bit0_val (n : Nat) : bit0 n = 2 * n :=
@@ -148,20 +156,8 @@ lemma bit0_val (n : Nat) : bit0 n = 2 * n :=
 lemma bit1_val (n : Nat) : bit1 n = 2 * n + 1 := congr_arg succ (bit0_val _)
 #align nat.bit1_val Nat.bit1_val
 
-lemma bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
-  cases b
-  · apply bit0_val
-  · apply bit1_val
 #align nat.bit_val Nat.bit_val
-
-lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
-  (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
 #align nat.bit_decomp Nat.bit_decomp
-
-/-- For a predicate `C : Nat → Sort*`, if instances can be
-  constructed for natural numbers of the form `bit b n`,
-  they can be constructed for any given natural number. -/
-def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
 #align nat.bit_cases_on Nat.bitCasesOn
 
 lemma bit_zero : bit false 0 = 0 :=
@@ -189,30 +185,6 @@ lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
 @[simp] lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl
 
 #align nat.test_bit Nat.testBit
-
-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
-
-/-- A recursion principle for `bit` representations of natural numbers.
-  For a predicate `C : Nat → Sort*`, if instances can be
-  constructed for natural numbers of the form `bit b n`,
-  they can be constructed for all natural numbers. -/
-def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) : ∀ n, C n :=
-  fun n =>
-    if n0 : n = 0 then by
-      simp only [n0]
-      exact z
-    else by
-      let n' := div2 n
-      have _x : bit (bodd n) n' = n := by
-        apply bit_decomp n
-      rw [← _x]
-      exact f (bodd n) n' (binaryRec z f n')
-  decreasing_by exact binaryRec_decreasing n0
 #align nat.binary_rec Nat.binaryRec
 
 /-- `size n` : Returns the size of a natural number in
@@ -240,11 +212,6 @@ def ldiff : ℕ → ℕ → ℕ :=
   bitwise fun a b => a && not b
 #align nat.ldiff Nat.ldiff
 
-@[simp]
-lemma binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) :
-    binaryRec z f 0 = z := by
-  rw [binaryRec]
-  rfl
 #align nat.binary_rec_zero Nat.binaryRec_zero
 
 /-! bitwise ops -/
@@ -278,12 +245,7 @@ lemma shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (sh
 lemma shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
   fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]
 
--- Not a `simp` lemma, as later `simp` will be able to prove this.
-lemma testBit_bit_zero (b n) : testBit (bit b n) 0 = b := by
-  rw [testBit, bit]
-  cases b
-  · simp [bit0, ← Nat.mul_two]
-  · simp [bit0, bit1, ← Nat.mul_two]
+@[deprecated (since := "2024-06-09")] alias testBit_bit_zero := bit_testBit_zero
 
 #align nat.test_bit_zero Nat.testBit_zero
 
@@ -301,34 +263,12 @@ lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
   exact this
 #align nat.test_bit_succ Nat.testBit_succ
 
-lemma binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)}
-    (h : f false 0 z = z) (b n) : binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
-  rw [binaryRec]
-  split_ifs with h'
-  · generalize binaryRec z f (bit b n) = e
-    revert e
-    have bf := bodd_bit b n
-    have n0 := div2_bit b n
-    rw [h'] at bf n0
-    simp only [bodd_zero, div2_zero] at bf n0
-    subst bf n0
-    rw [binaryRec_zero]
-    intros
-    rw [h, eq_mpr_eq_cast, cast_eq]
-  · simp only; generalize_proofs h
-    revert h
-    rw [bodd_bit, div2_bit]
-    intros; simp only [eq_mpr_eq_cast, cast_eq]
 #align nat.binary_rec_eq Nat.binaryRec_eq
 #noalign nat.bitwise_bit_aux
 
 /-! ### `boddDiv2_eq` and `bodd` -/
 
 
-@[simp]
-theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := rfl
-#align nat.bodd_div2_eq Nat.boddDiv2_eq
-
 @[simp]
 theorem bodd_bit0 (n) : bodd (bit0 n) = false :=
   bodd_bit false n
@@ -406,10 +346,6 @@ theorem pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n := by
   · apply succ_pos
 #align nat.pos_of_bit0_pos Nat.pos_of_bit0_pos
 
-@[simp]
-theorem bitCasesOn_bit {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (b : Bool) (n : ℕ) :
-    bitCasesOn (bit b n) H = H b n :=
-  eq_of_heq <| (eq_rec_heq _ _).trans <| by rw [bodd_bit, div2_bit]
 #align nat.bit_cases_on_bit Nat.bitCasesOn_bit
 
 @[simp]
@@ -441,11 +377,6 @@ protected theorem bit0_eq_zero {n : ℕ} : bit0 n = 0 ↔ n = 0 :=
   ⟨Nat.eq_zero_of_add_eq_zero_left, fun h => by simp [h]⟩
 #align nat.bit0_eq_zero Nat.bit0_eq_zero
 
-theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
-  constructor
-  · cases b <;> simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
-  · rintro ⟨rfl, rfl⟩
-    rfl
 #align nat.bit_eq_zero_iff Nat.bit_eq_zero_iff
 
 protected lemma bit0_le (h : n ≤ m) : bit0 n ≤ bit0 m :=
@@ -538,50 +469,10 @@ theorem bit_le_bit1_iff : ∀ {b : Bool}, bit b m ≤ bit1 n ↔ m ≤ n
 #align nat.bit_le_bit1_iff Nat.bit_le_bit1_iff
 -/
 
-/--
-The same as `binaryRec_eq`,
-but that one unfortunately requires `f` to be the identity when appending `false` to `0`.
-Here, we allow you to explicitly say that that case is not happening,
-i.e. supplying `n = 0 → b = true`. -/
-theorem binaryRec_eq' {C : ℕ → Sort*} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
-    (h : f false 0 z = z ∨ (n = 0 → b = true)) :
-    binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
-  rw [binaryRec]
-  split_ifs with h'
-  · rcases bit_eq_zero_iff.mp h' with ⟨rfl, rfl⟩
-    rw [binaryRec_zero]
-    simp only [imp_false, or_false_iff, eq_self_iff_true, not_true] at h
-    exact h.symm
-  · dsimp only []
-    generalize_proofs e
-    revert e
-    rw [bodd_bit, div2_bit]
-    intros
-    rfl
-#align nat.binary_rec_eq' Nat.binaryRec_eq'
+@[deprecated (since := "2024-06-09")] alias binaryRec_eq' := Nat.binaryRec_eq
 
-/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
-  the bit being appended is `true`-/
-@[elab_as_elim]
-def binaryRec' {C : ℕ → Sort*} (z : C 0) (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) :
-    ∀ n, C n :=
-  binaryRec z fun b n ih =>
-    if h : n = 0 → b = true then f b n h ih
-    else by
-      convert z
-      rw [bit_eq_zero_iff]
-      simpa using h
+#align nat.binary_rec_eq' Nat.binaryRec_eq'
 #align nat.binary_rec' Nat.binaryRec'
-
-/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
-@[elab_as_elim]
-def binaryRecFromOne {C : ℕ → Sort*} (z₀ : C 0) (z₁ : C 1) (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) :
-    ∀ n, C n :=
-  binaryRec' z₀ fun b n h ih =>
-    if h' : n = 0 then by
-      rw [h', h h']
-      exact z₁
-    else f b n h' ih
 #align nat.binary_rec_from_one Nat.binaryRecFromOne
 
 @[simp]
@@ -591,7 +482,7 @@ theorem zero_bits : bits 0 = [] := by simp [Nat.bits]
 @[simp]
 theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
     (bit b n).bits = b :: n.bits := by
-  rw [Nat.bits, binaryRec_eq']
+  rw [Nat.bits, Nat.bits, binaryRec_eq]
   simpa
 #align nat.bits_append_bit Nat.bits_append_bit
 
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 21f60c15b1871..4d679c6e66464 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -66,20 +66,11 @@ lemma bitwise_zero : bitwise f 0 0 = 0 := by
 #align nat.bitwise_zero Nat.bitwise_zero
 
 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, bit1, bit0, Bool.cond_eq_ite]
-  split_ifs <;> rfl
-
-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
-  rw [Eq.rec_eq_cast]
-  rw [binaryRec]
-  dsimp only
-  rw [dif_neg h, eq_mpr_eq_cast]
+  simp [hn, hm, mod_two_iff_bod, bit, div2_val]
 
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
@@ -96,23 +87,13 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by
     <;> simp_all (config := {decide := true})
 #align nat.bitwise_bit Nat.bitwise_bit
 
-lemma bit_mod_two (a : Bool) (x : ℕ) :
-    bit a x % 2 = if a then 1 else 0 := by
-  #adaptation_note /-- nightly-2024-03-16: simp was
-  -- simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, ← mul_two,
-  --   Bool.cond_eq_ite] -/
-  simp only [bit, ite_apply, bit1, bit0, ← mul_two, Bool.cond_eq_ite]
-  split_ifs <;> simp [Nat.add_mod]
-
-@[simp]
 lemma bit_mod_two_eq_zero_iff (a x) :
     bit a x % 2 = 0 ↔ !a := by
-  rw [bit_mod_two]; split_ifs <;> simp_all
+  simp
 
-@[simp]
 lemma bit_mod_two_eq_one_iff (a x) :
     bit a x % 2 = 1 ↔ a := by
-  rw [bit_mod_two]; split_ifs <;> simp_all
+  simp
 
 @[simp]
 theorem lor_bit : ∀ a m b n, bit a m ||| bit b n = bit (a || b) (m ||| n) :=
@@ -184,7 +165,6 @@ lemma bitwise_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool)
   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, bit1, bit0, Bool.cond_eq_ite]
-  split_ifs with hf <;> rfl
 
 lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
     bitwise f =
@@ -200,8 +180,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
@@ -307,12 +287,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.strongInductionOn 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]
 #align nat.bitwise_swap Nat.bitwise_swap
 
 /-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index c9c548e0a5cc3..405cbd63a6e8b 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -627,9 +627,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, Nat.bit0_val n]
-    · simpa [pos_iff_ne_zero, Nat.bit0_eq_zero]
-  · simpa [Nat.bit, Nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
+    · simpa [bit_false, bit0_val n]
+    · simpa [pos_iff_ne_zero, bit_eq_zero_iff, - bit_false]
+  · simpa [bit_true, bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
 #align nat.digits_two_eq_bits Nat.digits_two_eq_bits
 
 /-! ### Modular Arithmetic -/
diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean
index 97d6b9bd45c41..b2b95423c96b6 100644
--- a/Mathlib/Data/Nat/EvenOddRec.lean
+++ b/Mathlib/Data/Nat/EvenOddRec.lean
@@ -42,7 +42,7 @@ theorem evenOddRec_even {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i →
     | _, rfl => by
       rw [evenOddRec, binaryRec_eq]
       · apply eq_rec_heq
-      · exact H
+      · exact .inl H
   eq_of_heq (this _ (bit0_val _))
 #align nat.even_odd_rec_even Nat.evenOddRec_even
 
@@ -55,7 +55,7 @@ theorem evenOddRec_odd {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P
     | _, rfl => by
       rw [evenOddRec, binaryRec_eq]
       · apply eq_rec_heq
-      · exact H
+      · exact .inl H
   eq_of_heq (this _ (bit1_val _))
 #align nat.even_odd_rec_odd Nat.evenOddRec_odd
 
diff --git a/Mathlib/Data/Nat/Fib/Basic.lean b/Mathlib/Data/Nat/Fib/Basic.lean
index 29415ad8827c3..e9785b589dec8 100644
--- a/Mathlib/Data/Nat/Fib/Basic.lean
+++ b/Mathlib/Data/Nat/Fib/Basic.lean
@@ -248,15 +248,13 @@ theorem fast_fib_aux_bit_tt (n : ℕ) :
 #align nat.fast_fib_aux_bit_tt Nat.fast_fib_aux_bit_tt
 
 theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1)) := by
-  apply Nat.binaryRec _ (fun b n' ih => _) n
-  · simp [fastFibAux]
-  · intro b
-    intro n'
-    intro ih
+  induction n using Nat.binaryRec with
+  | z => simp [fastFibAux]
+  | f b n' ih =>
     cases b <;>
           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_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
+          simp [bit_false, bit_true, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
 #align nat.fast_fib_aux_eq Nat.fast_fib_aux_eq
 
 theorem fast_fib_eq (n : ℕ) : fastFib n = fib n := by rw [fastFib, fast_fib_aux_eq]
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index 38621339aa835..cf4132740b765 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -305,7 +305,7 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
     cases b
     · simpa [bit0_eq_two_mul n]
     · suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
-        simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0,
+        simpa [multiplicity.mul, h2, ← two_mul, Nat.bit1_eq_succ_bit0,
           bit0_eq_two_mul n, factorial]
       rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
       refine this.trans ?_
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 89afd428e1bd8..36a557daedb29 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -58,7 +58,7 @@ theorem size_bit {b n} (h : bit b n ≠ 0) : size (bit b n) = succ (size n) := b
     lhs
     rw [binaryRec]
     simp [h]
-  rw [div2_bit]
+  rfl
 #align nat.size_bit Nat.size_bit
 
 section
@@ -107,22 +107,22 @@ theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n := by
 theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
   rw [← one_shiftLeft]
   have : ∀ {n}, n = 0 → n < 1 <<< (size n) := by simp
-  apply binaryRec _ _ n
-  · apply this rfl
-  intro b n IH
-  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 [shiftLeft_eq, shiftRight_eq_div_pow] using IH)
+  induction n using binaryRec with
+  | z => apply this rfl
+  | f b n IH =>
+    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 [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 :=
   ⟨fun h => lt_of_lt_of_le (lt_size_self _) (pow_le_pow_of_le_right (by decide) h), by
-    rw [← one_shiftLeft]; revert n
-    apply binaryRec _ _ m
-    · intro n
-      simp
-    · intro b m IH n h
+    rw [← one_shiftLeft]
+    induction m using binaryRec generalizing n with
+    | z => intro; simp
+    | f b m IH =>
+      intro h
       by_cases e : bit b m = 0
       · simp [e]
       rw [size_bit e]
diff --git a/Mathlib/Data/Num/Basic.lean b/Mathlib/Data/Num/Basic.lean
index 5271c5099b073..dc7a97945649f 100644
--- a/Mathlib/Data/Num/Basic.lean
+++ b/Mathlib/Data/Num/Basic.lean
@@ -5,9 +5,10 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Lean.Linter.Deprecated
 import Mathlib.Mathport.Rename
+import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Init.ZeroOne
-import Mathlib.Data.Nat.Bits
+import Mathlib.Tactic.TypeStar
 
 #align_import data.num.basic from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 /-!
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 758bc52285767..8586e87f3bebd 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -239,7 +239,7 @@ theorem ofNat'_zero : Num.ofNat' 0 = 0 := by simp [Num.ofNat']
 #align num.of_nat'_zero Num.ofNat'_zero
 
 theorem ofNat'_bit (b n) : ofNat' (Nat.bit b n) = cond b Num.bit1 Num.bit0 (ofNat' n) :=
-  Nat.binaryRec_eq rfl _ _
+  Nat.binaryRec_eq _ _ (.inl rfl)
 #align num.of_nat'_bit Num.ofNat'_bit
 
 @[simp]
@@ -762,8 +762,8 @@ 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 [Nat.bit, bit0_of_bit0, bit1_of_bit1, Nat.cast_bit0, Nat.cast_bit1]
-    · rfl
+    · cases b <;> simp [Nat.bit, ← bit0_of_bit0, ← bit1_of_bit1, _root_.bit0, _root_.bit1]
+    · left; rfl
 #align num.of_nat'_eq Num.ofNat'_eq
 
 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 947009ef19840..73f2c2da16652 100644
--- a/Mathlib/Logic/Denumerable.lean
+++ b/Mathlib/Logic/Denumerable.lean
@@ -142,9 +142,8 @@ set_option linter.deprecated false in
 instance sum : Denumerable (Sum α β) :=
   ⟨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, bit0_eq_two_mul, bit1]⟩
+    simp only [decodeSum, decode_eq_ofNat, Option.map_some', Option.mem_def, Sum.exists]
+    cases bodd n <;> simp [bit, encodeSum, two_mul]⟩
 #align denumerable.sum Denumerable.sum
 
 section Sigma
diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index 9140af80780a0..2eed936a73a76 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -270,9 +270,9 @@ def encodeSum : Sum α β → ℕ
 
 /-- Explicit decoding function for the sum of two encodable types. -/
 def decodeSum (n : ℕ) : Option (Sum α β) :=
-  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
 #align encodable.decode_sum Encodable.decodeSum
 
 /-- If `α` and `β` are encodable, then so is their sum. -/
@@ -332,7 +332,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]
 #align encodable.decode_ge_two Encodable.decode_ge_two
 
 noncomputable instance _root_.Prop.encodable : Encodable Prop :=
diff --git a/Mathlib/Logic/Equiv/Nat.lean b/Mathlib/Logic/Equiv/Nat.lean
index c938dd079da83..f9fa63aec4bbf 100644
--- a/Mathlib/Logic/Equiv/Nat.lean
+++ b/Mathlib/Logic/Equiv/Nat.lean
@@ -27,9 +27,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]
 #align equiv.bool_prod_nat_equiv_nat Equiv.boolProdNatEquivNat
 #align equiv.bool_prod_nat_equiv_nat_symm_apply Equiv.boolProdNatEquivNat_symm_apply
 #align equiv.bool_prod_nat_equiv_nat_apply Equiv.boolProdNatEquivNat_apply

From 5ccab297d794b9ae8b7d11cc0d1fe61c6be39b3c Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sun, 9 Jun 2024 08:48:55 +0800
Subject: [PATCH 02/37] Update Mathlib.lean

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 819966bca8ac9..c84a6a02d44e0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2102,6 +2102,7 @@ import Mathlib.Data.Multiset.Sym
 import Mathlib.Data.NNRat.BigOperators
 import Mathlib.Data.NNRat.Defs
 import Mathlib.Data.NNRat.Lemmas
+import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Cast.Basic

From 9f429e9f49207cc3397048e52e22dd89c4787669 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sun, 9 Jun 2024 10:08:41 +0800
Subject: [PATCH 03/37] fix

---
 Mathlib/Data/Tree/Get.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index b034da7c9adc8..028ddc8fd9933 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Wojciech Nawrocki
 -/
 import Mathlib.Data.Num.Basic
 import Mathlib.Data.Tree.Basic
+import Mathlib.Init.Data.Ordering.Basic
 
 #align_import data.tree from "leanprover-community/mathlib"@"ed989ff568099019c6533a4d94b27d852a5710d8"
 

From 584c3ce56b5e912d63deb6548af7d2475053bd70 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sat, 13 Jul 2024 18:55:09 +0800
Subject: [PATCH 04/37] fix

---
 Mathlib/Data/Nat/BinaryRec.lean    |  1 +
 Mathlib/Data/Nat/Bitwise.lean      |  8 +++-----
 Mathlib/Data/Nat/Digits.lean       | 10 +++-------
 Mathlib/Data/Nat/Multiplicity.lean |  4 +---
 Mathlib/Logic/Denumerable.lean     |  5 +----
 5 files changed, 9 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index a49066806abfa..2e9e40d114e39 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -32,6 +32,7 @@ theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1)
   cases mod_two_eq_zero_or_one n with | _ h =>
     simpa [h, shiftRight_one] using Eq.trans (by simp [h, Nat.two_mul]) (Nat.div_add_mod n 2)
 
+@[simp]
 theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
   cases n <;> cases b <;> simp [bit, ← Nat.add_assoc]
 
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index a9a9725571478..2e778797a7e49 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -145,13 +145,11 @@ theorem bit_true : bit true = bit1 :=
   rfl
 #align nat.bit_tt Nat.bit_true
 
-@[simp]
-theorem bit_eq_zero {n : ℕ} {b : Bool} : n.bit b = 0 ↔ n = 0 ∧ b = false := by
-  cases b <;> simp [Nat.bit0_eq_zero, Nat.bit1_ne_zero]
-#align nat.bit_eq_zero Nat.bit_eq_zero
+@[deprecated (since := "2024-07-13")] alias bit_eq_zero := bit_eq_zero_iff
+#align nat.bit_eq_zero Nat.bit_eq_zero_iff
 
 theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true := by
-  simpa only [not_and, Bool.not_eq_false] using (@bit_eq_zero n b).not
+  simpa only [not_and, Bool.not_eq_false] using bit_eq_zero_iff.not
 
 /-- An alternative for `bitwise_bit` which replaces the `f false false = false` assumption
 with assumptions that neither `bit a m` nor `bit b n` are `0`
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index a4e773381979a..6d6377531ac21 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -619,7 +619,6 @@ theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) :
 
 /-! ### Binary -/
 
-
 theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0 := by
   induction' n using Nat.binaryRecFromOne with b n h ih
   · simp
@@ -627,12 +626,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 [bit_false, bit0_val n]
-    · simpa [pos_iff_ne_zero, bit_eq_zero_iff, - bit_false]
-  · simpa [bit_true, bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
-    · simpa [Nat.bit, Nat.bit0_val n]
-    · simpa [Nat.bit, pos_iff_ne_zero, Nat.bit0_eq_zero]
-  · simpa [Nat.bit, Nat.bit1_val n, 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]
 #align nat.digits_two_eq_bits Nat.digits_two_eq_bits
 
 /-! ### Modular Arithmetic -/
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index 034983a03e4a8..71c6fcfee29df 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -292,7 +292,7 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
   · intro b n ih h
     by_cases hn : n = 0
     · subst hn
-      simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h
+      simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h
       simp only [h, bit_true, bit1_zero, factorial, mul_one, Nat.isUnit_iff, cast_one]
       rw [Prime.multiplicity_one]
       · simp only [zero_lt_one]
@@ -307,8 +307,6 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
     · suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
         simpa [multiplicity.mul, h2, ← two_mul, Nat.bit1_eq_succ_bit0,
           bit0_eq_two_mul n, factorial]
-        simpa [multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0, bit0_eq_two_mul n,
-          factorial]
       rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
       refine this.trans ?_
       exact mod_cast lt_succ_self _
diff --git a/Mathlib/Logic/Denumerable.lean b/Mathlib/Logic/Denumerable.lean
index 120bbc8f2d2e2..cef05c9551ab2 100644
--- a/Mathlib/Logic/Denumerable.lean
+++ b/Mathlib/Logic/Denumerable.lean
@@ -144,10 +144,7 @@ instance sum : Denumerable (Sum α β) :=
   ⟨fun n => by
     suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
     simp only [decodeSum, decode_eq_ofNat, Option.map_some', Option.mem_def, Sum.exists]
-    cases bodd n <;> simp [bit, encodeSum, two_mul]⟩
-    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, bit0, bit1, Nat.two_mul]⟩
+    cases bodd n <;> simp [bit_val, encodeSum]⟩
 #align denumerable.sum Denumerable.sum
 
 section Sigma

From fde50dfb67e76ee5d2eea6c7d4a02e2836700698 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sat, 13 Jul 2024 18:57:45 +0800
Subject: [PATCH 05/37] fix

---
 Mathlib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index a4853f84c8a8e..4952f81faaf0a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2203,8 +2203,8 @@ import Mathlib.Data.NNRat.Defs
 import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Data.NNReal.Basic
 import Mathlib.Data.NNReal.Star
-import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.BinaryRec
+import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Data.Nat.Cast.Commute

From 68a2c0b08b340d12226ef329e7d9fcd68683e55e Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sat, 13 Jul 2024 19:53:47 +0800
Subject: [PATCH 06/37] fix

---
 Mathlib/Data/Nat/Fib/Basic.lean | 2 +-
 Mathlib/Data/Nat/Size.lean      | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Nat/Fib/Basic.lean b/Mathlib/Data/Nat/Fib/Basic.lean
index 0a4fdd9c08eb9..91272a7cef1dc 100644
--- a/Mathlib/Data/Nat/Fib/Basic.lean
+++ b/Mathlib/Data/Nat/Fib/Basic.lean
@@ -254,7 +254,7 @@ theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1)) := by
     cases b <;>
           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_false, bit_true, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
+          simp [bit_val, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]
 #align nat.fast_fib_aux_eq Nat.fast_fib_aux_eq
 
 theorem fast_fib_eq (n : ℕ) : fastFib n = fib n := by rw [fastFib, fast_fib_aux_eq]
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index dc64a9c6bc2cb..afae66d88ed8d 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -23,8 +23,8 @@ theorem shiftLeft_eq_mul_pow (m) : ∀ n, m <<< n = m * 2 ^ n := shiftLeft_eq _
 theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
   | 0 => by simp [shiftLeft', pow_zero, Nat.one_mul]
   | k + 1 => by
-    rw [shiftLeft', bit_val, cond_true, add_assoc, ← Nat.mul_add_one, shiftLeft'_tt_eq_mul_pow m k,
-      mul_left_comm, mul_comm 2, pow_succ]
+    rw [shiftLeft', bit_val, Bool.toNat_true, add_assoc, ← Nat.mul_add_one,
+      shiftLeft'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2, pow_succ]
 #align nat.shiftl'_tt_eq_mul_pow Nat.shiftLeft'_tt_eq_mul_pow
 
 end

From ea3360bdf49960ac195528c3707a8ee587c78aa0 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sat, 13 Jul 2024 20:54:57 +0800
Subject: [PATCH 07/37] shake

---
 Mathlib/Data/Nat/Fib/Basic.lean    | 2 +-
 Mathlib/Data/Nat/Multiplicity.lean | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Fib/Basic.lean b/Mathlib/Data/Nat/Fib/Basic.lean
index 91272a7cef1dc..7dd30e5cd72bc 100644
--- a/Mathlib/Data/Nat/Fib/Basic.lean
+++ b/Mathlib/Data/Nat/Fib/Basic.lean
@@ -6,7 +6,7 @@ Authors: Kevin Kappelmann, Kyle Miller, Mario Carneiro
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Data.Finset.NatAntidiagonal
 import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Data.Nat.Bits
+import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Ring
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index 71c6fcfee29df..29999df0974e3 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -6,7 +6,6 @@ Authors: Chris Hughes
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Log
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Nat.Digits

From 6392674099cac4393b17ddc0aa486d6709914261 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Sat, 13 Jul 2024 21:00:06 +0800
Subject: [PATCH 08/37] fix

---
 Mathlib/Data/Nat/Multiplicity.lean | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index 29999df0974e3..17bd321b5a20d 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -292,20 +292,18 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
     by_cases hn : n = 0
     · subst hn
       simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h
-      simp only [h, bit_true, bit1_zero, factorial, mul_one, Nat.isUnit_iff, cast_one]
-      rw [Prime.multiplicity_one]
-      · simp only [zero_lt_one]
-      · decide
+      simp only [h, bit_val, mul_zero, Bool.toNat_true, zero_add, factorial_one, cast_one]
+      rw [Prime.multiplicity_one (by decide)]
+      exact zero_lt_one
     have : multiplicity 2 (2 * n)! < (2 * n : ℕ) := by
       rw [prime_two.multiplicity_factorial_mul]
       refine (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le ?_
       rw [two_mul]
       norm_cast
     cases b
-    · simpa [bit0_eq_two_mul n]
+    · simpa [bit_val]
     · suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
-        simpa [multiplicity.mul, h2, ← two_mul, Nat.bit1_eq_succ_bit0,
-          bit0_eq_two_mul n, factorial]
+        simpa [multiplicity.mul, h2, ← two_mul, bit_val, factorial]
       rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
       refine this.trans ?_
       exact mod_cast lt_succ_self _

From fd5c58dc7ddd1272529817cf2780998c7f63a40d Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Tue, 16 Jul 2024 05:06:15 +0800
Subject: [PATCH 09/37] fix merge

---
 Mathlib/Data/Nat/BinaryRec.lean | 11 ++++-------
 Mathlib/Data/Nat/Bits.lean      | 18 +++++++-----------
 2 files changed, 11 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 2e9e40d114e39..5743a676aa045 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -23,18 +23,18 @@ namespace Nat
 /-- `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 + n + 1) (n + n)
+  cond b (n <<< 1 + 1) (n <<< 1)
 
 theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
 
 theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
   simp only [bit, testBit_zero]
   cases mod_two_eq_zero_or_one n with | _ h =>
-    simpa [h, shiftRight_one] using Eq.trans (by simp [h, Nat.two_mul]) (Nat.div_add_mod n 2)
+    simpa [h, shiftRight_one] using Eq.trans (by simp [h, Nat.shiftLeft_succ]) (Nat.div_add_mod n 2)
 
 @[simp]
 theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
-  cases n <;> cases b <;> simp [bit, ← Nat.add_assoc]
+  cases n <;> cases b <;> simp [bit, Nat.shiftLeft_succ, Nat.two_mul, ← Nat.add_assoc]
 
 /-- For a predicate `C : Nat → Sort u`, if instances can be
   constructed for natural numbers of the form `bit b n`,
@@ -83,10 +83,7 @@ def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
     else f b n h' ih
 
 theorem bit_val (b n) : bit b n = 2 * n + b.toNat := by
-  rw [Nat.mul_comm]
-  induction b with
-  | false => exact congrArg (· + n) n.zero_add.symm
-  | true => exact congrArg (· + n + 1) n.zero_add.symm
+  cases b <;> rfl
 
 @[simp]
 theorem bit_div_two (b n) : bit b n / 2 = n := by
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index c90c46be258b4..83f712a480cbd 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -259,15 +259,11 @@ lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
 #align nat.binary_rec_eq Nat.binaryRec_eq
 #noalign nat.bitwise_bit_aux
 
-/-! ### `boddDiv2_eq` and `bodd` -/
-
-
-#noalign nat.bodd_bit0 Nat.bodd_bit0
-#noalign nat.div2_bit0 Nat.div2_bit0
-#noalign nat.div2_bit1 Nat.div2_bit1
-
 /-! ### `bit0` and `bit1` -/
 
+#noalign nat.bodd_bit0
+#noalign nat.div2_bit0
+#noalign nat.div2_bit1
 #noalign nat.bit0_eq_bit0
 #noalign nat.bit1_eq_bit1
 #noalign nat.bit1_eq_one
@@ -283,8 +279,8 @@ theorem bit_add' : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit b n + bit fal
   | false, _, _ => by dsimp [bit]; omega
 #align nat.bit_add' Nat.bit_add'
 
-theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0 := by
-  cases b <;> [exact Nat.bit0_ne_zero h; exact Nat.bit1_ne_zero _]
+theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0 :=
+  bit_eq_zero_iff.not.mpr (h ·.1)
 #align nat.bit_ne_zero Nat.bit_ne_zero
 
 theorem bit0_mod_two : 2 * n % 2 = 0 := by
@@ -307,13 +303,13 @@ theorem pos_of_bit0_pos {n : ℕ} (h : 0 < 2 * n) : 0 < n := by
 
 @[simp]
 theorem bitCasesOn_bit0 {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (n : ℕ) :
-    bitCasesOn (2 * n) H = H false n :=
+    bitCasesOn (bit false n) H = H false n :=
   bitCasesOn_bit H false n
 #align nat.bit_cases_on_bit0 Nat.bitCasesOn_bit0
 
 @[simp]
 theorem bitCasesOn_bit1 {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (n : ℕ) :
-    bitCasesOn (2 * n + 1) H = H true n :=
+    bitCasesOn (bit true n) H = H true n :=
   bitCasesOn_bit H true n
 #align nat.bit_cases_on_bit1 Nat.bitCasesOn_bit1
 

From 049d44240885a8ae90cda03917bc45f7abd9550a Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Tue, 16 Jul 2024 05:39:44 +0800
Subject: [PATCH 10/37] fix

---
 Mathlib/Data/Nat/Bitwise.lean      | 6 +++---
 Mathlib/Data/Nat/Multiplicity.lean | 6 +++++-
 Mathlib/Data/Nat/Size.lean         | 2 +-
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index ab37be8db66dc..23c71f73bbfb3 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -69,7 +69,7 @@ lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
   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 [hn, hm, mod_two_iff_bod, bit, div2_val]
+  simp [hn, hm, mod_two_iff_bod, bit, div2_val, Nat.shiftLeft_succ, two_mul]
 
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
@@ -77,7 +77,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
@@ -159,7 +159,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, bit1, bit0, Bool.cond_eq_ite]
+  conv_rhs => simp [bit, Bool.cond_eq_ite, Nat.shiftLeft_succ, two_mul]
 
 lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
     bitwise f =
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index 79b61a71cc9c4..8c645371befd5 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -301,8 +301,12 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
       rw [two_mul]
       norm_cast
     cases b
-    · simpa [bit_val]
+    · simpa
     · suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
         simpa [multiplicity.mul, h2, ← two_mul, bit_val, factorial]
+      rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
       refine this.trans ?_
       exact mod_cast lt_succ_self _
+#align nat.multiplicity_two_factorial_lt Nat.multiplicity_two_factorial_lt
+
+end Nat
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index a2bafe1414fea..c4782da0dbcaf 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -113,7 +113,7 @@ theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
   | f b n IH =>
     by_cases h : bit b n = 0
     · apply this h
-    rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul, ← bit0_val]
+    rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul]
     exact bit_lt_bit0 _ (by simpa [shiftLeft_eq, shiftRight_eq_div_pow] using IH)
 #align nat.lt_size_self Nat.lt_size_self
 

From 16a10ce4d07bb5a3078e60bfd6d41f8ec96db7e3 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Tue, 16 Jul 2024 06:15:30 +0800
Subject: [PATCH 11/37] fix

---
 Mathlib/Data/Nat/BinaryRec.lean  | 3 +--
 Mathlib/Data/Nat/BitIndices.lean | 4 ++--
 Mathlib/Data/Num/Lemmas.lean     | 8 ++++----
 3 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 5743a676aa045..80ace28229d70 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -29,8 +29,7 @@ theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
 
 theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
   simp only [bit, testBit_zero]
-  cases mod_two_eq_zero_or_one n with | _ h =>
-    simpa [h, shiftRight_one] using Eq.trans (by simp [h, Nat.shiftLeft_succ]) (Nat.div_add_mod n 2)
+  cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2
 
 @[simp]
 theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
diff --git a/Mathlib/Data/Nat/BitIndices.lean b/Mathlib/Data/Nat/BitIndices.lean
index b68b2bd3c5b95..2f81ab8b0583a 100644
--- a/Mathlib/Data/Nat/BitIndices.lean
+++ b/Mathlib/Data/Nat/BitIndices.lean
@@ -42,11 +42,11 @@ def bitIndices (n : ℕ) : List ℕ :=
 
 theorem bitIndices_bit_true (n : ℕ) :
     bitIndices (bit true n) = 0 :: ((bitIndices n).map (· + 1)) :=
-  binaryRec_eq rfl _ _
+  binaryRec_eq _ _ (.inl rfl)
 
 theorem bitIndices_bit_false (n : ℕ) :
     bitIndices (bit false n) = (bitIndices n).map (· + 1) :=
-  binaryRec_eq rfl _ _
+  binaryRec_eq _ _ (.inl rfl)
 
 @[simp] theorem bitIndices_two_mul_add_one (n : ℕ) :
     bitIndices (2 * n + 1) = 0 :: (bitIndices n).map (· + 1) := by
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 819482852b856..fdaa61b1d805c 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -248,7 +248,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]
-    · erw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
+    · erw [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])
 #align num.of_nat'_succ Num.ofNat'_succ
@@ -757,7 +757,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 [Nat.bit, ← bit0_of_bit0, ← bit1_of_bit1, _root_.bit0, _root_.bit1]
+    · cases b <;> simp [Nat.bit_val, two_mul, ← bit0_of_bit0, ← bit1_of_bit1]
     · left; rfl
 #align num.of_nat'_eq Num.ofNat'_eq
 
@@ -985,8 +985,8 @@ theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by
     induction' n with n IH generalizing m <;> cases' m with m m
         <;> dsimp only [PosNum.testBit, Nat.zero_eq]
     · rfl
-    · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
-    · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
+    · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.bit_testBit_zero]
+    · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.bit_testBit_zero]
     · simp
     · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
     · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]

From 7398e5be0f303487b5b7e513b751c1fb8554185e Mon Sep 17 00:00:00 2001
From: FR <zhao.yu-yang@foxmail.com>
Date: Tue, 16 Jul 2024 07:06:58 +0800
Subject: [PATCH 12/37] fix

---
 Mathlib/Data/Nat/Bits.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 83f712a480cbd..e87c0f380868c 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -303,13 +303,13 @@ theorem pos_of_bit0_pos {n : ℕ} (h : 0 < 2 * n) : 0 < n := by
 
 @[simp]
 theorem bitCasesOn_bit0 {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (n : ℕ) :
-    bitCasesOn (bit false n) H = H false n :=
+    bitCasesOn (2 * n) H = H false n :=
   bitCasesOn_bit H false n
 #align nat.bit_cases_on_bit0 Nat.bitCasesOn_bit0
 
 @[simp]
 theorem bitCasesOn_bit1 {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (n : ℕ) :
-    bitCasesOn (bit true n) H = H true n :=
+    bitCasesOn (2 * n + 1) H = H true n :=
   bitCasesOn_bit H true n
 #align nat.bit_cases_on_bit1 Nat.bitCasesOn_bit1
 

From ccb809ca06cb5993d994d7d8d31f9d7678b05cbc Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Thu, 18 Jul 2024 01:19:37 +0800
Subject: [PATCH 13/37] fix

---
 Mathlib/Data/Num/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Num/Basic.lean b/Mathlib/Data/Num/Basic.lean
index e1396f1803cd6..7c50658be8a94 100644
--- a/Mathlib/Data/Num/Basic.lean
+++ b/Mathlib/Data/Num/Basic.lean
@@ -7,7 +7,6 @@ import Lean.Linter.Deprecated
 import Mathlib.Mathport.Rename
 import Mathlib.Data.Int.Notation
 import Mathlib.Data.Nat.BinaryRec
-import Mathlib.Init.Data.Int.Basic
 import Mathlib.Init.ZeroOne
 import Mathlib.Tactic.TypeStar
 

From 38780b5a0f6d8d613820b70e05e5b51e6d4b500e Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Thu, 18 Jul 2024 01:23:10 +0800
Subject: [PATCH 14/37] fix

---
 Mathlib/Data/Nat/Bitwise.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 45bc82e93c671..e0e2566550fd7 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -210,7 +210,7 @@ theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
     rw [show b = true by
         revert h
         cases b <;> simp]
-    refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩
+    refine ⟨0, ⟨by rw [bit_testBit_zero], fun j hj => ?_⟩⟩
     obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
     rw [testBit_bit_succ, zero_testBit]
   · obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
@@ -229,7 +229,7 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
   · exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
   by_cases hi : i = 0
   · subst hi
-    simp only [testBit_bit_zero] at hn hm
+    simp only [bit_testBit_zero] at hn hm
     have : n = m :=
       eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
       <;> rw [testBit_bit_succ]

From e056180505d0c46b490199ab2c8776ccc96c4ea9 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Thu, 18 Jul 2024 01:26:58 +0800
Subject: [PATCH 15/37] fix

---
 Mathlib/Data/Nat/EvenOddRec.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean
index 6476d50c4741d..8d193927601c7 100644
--- a/Mathlib/Data/Nat/EvenOddRec.lean
+++ b/Mathlib/Data/Nat/EvenOddRec.lean
@@ -33,7 +33,7 @@ theorem evenOddRec_zero {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i →
 theorem evenOddRec_even {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
     (2 * n).evenOddRec h0 h_even h_odd = h_even n (evenOddRec h0 h_even h_odd n) := by
-  apply binaryRec_eq' false n
+  apply binaryRec_eq false n
   simp [H]
 #align nat.even_odd_rec_even Nat.evenOddRec_even
 
@@ -41,7 +41,7 @@ theorem evenOddRec_even {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i →
 theorem evenOddRec_odd {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
     (2 * n + 1).evenOddRec h0 h_even h_odd = h_odd n (evenOddRec h0 h_even h_odd n) := by
-  apply binaryRec_eq' true n
+  apply binaryRec_eq true n
   simp [H]
 #align nat.even_odd_rec_odd Nat.evenOddRec_odd
 

From 199117ab83f984709f6800f65c856e01e2f151ac Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Thu, 18 Jul 2024 02:31:20 +0800
Subject: [PATCH 16/37] shake

---
 Mathlib/Data/Nat/Bits.lean       | 1 -
 Mathlib/Data/Nat/EvenOddRec.lean | 2 +-
 Mathlib/Data/Nat/Size.lean       | 1 +
 scripts/noshake.json             | 4 +---
 4 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 979ffcbb68a3e..c28c64700e3c6 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.Group.Nat
 import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.Nat.Defs
 import Mathlib.Init.Data.List.Basic
-import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Says
diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean
index 8d193927601c7..a6d5366f9ff39 100644
--- a/Mathlib/Data/Nat/EvenOddRec.lean
+++ b/Mathlib/Data/Nat/EvenOddRec.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stuart Presnell
 -/
 import Mathlib.Algebra.Ring.Parity
-import Mathlib.Data.Nat.Bits
+import Mathlib.Data.Nat.BinaryRec
 
 #align_import data.nat.even_odd_rec from "leanprover-community/mathlib"@"18a5306c091183ac90884daa9373fa3b178e8607"
 /-! # A recursion principle based on even and odd numbers. -/
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 8d0337c86c5fe..1569290014184 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.Nat.Bits
+import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Order.Lattice
 
 #align_import data.nat.size from "leanprover-community/mathlib"@"18a5306c091183ac90884daa9373fa3b178e8607"
diff --git a/scripts/noshake.json b/scripts/noshake.json
index b53b7c91ae10d..37611ebd809a5 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -40,6 +40,7 @@
   "Mathlib.Combinatorics.SimpleGraph.Init",
   "Mathlib.Control.Traversable.Lemmas",
   "Mathlib.Data.Int.Defs",
+  "Mathlib.Data.Int.Notation",
   "Mathlib.Data.Matrix.Notation",
   "Mathlib.Data.Matroid.Init",
   "Mathlib.Data.Nat.Notation",
@@ -291,7 +292,6 @@
   "Mathlib.MeasureTheory.MeasurableSpace.Defs": ["Mathlib.Tactic.FunProp.Attr"],
   "Mathlib.Logic.Nontrivial.Defs": ["Mathlib.Init.Logic"],
   "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic"],
-  "Mathlib.Logic.Basic": ["Mathlib.Data.Int.Notation"],
   "Mathlib.LinearAlgebra.Matrix.Transvection": ["Mathlib.Data.Matrix.DMatrix"],
   "Mathlib.LinearAlgebra.Basic": ["Mathlib.Algebra.BigOperators.Group.Finset"],
   "Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional": ["Mathlib.Init.Core"],
@@ -305,7 +305,6 @@
   "Mathlib.Init.Data.Nat.GCD": ["Batteries.Data.Nat.Gcd"],
   "Mathlib.Init.Data.List.Basic": ["Batteries.Data.List.Basic"],
   "Mathlib.Init.Data.Int.Basic": ["Batteries.Data.Int.Order"],
-  "Mathlib.Init.Data.Int.Order": ["Mathlib.Data.Int.Notation"],
   "Mathlib.Init.Data.Bool.Lemmas": ["Mathlib.Tactic.AdaptationNote"],
   "Mathlib.GroupTheory.MonoidLocalization": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Geometry.Manifold.Sheaf.Smooth":
@@ -351,7 +350,6 @@
   "Mathlib.Algebra.Module.Equiv": ["Mathlib.Algebra.Star.Basic"],
   "Mathlib.Algebra.Homology.ModuleCat": ["Mathlib.Algebra.Homology.Homotopy"],
   "Mathlib.Algebra.Group.Units": ["Mathlib.Tactic.Subsingleton"],
-  "Mathlib.Algebra.Group.Defs": ["Mathlib.Data.Int.Notation"],
   "Mathlib.Algebra.GeomSum": ["Mathlib.Algebra.Order.BigOperators.Ring.Finset"],
   "Mathlib.Algebra.Category.Ring.Basic":
   ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],

From 40ed248dff96eb319bea4ac997eb3f7fd5b0623f Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 14:39:04 +0800
Subject: [PATCH 17/37] shake

---
 Mathlib/Data/Nat/Size.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 17c62282275f8..35dd738707b51 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.Nat.Bits
-import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Order.Lattice
 
 /-! Lemmas about `size`. -/

From 80ce83eef82295a4d7d74e3d4616182449c09aca Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 14:57:03 +0800
Subject: [PATCH 18/37] fix

---
 Mathlib/Data/Num/Basic.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Data/Num/Basic.lean b/Mathlib/Data/Num/Basic.lean
index 228f24561c5bc..be3b3c344c27b 100644
--- a/Mathlib/Data/Num/Basic.lean
+++ b/Mathlib/Data/Num/Basic.lean
@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Lean.Linter.Deprecated
+import Mathlib.Algebra.Group.ZeroOne
 import Mathlib.Data.Int.Notation
 import Mathlib.Data.Nat.BinaryRec
-import Mathlib.Init.ZeroOne
-import Mathlib.Tactic.TypeStar
-
 /-!
 # Binary representation of integers using inductive types
 

From e57a5d9f3613e0d11fec877d12ca946783e97343 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 15:04:40 +0800
Subject: [PATCH 19/37] fix

---
 Mathlib/Data/Tree/Get.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Tree/Get.lean b/Mathlib/Data/Tree/Get.lean
index ed6a66817bdff..b374b675b07ba 100644
--- a/Mathlib/Data/Tree/Get.lean
+++ b/Mathlib/Data/Tree/Get.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Wojciech Nawrocki
 -/
 import Mathlib.Data.Num.Basic
+import Mathlib.Data.Ordering.Basic
 import Mathlib.Data.Tree.Basic
-import Mathlib.Init.Data.Ordering.Basic
 
 /-!
 # Binary tree get operation

From 2046094f02f5518d60ad0370359cebc6951d6c49 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 15:19:47 +0800
Subject: [PATCH 20/37] fix

---
 Mathlib/Data/Nat/Bits.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index dc169fe509992..5de8f1350948c 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -114,6 +114,9 @@ lemma bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
     · simp
     · simp; omega
 
+lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
+  (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
+
 lemma bit_zero : bit false 0 = 0 :=
   rfl
 

From 432eaecf5f1d15cef1bfce3262501c9637bf8b27 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 15:40:40 +0800
Subject: [PATCH 21/37] fix

---
 Mathlib/Data/Nat/Bitwise.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index aa603121c38b2..c03f5ffa343cc 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -64,6 +64,14 @@ lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
     simp only [mod_two_of_bodd, cond]; cases bodd x <;> 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
+  rw [Eq.rec_eq_cast]
+  rw [binaryRec]
+  dsimp only
+  rw [dif_neg h, eq_mpr_eq_cast]
+
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
     bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by

From 9d9ccda556b71505d08c53fbb802add24a64fd64 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 15:50:20 +0800
Subject: [PATCH 22/37] fix

---
 Mathlib/Logic/Encodable/Basic.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index 34836e9523720..52bb82701693a 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -287,8 +287,12 @@ theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none := by
   simp only [decodeSum, div2_val]; cases bodd n <;> simp [e]
 
 noncomputable instance _root_.Prop.encodable : Encodable Prop :=
+  ofEquiv Bool Equiv.propEquivBool
 
 section Sigma
+
+variable {γ : α → Type*} [Encodable α] [∀ a, Encodable (γ a)]
+
 /-- Explicit encoding function for `Sigma γ` -/
 def encodeSigma : Sigma γ → ℕ
   | ⟨a, b⟩ => pair (encode a) (encode b)

From 209740051bedb5a4227770dea6e1356de420868a Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 24 Jul 2024 16:48:10 +0800
Subject: [PATCH 23/37] fix

---
 Mathlib/Data/Nat/Bits.lean    | 5 +++++
 Mathlib/Data/Nat/Bitwise.lean | 8 --------
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 5de8f1350948c..4174d90bafb24 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -117,6 +117,11 @@ lemma bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
 lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
   (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
 
+theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
+    (h : n ≠ 0) :
+    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
+
 lemma bit_zero : bit false 0 = 0 :=
   rfl
 
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index c03f5ffa343cc..aa603121c38b2 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -64,14 +64,6 @@ lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
     simp only [mod_two_of_bodd, cond]; cases bodd x <;> 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
-  rw [Eq.rec_eq_cast]
-  rw [binaryRec]
-  dsimp only
-  rw [dif_neg h, eq_mpr_eq_cast]
-
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
     bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by

From 6b19c7e159d9b5e10b9832cc97c92b8e42f72a95 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 7 Aug 2024 05:56:04 +0800
Subject: [PATCH 24/37] name

---
 Mathlib/Data/Int/Bitwise.lean   | 8 +++-----
 Mathlib/Data/Nat/BinaryRec.lean | 6 +++---
 Mathlib/Data/Nat/Bits.lean      | 2 --
 Mathlib/Data/Nat/Bitwise.lean   | 4 ++--
 Mathlib/Data/Num/Lemmas.lean    | 4 ++--
 5 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index ed0cfe0cbe397..195e635e8183c 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -216,12 +216,10 @@ theorem bodd_bit (b n) : bodd (bit b n) = b := by
   cases b <;> cases bodd n <;> simp [(show bodd 2 = false by rfl)]
 
 @[simp]
-theorem bit_testBit_zero (b) : ∀ n, testBit (bit b n) 0 = b
-  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.bit_testBit_zero
+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.bit_testBit_zero, Bool.not_not]
-
-@[deprecated (since := "2024-06-09")] alias testBit_bit_zero := bit_testBit_zero
+    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 80ace28229d70..434acf6cb2469 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -97,7 +97,7 @@ theorem bit_mod_two (b n) : bit b n % 2 = b.toNat := by
 @[simp] theorem bit_shiftRight_one (b n) : bit b n >>> 1 = n :=
   bit_div_two b n
 
-theorem bit_testBit_zero (b n) : (bit b n).testBit 0 = b := by
+theorem testBit_bit_zero (b n) : (bit b n).testBit 0 = b := by
   simp
 
 @[simp]
@@ -105,7 +105,7 @@ theorem bitCasesOn_bit {C : Nat → Sort u} (h : ∀ b n, C (bit b n)) (b : Bool
     bitCasesOn (bit b n) h = h b n := by
   change congrArg C (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
   generalize congrArg C (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
-  rw [bit_testBit_zero, bit_shiftRight_one]
+  rw [testBit_bit_zero, bit_shiftRight_one]
   intros; rfl
 
 unseal binaryRec in
@@ -127,7 +127,7 @@ theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit
     rw [binaryRec, dif_neg h']
     change congrArg C (bit b n).bit_testBit_zero_shiftRight_one ▸ f _ _ _ = _
     generalize congrArg C (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
-    rw [bit_testBit_zero, bit_shiftRight_one]
+    rw [testBit_bit_zero, bit_shiftRight_one]
     intros; rfl
 
 end Nat
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 4174d90bafb24..31a4fbaf82fef 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -187,8 +187,6 @@ lemma shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (sh
 lemma shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
   fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]
 
-@[deprecated (since := "2024-06-09")] alias testBit_bit_zero := bit_testBit_zero
-
 lemma bodd_eq_one_and_ne_zero : ∀ n, bodd n = (1 &&& n != 0)
   | 0 => rfl
   | 1 => rfl
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index aa603121c38b2..496508ac27afe 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -186,7 +186,7 @@ theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
     rw [show b = true by
         revert h
         cases b <;> simp]
-    refine ⟨0, ⟨by rw [bit_testBit_zero], fun j hj => ?_⟩⟩
+    refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩
     obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
     rw [testBit_bit_succ, zero_testBit]
   · obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
@@ -204,7 +204,7 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
   · exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
   by_cases hi : i = 0
   · subst hi
-    simp only [bit_testBit_zero] at hn hm
+    simp only [testBit_bit_zero] at hn hm
     have : n = m :=
       eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
       <;> rw [testBit_bit_succ]
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 80fbb9cffa09e..f353d7b69b801 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -863,8 +863,8 @@ theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by
     induction' n with n IH generalizing m <;> cases' m with m m
         <;> dsimp only [PosNum.testBit, Nat.zero_eq]
     · rfl
-    · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.bit_testBit_zero]
-    · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.bit_testBit_zero]
+    · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
+    · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
     · simp
     · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
     · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]

From 871aa5f1fb3ac1f643df09760edb1d18de78c5c1 Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 7 Aug 2024 06:10:16 +0800
Subject: [PATCH 25/37] golf

---
 Mathlib/Data/Nat/Bits.lean | 28 +++++++++++++---------------
 1 file changed, 13 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 31a4fbaf82fef..f36e996413023 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -73,6 +73,12 @@ 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 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 mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
   have := congr_arg bodd (mod_add_div n 2)
   simp? [not] at this says
@@ -96,12 +102,15 @@ lemma div2_one : div2 1 = 0 := rfl
 
 lemma div2_two : div2 2 = 1 := 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
+
 @[simp]
 lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
-  apply Nat.eq_of_mul_eq_mul_left (by decide : 0 < 2)
-  apply Nat.add_right_cancel (m := cond (bodd (succ n)) 1 0)
-  rw (config := { occs := .pos [1] }) [div2_add_bodd, bodd_succ, ← div2_add_bodd n]
-  cases bodd n <;> simp [succ_eq_add_one, Nat.add_comm 1, Nat.mul_add]
+  cases n using bitCasesOn with
+  | h b n => cases b <;> simp [bit_val, div2_val, succ_div]
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
 
@@ -162,17 +171,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)

From 19b05e0aaf717e9a2ec5aeb1dde88d973fce489c Mon Sep 17 00:00:00 2001
From: negiizhao <zhao.yu-yang@foxmail.com>
Date: Wed, 7 Aug 2024 06:34:34 +0800
Subject: [PATCH 26/37] golf

---
 Mathlib/Data/Nat/BinaryRec.lean |  3 ++-
 Mathlib/Data/Nat/Bits.lean      | 36 +++++++++------------------------
 2 files changed, 11 insertions(+), 28 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 434acf6cb2469..a1d76452986bd 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -94,7 +94,8 @@ theorem bit_div_two (b n) : bit b n / 2 = n := by
 theorem bit_mod_two (b n) : bit b n % 2 = b.toNat := by
   cases b <;> simp [bit_val, mul_add_mod]
 
-@[simp] theorem bit_shiftRight_one (b n) : bit b n >>> 1 = n :=
+@[simp]
+theorem bit_shiftRight_one (b n) : bit b n >>> 1 = n :=
   bit_div_two b n
 
 theorem testBit_bit_zero (b n) : (bit b n).testBit 0 = b := by
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index f36e996413023..19afc1b02bf44 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -73,25 +73,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
 
+@[simp]
 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
+  simp [bodd]
 
 lemma mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := 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]
-  cases' mod_two_eq_zero_or_one n with h h <;> rw [h] <;> rfl
+  cases n using bitCasesOn with
+  | h b n => cases b <;> simp
 
 theorem div2_add_bodd (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
   rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
@@ -102,10 +90,9 @@ lemma div2_one : div2 1 = 0 := rfl
 
 lemma div2_two : div2 2 = 1 := rfl
 
+@[simp]
 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
+  rw [div2_val, bit_div_two]
 
 @[simp]
 lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
@@ -114,14 +101,9 @@ lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
 
-lemma bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 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 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 _

From 8b6ae3bdf359a6eac80a4da8f7763673cdcc5b95 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 16:43:05 +0800
Subject: [PATCH 27/37] split to #18039

---
 Mathlib/Data/Nat/BinaryRec.lean  | 12 ++++++++++--
 Mathlib/Data/Nat/BitIndices.lean |  4 ++--
 Mathlib/Data/Nat/Bits.lean       |  2 +-
 Mathlib/Data/Nat/EvenOddRec.lean |  4 ++--
 Mathlib/Data/Num/Lemmas.lean     |  2 +-
 5 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 87a718097b5a7..ce6e593aaed3e 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -128,7 +128,12 @@ theorem binaryRec_one {motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, mot
   simp only [add_one_ne_zero, ↓reduceDIte, Nat.reduceShiftRight, binaryRec_zero]
   rfl
 
-theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0}
+/--
+The same as `binaryRec_eq`,
+but that one unfortunately requires `f` to be the identity when appending `false` to `0`.
+Here, we allow you to explicitly say that that case is not happening,
+i.e. supplying `n = 0 → b = true`. -/
+theorem binaryRec_eq' {motive : Nat → Sort u} {z : motive 0}
     {f : ∀ b n, motive n → motive (bit b n)} (b n)
     (h : f false 0 z = z ∨ (n = 0 → b = true)) :
     binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
@@ -145,6 +150,9 @@ theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0}
     rw [testBit_bit_zero, bit_shiftRight_one]
     intros; rfl
 
-@[deprecated (since := "2024-10-21")] alias binaryRec_eq' := Nat.binaryRec_eq
+theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0} {f : ∀ b n, motive n → motive (bit b n)}
+    (h : f false 0 z = z) (b n) :
+    binaryRec z f (bit b n) = f b n (binaryRec z f n) :=
+  binaryRec_eq' b n (.inl h)
 
 end Nat
diff --git a/Mathlib/Data/Nat/BitIndices.lean b/Mathlib/Data/Nat/BitIndices.lean
index 9d9c7c094edad..bd77462f10032 100644
--- a/Mathlib/Data/Nat/BitIndices.lean
+++ b/Mathlib/Data/Nat/BitIndices.lean
@@ -41,11 +41,11 @@ def bitIndices (n : ℕ) : List ℕ :=
 
 theorem bitIndices_bit_true (n : ℕ) :
     bitIndices (bit true n) = 0 :: ((bitIndices n).map (· + 1)) :=
-  binaryRec_eq _ _ (.inl rfl)
+  binaryRec_eq rfl _ _
 
 theorem bitIndices_bit_false (n : ℕ) :
     bitIndices (bit false n) = (bitIndices n).map (· + 1) :=
-  binaryRec_eq _ _ (.inl rfl)
+  binaryRec_eq rfl _ _
 
 @[simp] theorem bitIndices_two_mul_add_one (n : ℕ) :
     bitIndices (2 * n + 1) = 0 :: (bitIndices n).map (· + 1) := by
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 879b62909c224..1ca92b02d28f3 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -230,7 +230,7 @@ theorem zero_bits : bits 0 = [] := by simp [Nat.bits]
 @[simp]
 theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
     (bit b n).bits = b :: n.bits := by
-  rw [Nat.bits, Nat.bits, binaryRec_eq]
+  rw [Nat.bits, Nat.bits, binaryRec_eq']
   simpa
 
 @[simp]
diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean
index 679a7ff57f097..ce6c89abcd14f 100644
--- a/Mathlib/Data/Nat/EvenOddRec.lean
+++ b/Mathlib/Data/Nat/EvenOddRec.lean
@@ -30,14 +30,14 @@ theorem evenOddRec_zero {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i →
 theorem evenOddRec_even {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
     (2 * n).evenOddRec h0 h_even h_odd = h_even n (evenOddRec h0 h_even h_odd n) := by
-  apply binaryRec_eq false n
+  apply binaryRec_eq' false n
   simp [H]
 
 @[simp]
 theorem evenOddRec_odd {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
     (2 * n + 1).evenOddRec h0 h_even h_odd = h_odd n (evenOddRec h0 h_even h_odd n) := by
-  apply binaryRec_eq true n
+  apply binaryRec_eq' true n
   simp [H]
 
 /-- Strong recursion principle on even and odd numbers: if for all `i : ℕ` we can prove `P (2 * i)`
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 5b510f1b4a111..8546cc7de8ec6 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -201,7 +201,7 @@ theorem bit1_of_bit1 : ∀ n : Num, (n + n) + 1 = n.bit1
 theorem ofNat'_zero : Num.ofNat' 0 = 0 := by simp [Num.ofNat']
 
 theorem ofNat'_bit (b n) : ofNat' (Nat.bit b n) = cond b Num.bit1 Num.bit0 (ofNat' n) :=
-  Nat.binaryRec_eq _ _ (.inl rfl)
+  Nat.binaryRec_eq rfl _ _
 
 @[simp]
 theorem ofNat'_one : Num.ofNat' 1 = 1 := by erw [ofNat'_bit true 0, cond, ofNat'_zero]; rfl

From ccbbd753627b67491a362785d4282a97675360e4 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 16:45:53 +0800
Subject: [PATCH 28/37] fix merge

---
 Mathlib/Data/Nat/Digits.lean       | 1 +
 Mathlib/Logic/Encodable/Basic.lean | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index ffe60893f7355..7482eb191db76 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -566,6 +566,7 @@ theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) :
 
 /-! ### Binary -/
 
+
 theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0 := by
   induction' n using Nat.binaryRecFromOne with b n h ih
   · simp
diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index b8110df9d2015..9f6991abcaf39 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -231,7 +231,7 @@ def encodeSum : α ⊕ β → ℕ
   | Sum.inr b => 2 * encode b + 1
 
 /-- Explicit decoding function for the sum of two encodable types. -/
-def decodeSum (n : ℕ) : Option (Sum α β) :=
+def decodeSum (n : ℕ) : Option (α ⊕ β) :=
   match bodd n, div2 n with
   | false, m => (decode m : Option α).map Sum.inl
   | _, m => (decode m : Option β).map Sum.inr

From 4855c89f6ff2ce87826739421eb1b47ff507977f Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 17:07:23 +0800
Subject: [PATCH 29/37] cleanup

---
 Mathlib/Data/Nat/Bits.lean    | 38 +++++++++++++++++++++++++++--------
 Mathlib/Data/Nat/Bitwise.lean |  5 +++++
 2 files changed, 35 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 1ca92b02d28f3..4e6350c90acde 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -83,9 +83,6 @@ 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
 
-theorem div2_add_bodd (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
-  rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
-
 @[simp] lemma div2_zero : div2 0 = 0 := rfl
 
 @[simp] lemma div2_one : div2 1 = 0 := rfl
@@ -93,14 +90,14 @@ theorem div2_add_bodd (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
 lemma div2_two : div2 2 = 1 := rfl
 
 @[simp]
-lemma div2_bit (b n) : div2 (bit b n) = n := by
-  rw [div2_val, bit_div_two]
-
-@[simp]
-lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
+lemma div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n) := by
   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 : ℕ) : cond (bodd n) 1 0 + 2 * div2 n = n := by
@@ -137,6 +134,11 @@ 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 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 -/
 def size : ℕ → ℕ :=
@@ -182,6 +184,26 @@ lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
   simp only [bodd_eq_one_and_ne_zero] at this
   exact this
 
+/-! ### `boddDiv2_eq` and `bodd` -/
+
+
+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 :=
+  div2_bit false n
+
+-- simp can prove this
+theorem div2_bit1 (n) : div2 (2 * n + 1) = n :=
+  div2_bit true n
+
 /-! ### `bit0` and `bit1` -/
 
 theorem bit_add : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit false n + bit b m
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index c9fa8f6b6d946..4c9e9d563810c 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -65,6 +65,11 @@ lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
     simp only [mod_two_of_bodd, cond]; cases bodd x <;> rfl
   simp [hn, hm, mod_two_iff_bod, bit, div2_val, Nat.shiftLeft_succ, two_mul]
 
+theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
+    (h : n ≠ 0) :
+    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) :
     bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by

From d1de536c94cd9bf9a1dd45151c8dbc0a2bcb9405 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 17:07:48 +0800
Subject: [PATCH 30/37] cleanup

---
 Mathlib/Data/Nat/Bits.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 4e6350c90acde..990315634ec83 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -107,11 +107,6 @@ lemma bodd_add_div2 (n : ℕ) : cond (bodd n) 1 0 + 2 * div2 n = n := by
 lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
   (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
 
-theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
-    (h : n ≠ 0) :
-    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
-
 lemma bit_zero : bit false 0 = 0 :=
   rfl
 

From c47385fff3dfc1fe2dbe39640e3b336ff4fd1f9e Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 17:12:28 +0800
Subject: [PATCH 31/37] fix merge

---
 Mathlib/Data/Nat/BinaryRec.lean | 29 ++++++++++++++---------------
 Mathlib/Data/Nat/Bits.lean      |  6 +++---
 Mathlib/Data/Nat/Bitwise.lean   |  2 +-
 3 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index ce6e593aaed3e..0edc733fa68b0 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Praneeth Kolichala, Yuyang Zhao
 -/
-import Batteries.Tactic.Alias
 
 /-!
 # Binary recursion on `Nat`
@@ -21,10 +20,8 @@ universe u
 
 namespace Nat
 
-/-- `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)
+/-- `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 * ·)
 
 theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
 
@@ -66,25 +63,27 @@ decreasing_by exact bitwise_rec_lemma n0
 /-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
   the bit being appended is `true`-/
 @[elab_as_elim, specialize]
-def binaryRec' {C : Nat → Sort u} (z : C 0)
-    (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) : ∀ n, C n :=
+def binaryRec' {motive : Nat → Sort u} (z : motive 0)
+    (f : ∀ b n, (n = 0 → b = true) → motive n → motive (bit b n)) :
+    ∀ n, motive n :=
   binaryRec z fun b n ih =>
     if h : n = 0 → b = true then f b n h ih
     else
       have : bit b n = 0 := by
         rw [bit_eq_zero_iff]
-        cases n <;> cases b <;> simp at h <;> simp [h]
-      congrArg C this ▸ z
+        cases n <;> cases b <;> simp at h ⊢
+      congrArg motive this ▸ z
 
 /-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
 @[elab_as_elim, specialize]
-def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
-    (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) : ∀ n, C n :=
+def binaryRecFromOne {motive : Nat → Sort u} (z₀ : motive 0) (z₁ : motive 1)
+    (f : ∀ b n, n ≠ 0 → motive n → motive (bit b n)) :
+    ∀ n, motive n :=
   binaryRec' z₀ fun b n h ih =>
     if h' : n = 0 then
       have : bit b n = bit true 0 := by
         rw [h', h h']
-      congrArg C this ▸ z₁
+      congrArg motive this ▸ z₁
     else f b n h' ih
 
 theorem bit_val (b n) : bit b n = 2 * n + b.toNat := by
@@ -108,10 +107,10 @@ theorem testBit_bit_zero (b n) : (bit b n).testBit 0 = b := by
   simp
 
 @[simp]
-theorem bitCasesOn_bit {C : Nat → Sort u} (h : ∀ b n, C (bit b n)) (b : Bool) (n : Nat) :
+theorem bitCasesOn_bit {motive : Nat → Sort u} (h : ∀ b n, motive (bit b n)) (b : Bool) (n : Nat) :
     bitCasesOn (bit b n) h = h b n := by
-  change congrArg C (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
-  generalize congrArg C (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
+  change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
+  generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
   rw [testBit_bit_zero, bit_shiftRight_one]
   intros; rfl
 
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 990315634ec83..63e98ac519048 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -209,11 +209,11 @@ theorem bit_add' : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit b n + bit fal
   | true,  _, _ => by dsimp [bit]; omega
   | false, _, _ => by dsimp [bit]; omega
 
-theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0 :=
-  bit_eq_zero_iff.not.mpr (h ·.1)
+theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0 := by
+  cases b <;> dsimp [bit] <;> omega
 
 @[simp]
-theorem bitCasesOn_bit0 {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (n : ℕ) :
+theorem bitCasesOn_bit0 {motive : ℕ → Sort u} (H : ∀ b n, motive (bit b n)) (n : ℕ) :
     bitCasesOn (2 * n) H = H false n :=
   bitCasesOn_bit H false n
 
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 4c9e9d563810c..9a575eadb4208 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -65,7 +65,7 @@ lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
     simp only [mod_two_of_bodd, cond]; cases bodd x <;> rfl
   simp [hn, hm, mod_two_iff_bod, bit, div2_val, Nat.shiftLeft_succ, two_mul]
 
-theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
+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 = 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

From 9bfda89d724315c0e2b92dc0d543b34172a2bd23 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 17:13:03 +0800
Subject: [PATCH 32/37] `Nat.bit`

---
 Mathlib/Data/Nat/BinaryRec.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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
 

From d569f2d682e5ca612abb44ae2996a127e2c3c7b8 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 17:14:20 +0800
Subject: [PATCH 33/37] fix merge

---
 Mathlib/Data/Nat/Bits.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index 63e98ac519048..c5c57e2e40979 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.Nat.Defs
-import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.List.Defs
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs

From 2983872d4c0b43a006c66b4b3a4284e8918dc208 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 18:02:32 +0800
Subject: [PATCH 34/37] fix

---
 Mathlib/Data/Nat/Fib/Basic.lean | 2 +-
 Mathlib/Data/Num/Lemmas.lean    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

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 8546cc7de8ec6..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])
 
@@ -664,7 +664,7 @@ theorem ofNat'_eq : ∀ n, Num.ofNat' n = n :=
     rw [Nat.binaryRec_eq, IH]
     -- Porting note: `Nat.cast_bit0` & `Nat.cast_bit1` are not `simp` theorems anymore.
     · cases b <;> simp [Nat.bit_val, two_mul, ← bit0_of_bit0, ← bit1_of_bit1]
-    · left; rfl
+    · rfl
 
 theorem zneg_toZNum (n : Num) : -n.toZNum = n.toZNumNeg := by cases n <;> rfl
 

From 7e64fc89b0fedaa055787262ec2d6c78ade4c586 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 18:03:51 +0800
Subject: [PATCH 35/37] fix merge

---
 Mathlib/Data/Nat/Bits.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index c5c57e2e40979..0067e836b372d 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -46,7 +46,7 @@ def div2 (n : ℕ) : ℕ := n >>> 1
 
 theorem div2_val (n) : div2 n = n / 2 := rfl
 
-/-- `bodd n` returns `true` if `n` is odd-/
+/-- `bodd n` returns `true` if `n` is odd -/
 def bodd (n : ℕ) : Bool := 1 &&& n != 0
 
 @[simp] lemma bodd_zero : bodd 0 = false := rfl

From 96624031539da639400e7b24cc87b3435b936560 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Wed, 23 Oct 2024 16:47:51 +0800
Subject: [PATCH 36/37] fix

---
 Mathlib/Data/Num/Lemmas.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index b190a910c52ff..2060d7870b58d 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -663,8 +663,7 @@ theorem ofNat'_eq : ∀ n, Num.ofNat' n = n :=
     rw [ofNat'] at IH ⊢
     rw [Nat.binaryRec_eq _ _ (.inl rfl), IH]
     -- Porting note: `Nat.cast_bit0` & `Nat.cast_bit1` are not `simp` theorems anymore.
-    · cases b <;> simp [Nat.bit_val, two_mul, ← bit0_of_bit0, ← bit1_of_bit1]
-    · rfl
+    cases b <;> simp [Nat.bit_val, two_mul, ← bit0_of_bit0, ← bit1_of_bit1]
 
 theorem zneg_toZNum (n : Num) : -n.toZNum = n.toZNumNeg := by cases n <;> rfl
 

From 759d699569f4dbabb89cc635b09d1ff627d22ed1 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Thu, 14 Nov 2024 18:19:17 +0800
Subject: [PATCH 37/37] `csimp`

---
 Mathlib/Data/Nat/BinaryRec.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 28cb2d1357725..f9d203b564a84 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -25,8 +25,13 @@ namespace Nat
 /-- `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 (2 * n + 1) (2 * n)
+
+private def bitImpl (b : Bool) (n : Nat) : Nat :=
   cond b (n <<< 1 + 1) (n <<< 1)
 
+@[csimp] theorem bit_eq_bitImpl : bit = bitImpl := rfl
+
 theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
 
 @[simp]