From dde0327eea7bbc787dfb3e2c95c888d775139cc4 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 22 Oct 2023 22:18:27 +0800
Subject: [PATCH 01/26] feat: de-mathlib `Nat.binaryRec`

---
 Std/Data/Nat/Basic.lean  |  17 +++
 Std/Data/Nat/Lemmas.lean | 233 ++++++++++++++++++++++++++++++++++++++-
 Std/Logic.lean           |   4 +
 3 files changed, 249 insertions(+), 5 deletions(-)

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index c952e64845..27c914cdc0 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -126,3 +126,20 @@ where
     else
       guess
 termination_by iter guess => guess
+
+/-- `bodd n` returns `true` if `n` is odd-/
+def bodd (n : Nat) : Bool :=
+  (1 &&& n) != 0
+
+/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
+def div2 (n : Nat) : Nat :=
+  n >>> 1
+
+/-- `bit b` appends the digit `b` to the binary representation of
+  its natural number input. -/
+def bit (b : Bool) (n : Nat) : Nat :=
+  cond b (n + n + 1) (n + n)
+
+/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
+def testBit (m n : Nat) : Bool :=
+  bodd (m >>> n)
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index a1a0ac1617..1f38b76fc9 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -287,6 +287,9 @@ theorem one_add (n : Nat) : 1 + n = succ n := by simp [Nat.add_comm]
 theorem eq_zero_of_add_eq_zero {n m : Nat} (H : n + m = 0) : n = 0 ∧ m = 0 :=
   ⟨Nat.eq_zero_of_add_eq_zero_right H, Nat.eq_zero_of_add_eq_zero_left H⟩
 
+protected theorem add_eq_zero {n m : Nat} : n + m = 0 ↔ n = 0 ∧ m = 0 :=
+  ⟨eq_zero_of_add_eq_zero, by simp (config := {contextual := true})⟩
+
 protected theorem add_left_cancel_iff {n m k : Nat} : n + m = n + k ↔ m = k :=
   ⟨Nat.add_left_cancel, fun | rfl => rfl⟩
 
@@ -699,11 +702,6 @@ theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
   | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
   | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
 
-theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by simp) with
-  | 0, _ => .inl rfl
-  | 1, _ => .inr rfl
-
 theorem le_of_mod_lt {a b : Nat} (h : a % b < a) : b ≤ a :=
   Nat.not_lt.1 fun hf => (ne_of_lt h).elim (Nat.mod_eq_of_lt hf)
 
@@ -781,6 +779,32 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
 theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
   rw [add_mod_mod, mod_add_mod]
 
+theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
+  match n % 2, @Nat.mod_lt n 2 (by simp) with
+  | 0, _ => .inl rfl
+  | 1, _ => .inr rfl
+
+@[simp]
+theorem mod_two_ne_one (n : Nat) : ¬n % 2 = 1 ↔ n % 2 = 0 := by
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+@[simp]
+theorem mod_two_ne_zero (n : Nat) : ¬n % 2 = 0 ↔ n % 2 = 1 := by
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+@[simp]
+theorem mod_two_add_succ_mod_two (n : Nat) : n % 2 + (n + 1) % 2 = 1 := by
+  rw [add_mod]
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+@[simp]
+theorem succ_mod_two_add_mod_two (n : Nat) : (n + 1) % 2 + n % 2 = 1 := by
+  rw [Nat.add_comm, mod_two_add_succ_mod_two]
+
+theorem succ_mod_two_eq_one_sub_mod_two (n : Nat) : (n + 1) % 2 = 1 - n % 2 := by
+  rw [add_mod]
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
 /-! ### pow -/
 
 theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
@@ -991,3 +1015,202 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
   | k + 1 => by
     rw [shiftRight_add, shiftRight_eq_div_pow m k]
     simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ]
+
+/-! ### shiftLeft -/
+
+theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
+
+theorem shiftLeft_succ (m n) : m <<< (n + 1) = 2 * (m <<< n) := by
+  simp only [shiftLeft_eq, Nat.pow_add, Nat.pow_one, ← Nat.mul_assoc, Nat.mul_comm]
+
+/-! ### bitwise -/
+
+@[simp]
+theorem bitwise_zero_left (m : Nat) : bitwise f 0 m = if f false true then m else 0 :=
+  rfl
+
+@[simp]
+theorem bitwise_zero_right (n : Nat) : bitwise f n 0 = if f true false then n else 0 := by
+  unfold bitwise
+  simp only [ite_self, decide_False, Nat.zero_div, ite_true]
+  cases n <;> simp
+
+theorem bitwise_zero : bitwise f 0 0 = 0 := by
+  simp only [bitwise_zero_right, ite_self]
+
+/-! ### bodd -/
+
+theorem bit_val (b n) : bit b n = cond b 1 0 + 2 * n := by
+  cases b <;> rw [Nat.add_comm, Nat.mul_comm]
+  · exact congrArg (· + n) n.zero_add.symm
+  · exact congrArg (· + n + 1) n.zero_add.symm
+
+@[simp]
+theorem bodd_zero : bodd 0 = false :=
+  rfl
+
+@[simp]
+theorem bodd_one : bodd 1 = true :=
+  rfl
+
+@[simp]
+theorem bodd_two : bodd 2 = false :=
+  rfl
+
+theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
+  dsimp [bodd, (· &&& ·), AndOp.and, land]
+  unfold bitwise
+  by_cases n0 : n = 0
+  · simp [n0]
+  · simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
+      show 1 / 2 = 0 by decide]
+    cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+theorem bodd_eq_mod_two_bne_zero (n : Nat) : bodd n = (n % 2 != 0) := by
+  rw [mod_two_of_bodd]
+  cases bodd n with | false | true => rfl
+
+@[simp]
+theorem bodd_succ (n : Nat) : bodd (succ n) = not (bodd n) := by
+  simp only [bodd_eq_mod_two_bne_zero, succ_eq_add_one, succ_mod_two_eq_one_sub_mod_two]
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+@[simp]
+theorem bodd_add (m n : Nat) : bodd (m + n) = (bodd m != bodd n) := by
+  induction n with
+  | zero => simp [bne]
+  | succ n ih => simp [add_succ, ih, bne, Bool.not_beq_not]
+
+@[simp]
+theorem bodd_mul (m n : Nat) : bodd (m * n) = (bodd m && bodd n) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp [mul_succ, ih]
+    cases bodd m <;> cases bodd n <;> rfl
+
+theorem bodd_bit (b n) : bodd (bit b n) = b := by
+  rw [bit_val, Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul]
+  cases b <;> cases bodd n <;> rfl
+
+/-! ### div2 -/
+
+theorem div2_val (n) : div2 n = n / 2 := rfl
+
+@[simp]
+theorem div2_zero : div2 0 = 0 :=
+  rfl
+
+theorem div2_one : div2 1 = 0 :=
+  rfl
+
+theorem div2_two : div2 2 = 1 :=
+  rfl
+
+theorem div2_eq_div_two (n : Nat) : div2 n = n / 2 := rfl
+
+theorem bodd_add_div2 (n : Nat) : cond (bodd n) 1 0 + 2 * div2 n = n := by
+  rw [← mod_two_of_bodd, div2_eq_div_two, Nat.mod_add_div]
+
+@[simp]
+theorem div2_succ (n : Nat) : 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_left_cancel (n := cond (bodd (succ n)) 1 0)
+  rw (config := {occs := .pos [1]}) [bodd_add_div2, bodd_succ, ← bodd_add_div2 n]
+  cases bodd n <;> simp [succ_eq_add_one, Nat.add_comm 1, Nat.mul_add]
+
+theorem div2_bit (b n) : div2 (bit b n) = n := by
+  rw [bit_val, div2_val, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
+  · cases b <;> decide
+  · decide
+
+theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
+  (bit_val _ _).trans (bodd_add_div2 _)
+
+/-! ### binary rec/cases -/
+
+/-- 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. -/
+def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
+
+theorem 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)
+    (Nat.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 u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[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 by rw [n0]; exact z
+  else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)
+  decreasing_by exact binaryRec_decreasing n0
+
+@[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 := by
+  rw [binaryRec]
+  rfl
+
+theorem 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]
+  by_cases h : bit b n = 0
+  -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0`
+  case pos h' =>
+    rw [dif_pos h]
+    have bf := bodd_bit b n
+    have n0 := div2_bit b n
+    rw [h] at bf n0
+    dsimp at bf n0
+    subst bf n0
+    exact h'.symm
+  case neg h' =>
+    simp only [dif_neg h]
+    generalize bit_decomp (bit b n) = e
+    revert e
+    rw [bodd_bit, div2_bit]
+    intros; rfl
+
+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 = bit_decomp n ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
+  rw [binaryRec, dif_neg h]
+  generalize bit_decomp n = e; revert e
+  apply bitCasesOn n
+  intro _ _
+  rw [bodd_bit, div2_bit]
+  intro; rfl
+
+theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
+  constructor
+  · cases b <;> simp [Nat.bit, Nat.add_eq_zero]
+  · simp (config := {contextual := true})
+
+/-- 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 : 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 by
+      have : bit b n = 0 := by
+        rw [Decidable.not_imp, Bool.not_eq_true] at h
+        rwa [bit_eq_zero_iff]
+      exact this ▸ z
+
+/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
+@[elab_as_elim]
+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 by
+      rw [h', h h']
+      exact z₁
+    else f b n h' ih
diff --git a/Std/Logic.lean b/Std/Logic.lean
index db0c1c9796..8fa22d100f 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -812,3 +812,7 @@ theorem Bool.eq_false_iff {b : Bool} : b = false ↔ b ≠ true :=
 theorem Bool.eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩
+
+@[simp] theorem Bool.beq_true (b : Bool) : (b == true) = b := by cases b <;> rfl
+@[simp] theorem Bool.beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
+theorem Bool.not_beq_not (a b : Bool) : (!a == !b) = (a == b) := by cases a <;> cases b <;> rfl

From 148c53f1beb7c85efd3b0a456f7a8ce59e75b039 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 22 Oct 2023 22:21:56 +0800
Subject: [PATCH 02/26] specialize

---
 Std/Data/Nat/Lemmas.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 1f38b76fc9..439f0b2801 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1132,6 +1132,7 @@ theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
 /-- 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. -/
+@[specialize]
 def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
 
 theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
@@ -1145,7 +1146,7 @@ theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
   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. -/
-@[specialize]
+@[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 by rw [n0]; exact z
   else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)
@@ -1194,7 +1195,7 @@ theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = fal
 
 /-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
   the bit being appended is `true`-/
-@[elab_as_elim]
+@[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 =>
@@ -1206,7 +1207,7 @@ def binaryRec' {C : Nat → Sort u} (z : C 0)
       exact this ▸ z
 
 /-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
-@[elab_as_elim]
+@[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 =>

From 6b9474b27315176980d0e60b461a385fd97fc1c6 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 22 Oct 2023 22:22:51 +0800
Subject: [PATCH 03/26] lint

---
 Std/Data/Nat/Lemmas.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 439f0b2801..f9ead2aa88 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1049,11 +1049,9 @@ theorem bit_val (b n) : bit b n = cond b 1 0 + 2 * n := by
 theorem bodd_zero : bodd 0 = false :=
   rfl
 
-@[simp]
 theorem bodd_one : bodd 1 = true :=
   rfl
 
-@[simp]
 theorem bodd_two : bodd 2 = false :=
   rfl
 

From 230166fceb7522d5f7ecf273eebc8db9ddc87276 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 22 Oct 2023 22:34:25 +0800
Subject: [PATCH 04/26] inline

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

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index f9ead2aa88..e04ec3077a 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1130,7 +1130,7 @@ theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
 /-- 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. -/
-@[specialize]
+@[inline]
 def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
 
 theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by

From 730782c8e2eba727bc226ad1596e58a69abfa3c2 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Mon, 23 Oct 2023 00:01:53 +0800
Subject: [PATCH 05/26] generalize & golf

---
 Std/Data/Nat/Lemmas.lean | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index e04ec3077a..fc454e03db 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Std.Logic
 import Std.Tactic.Basic
+import Std.Tactic.RCases
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.Nat.Basic
 
@@ -1125,6 +1126,11 @@ theorem div2_bit (b n) : div2 (bit b n) = n := by
 theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
   (bit_val _ _).trans (bodd_add_div2 _)
 
+theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
+  constructor
+  · cases b <;> simp [Nat.bit, Nat.add_eq_zero]
+  · simp (config := {contextual := true})
+
 /-! ### binary rec/cases -/
 
 /-- For a predicate `C : Nat → Sort u`, if instances can be
@@ -1156,18 +1162,15 @@ theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (b
   rw [binaryRec]
   rfl
 
-theorem 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
+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
   rw [binaryRec]
   by_cases h : bit b n = 0
   -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0`
   case pos h' =>
-    rw [dif_pos h]
-    have bf := bodd_bit b n
-    have n0 := div2_bit b n
-    rw [h] at bf n0
-    dsimp at bf n0
-    subst bf n0
+    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h
+    simp only [or_false] at h'
     exact h'.symm
   case neg h' =>
     simp only [dif_neg h]
@@ -1186,11 +1189,6 @@ theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n 
   rw [bodd_bit, div2_bit]
   intro; rfl
 
-theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
-  constructor
-  · cases b <;> simp [Nat.bit, Nat.add_eq_zero]
-  · simp (config := {contextual := true})
-
 /-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
   the bit being appended is `true`-/
 @[elab_as_elim, specialize]

From 9da444d48954c506c79137c0adaf39da35c2a168 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Mon, 23 Oct 2023 00:21:12 +0800
Subject: [PATCH 06/26] mathlib dislike `binaryRec` with `elab_as_elim`

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

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index fc454e03db..a643631db0 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1150,7 +1150,7 @@ theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
   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]
+@[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 by rw [n0]; exact z
   else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)

From 6c6cd815841258e65ab96224c8f161912902fbdd Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Mon, 23 Oct 2023 20:59:31 +0800
Subject: [PATCH 07/26] move & golf

---
 Std/Data/Nat/Basic.lean  | 72 +++++++++++++++++++++++++++++++++++
 Std/Data/Nat/Lemmas.lean | 82 +---------------------------------------
 Std/Logic.lean           |  2 +
 3 files changed, 76 insertions(+), 80 deletions(-)

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 27c914cdc0..902f05c84e 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -143,3 +143,75 @@ def bit (b : Bool) (n : Nat) : Nat :=
 /-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
 def testBit (m n : Nat) : Bool :=
   bodd (m >>> n)
+
+theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
+  cases b <;> rw [Nat.mul_comm]
+  · exact congrArg (· + n) n.zero_add.symm
+  · exact congrArg (· + n + 1) n.zero_add.symm
+
+theorem div2_val (n) : div2 n = n / 2 := rfl
+
+theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
+  match n % 2, @Nat.mod_lt n 2 (by simp) with
+  | 0, _ => .inl rfl
+  | 1, _ => .inr rfl
+
+theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
+  dsimp [bodd, (· &&& ·), AndOp.and, land]
+  unfold bitwise
+  by_cases n0 : n = 0
+  · simp [n0]
+  · simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
+      show 1 / 2 = 0 by decide]
+    cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
+
+theorem bodd_add_div2 (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
+  rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
+
+theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
+  (bit_val _ _).trans (bodd_add_div2 _)
+
+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.succ_add]
+
+/-- 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 := bit_decomp n ▸ h _ _
+
+theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n :=
+  div_lt_self (n.zero_lt_of_ne_zero h) (by decide)
+
+/-- 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. -/
+@[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 by rw [n0]; exact z
+  else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)
+  decreasing_by exact binaryRec_decreasing 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 by
+      have : bit b n = 0 := by
+        rw [bit_eq_zero_iff]
+        cases n <;> cases b <;> simp at h <;> simp [h]
+      exact 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 by
+      rw [h', h h']
+      exact z₁
+    else f b n h' ih
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index a643631db0..0ae5f53b12 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -780,11 +780,6 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
 theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
   rw [add_mod_mod, mod_add_mod]
 
-theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by simp) with
-  | 0, _ => .inl rfl
-  | 1, _ => .inr rfl
-
 @[simp]
 theorem mod_two_ne_one (n : Nat) : ¬n % 2 = 1 ↔ n % 2 = 0 := by
   cases mod_two_eq_zero_or_one n with | _ h => simp [h]
@@ -1041,11 +1036,6 @@ theorem bitwise_zero : bitwise f 0 0 = 0 := by
 
 /-! ### bodd -/
 
-theorem bit_val (b n) : bit b n = cond b 1 0 + 2 * n := by
-  cases b <;> rw [Nat.add_comm, Nat.mul_comm]
-  · exact congrArg (· + n) n.zero_add.symm
-  · exact congrArg (· + n + 1) n.zero_add.symm
-
 @[simp]
 theorem bodd_zero : bodd 0 = false :=
   rfl
@@ -1056,15 +1046,6 @@ theorem bodd_one : bodd 1 = true :=
 theorem bodd_two : bodd 2 = false :=
   rfl
 
-theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
-  dsimp [bodd, (· &&& ·), AndOp.and, land]
-  unfold bitwise
-  by_cases n0 : n = 0
-  · simp [n0]
-  · simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
-      show 1 / 2 = 0 by decide]
-    cases mod_two_eq_zero_or_one n with | _ h => simp [h]
-
 theorem bodd_eq_mod_two_bne_zero (n : Nat) : bodd n = (n % 2 != 0) := by
   rw [mod_two_of_bodd]
   cases bodd n with | false | true => rfl
@@ -1094,8 +1075,6 @@ theorem bodd_bit (b n) : bodd (bit b n) = b := by
 
 /-! ### div2 -/
 
-theorem div2_val (n) : div2 n = n / 2 := rfl
-
 @[simp]
 theorem div2_zero : div2 0 = 0 :=
   rfl
@@ -1108,54 +1087,20 @@ theorem div2_two : div2 2 = 1 :=
 
 theorem div2_eq_div_two (n : Nat) : div2 n = n / 2 := rfl
 
-theorem bodd_add_div2 (n : Nat) : cond (bodd n) 1 0 + 2 * div2 n = n := by
-  rw [← mod_two_of_bodd, div2_eq_div_two, Nat.mod_add_div]
-
 @[simp]
 theorem div2_succ (n : Nat) : 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_left_cancel (n := cond (bodd (succ n)) 1 0)
+  apply Nat.add_right_cancel (m := cond (bodd (succ n)) 1 0)
   rw (config := {occs := .pos [1]}) [bodd_add_div2, bodd_succ, ← bodd_add_div2 n]
   cases bodd n <;> simp [succ_eq_add_one, Nat.add_comm 1, Nat.mul_add]
 
 theorem div2_bit (b n) : div2 (bit b n) = n := by
-  rw [bit_val, div2_val, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
+  rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
   · cases b <;> decide
   · decide
 
-theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
-  (bit_val _ _).trans (bodd_add_div2 _)
-
-theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
-  constructor
-  · cases b <;> simp [Nat.bit, Nat.add_eq_zero]
-  · simp (config := {contextual := true})
-
 /-! ### binary rec/cases -/
 
-/-- 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 := bit_decomp n ▸ h _ _
-
-theorem 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)
-    (Nat.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 u`, if instances can be
-  constructed for natural numbers of the form `bit b n`,
-  they can be constructed for all natural numbers. -/
-@[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 by rw [n0]; exact z
-  else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)
-  decreasing_by exact binaryRec_decreasing n0
-
 @[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 := by
@@ -1188,26 +1133,3 @@ theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n 
   intro _ _
   rw [bodd_bit, div2_bit]
   intro; rfl
-
-/-- 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 by
-      have : bit b n = 0 := by
-        rw [Decidable.not_imp, Bool.not_eq_true] at h
-        rwa [bit_eq_zero_iff]
-      exact 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 by
-      rw [h', h h']
-      exact z₁
-    else f b n h' ih
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 8fa22d100f..ad5b6ad795 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -814,5 +814,7 @@ theorem Bool.eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> sim
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩
 
 @[simp] theorem Bool.beq_true (b : Bool) : (b == true) = b := by cases b <;> rfl
+
 @[simp] theorem Bool.beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
+
 theorem Bool.not_beq_not (a b : Bool) : (!a == !b) = (a == b) := by cases a <;> cases b <;> rfl

From ff6786b8ac8fa50eb1fea19466c5061e44828677 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 15 Nov 2023 19:41:14 +0800
Subject: [PATCH 08/26] fix

---
 Std/Data/Nat/Lemmas.lean | 8 ++++----
 Std/Logic.lean           | 6 ------
 2 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index f13ec6daeb..443a87e880 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Std.Logic
-import Std.Tactic.Alias
 import Std.Tactic.Basic
 import Std.Tactic.RCases
+import Std.Data.Bool
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.Nat.Basic
 import Std.Data.Ord
@@ -1255,10 +1255,10 @@ theorem bodd_succ (n : Nat) : bodd (succ n) = not (bodd n) := by
   cases mod_two_eq_zero_or_one n with | _ h => simp [h]
 
 @[simp]
-theorem bodd_add (m n : Nat) : bodd (m + n) = (bodd m != bodd n) := by
+theorem bodd_add (m n : Nat) : bodd (m + n) = ((bodd m).xor (bodd n)) := by
   induction n with
-  | zero => simp [bne]
-  | succ n ih => simp [add_succ, ih, bne, Bool.not_beq_not]
+  | zero => simp
+  | succ n ih => simp [add_succ, ih, Bool.xor_not]
 
 @[simp]
 theorem bodd_mul (m n : Nat) : bodd (m * n) = (bodd m && bodd n) := by
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 12869ea168..36855da23f 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -841,9 +841,3 @@ theorem Bool.eq_false_iff {b : Bool} : b = false ↔ b ≠ true :=
 theorem Bool.eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩
-
-@[simp] theorem Bool.beq_true (b : Bool) : (b == true) = b := by cases b <;> rfl
-
-@[simp] theorem Bool.beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
-
-theorem Bool.not_beq_not (a b : Bool) : (!a == !b) = (a == b) := by cases a <;> cases b <;> rfl

From cff0bf7e7a32db8585700245cba719a80ee18101 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Fri, 15 Dec 2023 17:45:09 +0800
Subject: [PATCH 09/26] fix merge

---
 Std/Data/Nat/Basic.lean  | 25 +++++++------------------
 Std/Data/Nat/Lemmas.lean | 11 +++++------
 2 files changed, 12 insertions(+), 24 deletions(-)

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 9ecbe56a12..b5d22cfc0b 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -127,15 +127,6 @@ where
       guess
 termination_by iter guess => guess
 
-/-!
-### testBit
-We define an operation for testing individual bits in the binary representation
-of a number.
--/
-
-/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
-def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
-
 /-- `bodd n` returns `true` if `n` is odd-/
 def bodd (n : Nat) : Bool :=
   (1 &&& n) != 0
@@ -149,6 +140,12 @@ def div2 (n : Nat) : Nat :=
 def bit (b : Bool) (n : Nat) : Nat :=
   cond b (n + n + 1) (n + n)
 
+/-!
+### testBit
+We define an operation for testing individual bits in the binary representation
+of a number.
+-/
+
 /-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
 def testBit (m n : Nat) : Bool :=
   bodd (m >>> n)
@@ -161,7 +158,7 @@ theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
 theorem div2_val (n) : div2 n = n / 2 := rfl
 
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by simp) with
+  match n % 2, @Nat.mod_lt n 2 (by decide) with
   | 0, _ => .inl rfl
   | 1, _ => .inr rfl
 
@@ -224,11 +221,3 @@ def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
       rw [h', h h']
       exact z₁
     else f b n h' ih
-/-!
-### testBit
-We define an operation for testing individual bits in the binary representation
-of a number.
--/
-
-/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
-def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 050f4e6c10..58f1b5f886 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -965,11 +965,6 @@ theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
   | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
   | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
 
-theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by decide) with
-  | 0, _ => .inl rfl
-  | 1, _ => .inr rfl
-
 theorem le_of_mod_lt {a b : Nat} (h : a % b < a) : b ≤ a :=
   Nat.not_lt.1 fun hf => (ne_of_lt h).elim (Nat.mod_eq_of_lt hf)
 
@@ -1047,6 +1042,10 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
 theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
   rw [add_mod_mod, mod_add_mod]
 
+@[simp]
+theorem one_mod (n : Nat) : 1 % (n + 2) = 1 :=
+  Nat.mod_eq_of_lt (succ_lt_succ n.succ_pos)
+
 @[simp]
 theorem mod_two_ne_one (n : Nat) : ¬n % 2 = 1 ↔ n % 2 = 0 := by
   cases mod_two_eq_zero_or_one n with | _ h => simp [h]
@@ -1310,7 +1309,7 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm
   | k + 1 => by
     rw [shiftRight_add, shiftRight_eq_div_pow m k]
-    simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ]
+    simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ, shiftRight_succ]
 
 theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
   match x with

From 615cfc9362ef691c830b1279019c5774d0dd8614 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 03:22:31 +0800
Subject: [PATCH 10/26] fix merge & golf

---
 Std/Data/Nat/Basic.lean  | 11 ++++---
 Std/Data/Nat/Lemmas.lean | 46 +++++++++------------------
 Std/Logic.lean           | 68 +++++++++++++++++++++++++++++++++++++++-
 3 files changed, 88 insertions(+), 37 deletions(-)

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index b5d22cfc0b..7051127ed0 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -165,9 +165,10 @@ theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
 theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
   dsimp [bodd, (· &&& ·), AndOp.and, land]
   unfold bitwise
-  by_cases n0 : n = 0
-  · simp [n0]
-  · simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
+  match Nat.decEq n 0 with
+  | isTrue n0 => subst n0; decide
+  | isFalse n0 =>
+    simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
       show 1 / 2 = 0 by decide]
     cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
 
@@ -195,8 +196,8 @@ theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n :=
   they can be constructed for all natural numbers. -/
 @[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 by rw [n0]; exact z
-  else by rw [← n.bit_decomp]; exact f n.bodd n.div2 (binaryRec z f n.div2)
+  if n0 : n = 0 then congrArg C n0 ▸ z -- `congrArg C _` is `rfl` in non-dependent case
+  else congrArg C n.bit_decomp ▸ f n.bodd n.div2 (binaryRec z f n.div2)
   decreasing_by exact binaryRec_decreasing n0
 
 /-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 58f1b5f886..39916cef24 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1332,13 +1332,6 @@ theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   · exact (m % 0).div_zero
   · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)
 
-/-! ### shiftLeft -/
-
-theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
-
-theorem shiftLeft_succ (m n) : m <<< (n + 1) = 2 * (m <<< n) := by
-  simp only [shiftLeft_eq, Nat.pow_add, Nat.pow_one, ← Nat.mul_assoc, Nat.mul_comm]
-
 /-! ### bitwise -/
 
 @[simp]
@@ -1373,7 +1366,7 @@ theorem bodd_eq_mod_two_bne_zero (n : Nat) : bodd n = (n % 2 != 0) := by
 @[simp]
 theorem bodd_succ (n : Nat) : bodd (succ n) = not (bodd n) := by
   simp only [bodd_eq_mod_two_bne_zero, succ_eq_add_one, succ_mod_two_eq_one_sub_mod_two]
-  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+  cases mod_two_eq_zero_or_one n with | _ h => simp (config := {decide := true}) [h]
 
 @[simp]
 theorem bodd_add (m n : Nat) : bodd (m + n) = ((bodd m).xor (bodd n)) := by
@@ -1423,33 +1416,24 @@ theorem div2_bit (b n) : div2 (bit b n) = n := by
 
 @[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 := by
-  rw [binaryRec]
+    binaryRec z f 0 = z :=
   rfl
 
+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 = bit_decomp n ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
+  rw [binaryRec, dif_neg h, Eq.rec_eq_cast, Eq.rec_eq_cast]
+
 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
-  rw [binaryRec]
-  by_cases h : bit b n = 0
-  -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0`
-  case pos h' =>
-    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h
-    simp only [or_false] at h'
-    exact h'.symm
-  case neg h' =>
-    simp only [dif_neg h]
-    generalize bit_decomp (bit b n) = e
-    revert e
+  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
+    exact h.symm
+  case neg =>
+    rw [binaryRec_of_ne_zero _ _ h']
+    generalize bit_decomp (bit b n) = e; revert e
     rw [bodd_bit, div2_bit]
     intros; rfl
-
-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 = bit_decomp n ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
-  rw [binaryRec, dif_neg h]
-  generalize bit_decomp n = e; revert e
-  apply bitCasesOn n
-  intro _ _
-  rw [bodd_bit, div2_bit]
-  intro; rfl
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 728476fc23..337cdaf759 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -721,6 +721,8 @@ end Classical
 
 /-! ## equality -/
 
+section Equality
+
 theorem heq_iff_eq : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
@@ -729,9 +731,73 @@ theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
 @[simp] theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
     (@Eq.rec α a (fun α _ => β) y a' h) = y := by cases h; rfl
 
-theorem congrArg₂ (f : α → β → γ) {x x' : α} {y y' : β}
+alias congr_fun := congrFun
+alias congr_arg := congrArg
+
+theorem congr_arg₂ (f : α → β → γ) {x x' : α} {y y' : β}
     (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl
 
+@[simp] theorem eq_mp_eq_cast (h : α = β) : Eq.mp h = cast h :=
+  rfl
+
+@[simp] theorem eq_mpr_eq_cast (h : α = β) : Eq.mpr h = cast h.symm :=
+  rfl
+
+@[simp] theorem cast_cast : ∀ (ha : α = β) (hb : β = γ) (a : α),
+    cast hb (cast ha a) = cast (ha.trans hb) a
+  | rfl, rfl, _ => rfl
+
+theorem heq_of_cast_eq : ∀ (e : α = β) (_ : cast e a = a'), HEq a a'
+  | rfl, h => Eq.recOn h (HEq.refl _)
+
+theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
+  ⟨heq_of_cast_eq _, fun h ↦ by cases h; rfl⟩
+
+section EqRec
+variable {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
+  (x : motive a (rfl : a = a)) {a' : α} (e : a = a')
+
+theorem Eq.rec_eq_cast : @Eq.rec α a motive x a' e = cast (e ▸ rfl) x := by
+  subst e; rfl
+
+--Porting note: new theorem. More general version of `eqRec_heq`
+theorem eqRec_heq' : HEq (@Eq.rec α a motive x a' e) x := by
+  subst e; rfl
+
+@[simp]
+theorem rec_heq_iff_heq {β : Sort _} (y : β) : HEq (@Eq.rec α a motive x a' e) y ↔ HEq x y := by
+  subst e; rfl
+
+@[simp]
+theorem heq_rec_iff_heq {β : Sort _} (y : β) : HEq y (@Eq.rec α a motive x a' e) ↔ HEq y x := by
+  subst e; rfl
+
+end EqRec
+
+protected theorem Eq.congr (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : x₁ = x₂ ↔ y₁ = y₂ := by
+  subst h₁; subst h₂; rfl
+
+theorem Eq.congr_left {x y z : α} (h : x = y) : x = z ↔ y = z := by rw [h]
+
+theorem Eq.congr_right {x y z : α} (h : x = y) : z = x ↔ z = y := by rw [h]
+
+variable {β : α → Sort _} {γ : ∀ a, β a → Sort _} {δ : ∀ a b, γ a b → Sort _}
+
+theorem congr_fun₂ {f g : ∀ a b, γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b :=
+  congr_fun (congr_fun h _) _
+
+theorem congr_fun₃ {f g : ∀ a b c, δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
+    f a b c = g a b c :=
+  congr_fun₂ (congr_fun h _) _ _
+
+theorem funext₂ {f g : ∀ a b, γ a b} (h : ∀ a b, f a b = g a b) : f = g :=
+  funext fun _ ↦ funext <| h _
+
+theorem funext₃ {f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
+  funext fun _ ↦ funext₂ <| h _
+
+end Equality
+
 /-! ## membership -/
 
 section Mem

From 6982af054313b76d86e6603dc76f3041c2268dce Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 04:18:02 +0800
Subject: [PATCH 11/26] feat: more `Bool` lemmas

---
 Std/Data/Bool.lean | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 Std/Logic.lean     | 15 ++-------------
 2 files changed, 48 insertions(+), 13 deletions(-)

diff --git a/Std/Data/Bool.lean b/Std/Data/Bool.lean
index 94264680ee..1df4ac7128 100644
--- a/Std/Data/Bool.lean
+++ b/Std/Data/Bool.lean
@@ -38,6 +38,52 @@ instance (x y : Bool) : Decidable (x < y) := inferInstanceAs (Decidable (!x && y
 instance : Max Bool := ⟨or⟩
 instance : Min Bool := ⟨and⟩
 
+theorem false_ne_true : false ≠ true := Bool.noConfusion
+
+theorem eq_false_or_eq_true : (b : Bool) → b = true ∨ b = false := by decide
+
+theorem eq_false_iff : {b : Bool} → b = false ↔ b ≠ true := by decide
+
+theorem eq_true_iff : {b : Bool} → b = true ↔ b ≠ false := by decide
+
+theorem eq_iff_iff : {a b : Bool} → a = b ↔ (a ↔ b) := by decide
+
+/-! ### beq -/
+
+@[simp] theorem beq_false_left : ∀ (x : Bool), (false == x) = !x := by decide
+
+@[simp] theorem beq_false_right : ∀ (x : Bool), (x == false) = !x := by decide
+
+@[simp] theorem beq_true_left : ∀ (x : Bool), (true == x) = x := by decide
+
+@[simp] theorem beq_true_right : ∀ (x : Bool), (x == true) = x := by decide
+
+theorem beq_not_left : ∀ (x y : Bool), (!x == y) = !(x == y) := by decide
+
+theorem beq_not_right : ∀ (x y : Bool), (x == !y) = !(x == y) := by decide
+
+@[simp] theorem beq_not_not : ∀ (x y : Bool), (!x == !y) = (x == y) := by decide
+
+theorem beq_eq_not_xor : ∀ (x y : Bool), (x == y) = !xor x y := by decide
+
+/-! ### bne -/
+
+@[simp] theorem bne_false_left : ∀ (x : Bool), (false != x) = x := by decide
+
+@[simp] theorem bne_false_right : ∀ (x : Bool), (x != false) = x := by decide
+
+@[simp] theorem bne_true_left : ∀ (x : Bool), (true != x) = !x := by decide
+
+@[simp] theorem bne_true_right : ∀ (x : Bool), (x != true) = !x := by decide
+
+theorem bne_not_left : ∀ (x y : Bool), (!x != y) = (x == y) := by decide
+
+theorem bne_not_right : ∀ (x y : Bool), (x != !y) = (x == y) := by decide
+
+@[simp] theorem bne_not_not : ∀ (x y : Bool), (!x != !y) = (x != y) := by decide
+
+theorem bne_eq_xor : ∀ (x y : Bool), (x != y) = xor x y := by decide
+
 /-! ### and -/
 
 @[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 728476fc23..22b33d0c20 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -662,15 +662,13 @@ This is the same as `decidable_of_iff` but the iff is flipped. -/
   decidable_of_decidable_of_iff h.symm
 
 instance Decidable.predToBool (p : α → Prop) [DecidablePred p] :
-    CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩
-
-theorem Bool.false_ne_true : false ≠ true := fun.
+  CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩
 
 /-- Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`.
 (This is sometimes taken as an alternate definition of decidability.) -/
 def decidable_of_bool : ∀ (b : Bool), (b ↔ a) → Decidable a
   | true, h => isTrue (h.1 rfl)
-  | false, h => isFalse (mt h.2 Bool.false_ne_true)
+  | false, h => isFalse (mt h.2 Bool.noConfusion)
 
 protected theorem Decidable.not_forall {p : α → Prop} [Decidable (∃ x, ¬p x)]
     [∀ x, Decidable (p x)] : (¬∀ x, p x) ↔ ∃ x, ¬p x :=
@@ -849,13 +847,4 @@ example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
 
 theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial
 
-theorem Bool.eq_false_or_eq_true : (b : Bool) → b = true ∨ b = false
-  | true => .inl rfl
-  | false => .inr rfl
-
-theorem Bool.eq_false_iff {b : Bool} : b = false ↔ b ≠ true :=
-  ⟨ne_true_of_eq_false, eq_false_of_ne_true⟩
-
-theorem Bool.eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
-
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩

From 2aacb408391b7232383994b7d49d068a9db906b0 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 04:19:49 +0800
Subject: [PATCH 12/26] style

---
 Std/Logic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Std/Logic.lean b/Std/Logic.lean
index 22b33d0c20..41725636b6 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -662,7 +662,7 @@ This is the same as `decidable_of_iff` but the iff is flipped. -/
   decidable_of_decidable_of_iff h.symm
 
 instance Decidable.predToBool (p : α → Prop) [DecidablePred p] :
-  CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩
+    CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩
 
 /-- Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`.
 (This is sometimes taken as an alternate definition of decidability.) -/

From 3fed6e4fd9bd5b67a5f2e7335f531facb9d4f481 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 05:35:43 +0800
Subject: [PATCH 13/26] fix

---
 Std/Data/Nat/Basic.lean   |   2 +-
 Std/Data/Nat/Bitwise.lean | 137 ++++++++++++++------------------------
 Std/Data/Nat/Lemmas.lean  |  10 ++-
 Std/Logic.lean            |   3 +
 4 files changed, 61 insertions(+), 91 deletions(-)

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 7051127ed0..2e7c4fe496 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -129,7 +129,7 @@ termination_by iter guess => guess
 
 /-- `bodd n` returns `true` if `n` is odd-/
 def bodd (n : Nat) : Bool :=
-  (1 &&& n) != 0
+  (1 &&& n) != 0 -- `1 &&& n` is faster than `n &&& 1` for big `n`. This may change in the future.
 
 /-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
 def div2 (n : Nat) : Nat :=
diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index 9a9fb8263b..36f024ca81 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -19,6 +19,9 @@ namespace Nat
 @[local simp]
 private theorem one_div_two : 1/2 = 0 := by trivial
 
+private theorem decide_mod_two_eq_one {x : Nat} : decide (x % 2 = 1) = (x % 2 != 0) := by
+  cases mod_two_eq_zero_or_one x with | _ h => simp (config := {decide := true}) [h]
+
 private theorem two_pow_succ_sub_one_div : (2 ^ (n+1) - 1) / 2 = 2^n - 1 := by
   apply fun x => (Nat.sub_eq_of_eq_add x).symm
   apply Eq.trans _
@@ -34,21 +37,6 @@ private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 :=
 
 /-! ### Preliminaries -/
 
-/--
-An induction principal that works on divison by two.
--/
-noncomputable def div2Induction {motive : Nat → Sort u}
-    (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
-  induction n using Nat.strongInductionOn with
-  | ind n hyp =>
-    apply ind
-    intro n_pos
-    if n_eq : n = 0 then
-      simp [n_eq] at n_pos
-    else
-      apply hyp
-      exact Nat.div_lt_self n_pos (Nat.le_refl _)
-
 @[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
@@ -56,7 +44,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
   unfold bitwise
   simp
 
-@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
+@[simp] theorem one_and_is_mod (x : Nat) : 1 &&& x = x % 2 := by
   if xz : x = 0 then
     simp [xz, zero_and]
   else
@@ -70,65 +58,47 @@ noncomputable def div2Induction {motive : Nat → Sort u}
 /-! ### testBit -/
 
 @[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
-  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
+  simp only [testBit, zero_shiftRight, bodd, and_zero, bne_self_eq_false]
 
-theorem testBit_zero_is_mod2 (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
-  cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
+theorem testBit_zero_is_bodd (x : Nat) : testBit x 0 = bodd x :=
+  rfl
 
-theorem testBit_succ_div2 (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+theorem testBit_succ_div_two (x i : Nat) : testBit x (i + 1) = testBit (x / 2) i := by
   unfold testBit
-  simp [shiftRight_succ_inside]
+  simp [shiftRight_succ_inside, div2]
 
 theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
     unfold testBit
-    cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]
+    cases mod_two_eq_zero_or_one x with | _ xz => simp [bodd, xz]
   | succ i hyp =>
-    simp [testBit_succ_div2, hyp,
+    simp [testBit_succ_div_two, hyp,
           Nat.div_div_eq_div_mul, Nat.pow_succ, Nat.mul_comm 2]
 
 theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
-  induction x using div2Induction with
-  | ind x hyp =>
-    have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
-    match mod_two_eq_zero_or_one x with
-    | Or.inl mod2_eq =>
-      rw [←div_add_mod x 2] at xnz
-      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
-      have ⟨d, dif⟩   := hyp x_pos xnz
-      apply Exists.intro (d+1)
-      simp [testBit_succ_div2, dif]
-    | Or.inr mod2_eq =>
-      apply Exists.intro 0
-      simp [testBit_zero_is_mod2, mod2_eq]
+  induction x using binaryRecFromOne with
+  | z₀ => exact absurd rfl xnz
+  | z₁ => exact ⟨0, rfl⟩
+  | f b n n0 hyp =>
+    obtain ⟨i, h⟩ := hyp n0
+    refine ⟨i + 1, ?_⟩
+    rwa [testBit_succ_div_two, bit_div_two]
 
 theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
-  induction y using Nat.div2Induction generalizing x with
-  | ind y hyp =>
-    cases Nat.eq_zero_or_pos y with
-    | inl yz =>
-      simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
-      simp only [yz] at p
-      have ⟨i,ip⟩  := ne_zero_implies_bit_true p
-      apply Exists.intro i
-      simp [ip]
-    | inr ypos =>
-      if lsb_diff : x % 2 = y % 2 then
-        rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
-        simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
-          Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
-        have ⟨i, ieq⟩  := hyp ypos p
-        apply Exists.intro (i+1)
-        simp [testBit_succ_div2]
-        exact ieq
-      else
-        apply Exists.intro 0
-        simp only [testBit_zero_is_mod2]
-        revert lsb_diff
-        cases mod_two_eq_zero_or_one x with | _ p =>
-          cases mod_two_eq_zero_or_one y with | _ q =>
-            simp [p,q]
+  induction y using binaryRec' generalizing x with
+  | z =>
+    simp only [zero_testBit, ← Bool.eq_true_iff]
+    exact ne_zero_implies_bit_true p
+  | f yb y h hyp =>
+    rw [← x.bit_decomp] at *
+    by_cases hb : bodd x = yb
+    · subst hb
+      obtain ⟨i, h⟩ := hyp (ne_of_apply_ne _ p)
+      refine ⟨i + 1, ?_⟩
+      rwa [testBit_succ_div_two, bit_div_two, testBit_succ_div_two, bit_div_two]
+    · refine ⟨0, ?_⟩
+      rwa [testBit_zero_is_bodd, testBit_zero_is_bodd, bodd_bit, bodd_bit]
 
 /--
 `eq_of_testBit_eq` allows proving two natural numbers are equal
@@ -142,27 +112,18 @@ theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) :
     have p := pred i
     contradiction
 
-theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
-  induction x using div2Induction generalizing n with
-  | ind x hyp =>
-    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.pow_two_pos n) p
-    have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
+theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : 2^n ≤ x) : ∃ i, n ≤ i ∧ testBit x i := by
+  induction x using binaryRec generalizing n with
+  | z => exact absurd p (Nat.not_le_of_lt n.pow_two_pos)
+  | f xb x hyp =>
     match n with
-    | zero =>
-      let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
-      exact Exists.intro j (And.intro (Nat.zero_le _) jp)
-    | succ n =>
-      have x_ge_n : x / 2 ≥ 2 ^ n := by
-          simp [le_div_iff_mul_le, ← Nat.pow_succ']
-          exact p
-      have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
-      apply Exists.intro (j+1)
-      apply And.intro
-      case left =>
-        exact (Nat.succ_le_succ jp.left)
-      case right =>
-        simp [testBit_succ_div2 _ j]
-        exact jp.right
+    | 0 =>
+      simp only [zero_le, true_and]
+      exact ne_zero_implies_bit_true (ne_of_gt (Nat.lt_of_succ_le p))
+    | n+1 =>
+      obtain ⟨i, h⟩ := hyp (mul_two_le_bit.mp p)
+      refine ⟨i + 1, ?_⟩
+      rwa [Nat.add_le_add_iff_right, testBit_succ_div_two, bit_div_two]
 
 theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
   simp only [testBit_to_div_mod] at p
@@ -262,14 +223,14 @@ private theorem testBit_one_zero : testBit 1 0 = true := by trivial
 @[simp] theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n) := by
   induction i generalizing n with
   | zero =>
-    simp [testBit_zero_is_mod2]
+    simp [testBit_zero_is_bodd]
     match n with
     | 0 =>
       simp
     | n+1 =>
-      simp [Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
+      simp [bodd, Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
   | succ i hyp =>
-    simp [testBit_succ_div2]
+    simp [testBit_succ_div_two]
     match n with
     | 0 =>
       simp [pow_zero]
@@ -304,12 +265,12 @@ theorem testBit_bitwise
       simp only [x_zero, y_zero, ←Nat.two_mul]
       cases i with
       | zero =>
-        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, testBit_zero_is_mod2, Nat.mul_add_mod, mod_eq_of_lt]
+        cases p : f (x % 2 != 0) (y % 2 != 0) <;>
+          simp [p, testBit_zero_is_bodd, bodd, decide_mod_two_eq_one, Nat.mul_add_mod]
       | succ i =>
         have hyp_i := hyp i (Nat.le_refl (i+1))
-        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, testBit_succ_div2, one_div_two, hyp_i, Nat.mul_add_div]
+        cases p : f (x % 2 != 0) (y % 2 != 0) <;>
+          simp [p, testBit_succ_div_two, decide_mod_two_eq_one, hyp_i, Nat.mul_add_div]
 
 /-! ### bitwise -/
 
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 39916cef24..35eb33f0e1 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1407,11 +1407,17 @@ theorem div2_succ (n : Nat) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div
   rw (config := {occs := .pos [1]}) [bodd_add_div2, bodd_succ, ← bodd_add_div2 n]
   cases bodd n <;> simp [succ_eq_add_one, Nat.add_comm 1, Nat.mul_add]
 
-theorem 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]
+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
 
+theorem div2_bit (b n) : div2 (bit b n) = n :=
+  bit_div_two b n
+
+theorem mul_two_le_bit {x b n} : x * 2 ≤ bit b n ↔ x ≤ n := by
+  rw [← le_div_iff_mul_le Nat.two_pos, bit_div_two]
+
 /-! ### binary rec/cases -/
 
 @[simp]
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 1bc991911d..67a28cd9d9 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -732,6 +732,9 @@ theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
 alias congr_fun := congrFun
 alias congr_arg := congrArg
 
+theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} (h : f x ≠ f y) : x ≠ y :=
+  fun w : x = y ↦ h (congr_arg f w)
+
 theorem congr_arg₂ (f : α → β → γ) {x x' : α} {y y' : β}
     (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl
 

From 760793902f52e01991a2f85fdb1af7a92bc9cace Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 05:40:22 +0800
Subject: [PATCH 14/26] fix

---
 Std/Data/Bool.lean | 2 --
 Std/Logic.lean     | 2 ++
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Std/Data/Bool.lean b/Std/Data/Bool.lean
index 1df4ac7128..55ab408cf6 100644
--- a/Std/Data/Bool.lean
+++ b/Std/Data/Bool.lean
@@ -46,8 +46,6 @@ theorem eq_false_iff : {b : Bool} → b = false ↔ b ≠ true := by decide
 
 theorem eq_true_iff : {b : Bool} → b = true ↔ b ≠ false := by decide
 
-theorem eq_iff_iff : {a b : Bool} → a = b ↔ (a ↔ b) := by decide
-
 /-! ### beq -/
 
 @[simp] theorem beq_false_left : ∀ (x : Bool), (false == x) = !x := by decide
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 41725636b6..82716bb224 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -847,4 +847,6 @@ example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
 
 theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial
 
+theorem Bool.eq_iff_iff : {a b : Bool} → a = b ↔ (a ↔ b) := by decide
+
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩

From abd94e25115c5a6655fe8dcf483886cd78e4dc93 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 05:43:08 +0800
Subject: [PATCH 15/26] fix

---
 Std/Logic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Std/Logic.lean b/Std/Logic.lean
index 82716bb224..7f9fd18a64 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -847,6 +847,6 @@ example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
 
 theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial
 
-theorem Bool.eq_iff_iff : {a b : Bool} → a = b ↔ (a ↔ b) := by decide
+theorem Bool.eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩

From daf763410a7fc825080185f739c7ec861dafbe2a Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 05:52:09 +0800
Subject: [PATCH 16/26] fix

---
 Std/Data/Bool.lean | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/Std/Data/Bool.lean b/Std/Data/Bool.lean
index 55ab408cf6..fb5a7f5a56 100644
--- a/Std/Data/Bool.lean
+++ b/Std/Data/Bool.lean
@@ -56,29 +56,29 @@ theorem eq_true_iff : {b : Bool} → b = true ↔ b ≠ false := by decide
 
 @[simp] theorem beq_true_right : ∀ (x : Bool), (x == true) = x := by decide
 
-theorem beq_not_left : ∀ (x y : Bool), (!x == y) = !(x == y) := by decide
+theorem beq_not_left : ∀ (x y : Bool), ((!x) == y) = !(x == y) := by decide
 
-theorem beq_not_right : ∀ (x y : Bool), (x == !y) = !(x == y) := by decide
+theorem beq_not_right : ∀ (x y : Bool), (x == (!y)) = !(x == y) := by decide
 
-@[simp] theorem beq_not_not : ∀ (x y : Bool), (!x == !y) = (x == y) := by decide
+@[simp] theorem beq_not_not : ∀ (x y : Bool), ((!x) == (!y)) = (x == y) := by decide
 
 theorem beq_eq_not_xor : ∀ (x y : Bool), (x == y) = !xor x y := by decide
 
 /-! ### bne -/
 
-@[simp] theorem bne_false_left : ∀ (x : Bool), (false != x) = x := by decide
+theorem bne_false_left : ∀ (x : Bool), (false != x) = x := by decide
 
-@[simp] theorem bne_false_right : ∀ (x : Bool), (x != false) = x := by decide
+theorem bne_false_right : ∀ (x : Bool), (x != false) = x := by decide
 
-@[simp] theorem bne_true_left : ∀ (x : Bool), (true != x) = !x := by decide
+theorem bne_true_left : ∀ (x : Bool), (true != x) = !x := by decide
 
-@[simp] theorem bne_true_right : ∀ (x : Bool), (x != true) = !x := by decide
+theorem bne_true_right : ∀ (x : Bool), (x != true) = !x := by decide
 
-theorem bne_not_left : ∀ (x y : Bool), (!x != y) = (x == y) := by decide
+theorem bne_not_left : ∀ (x y : Bool), ((!x) != y) = (x == y) := by decide
 
-theorem bne_not_right : ∀ (x y : Bool), (x != !y) = (x == y) := by decide
+theorem bne_not_right : ∀ (x y : Bool), (x != (!y)) = (x == y) := by decide
 
-@[simp] theorem bne_not_not : ∀ (x y : Bool), (!x != !y) = (x != y) := by decide
+theorem bne_not_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
 
 theorem bne_eq_xor : ∀ (x y : Bool), (x != y) = xor x y := by decide
 

From 3e9efc48ec31c05b0eaad0c2bf7420a50536af05 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 05:59:06 +0800
Subject: [PATCH 17/26] feat: more lemmas about equality

---
 Std/Logic.lean | 71 +++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 70 insertions(+), 1 deletion(-)

diff --git a/Std/Logic.lean b/Std/Logic.lean
index 728476fc23..84fb4c5c7a 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -721,6 +721,8 @@ end Classical
 
 /-! ## equality -/
 
+section Equality
+
 theorem heq_iff_eq : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
@@ -729,9 +731,76 @@ theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
 @[simp] theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
     (@Eq.rec α a (fun α _ => β) y a' h) = y := by cases h; rfl
 
-theorem congrArg₂ (f : α → β → γ) {x x' : α} {y y' : β}
+alias congr_fun := congrFun
+alias congr_arg := congrArg
+
+theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} (h : f x ≠ f y) : x ≠ y :=
+  fun w : x = y ↦ h (congr_arg f w)
+
+theorem congr_arg₂ (f : α → β → γ) {x x' : α} {y y' : β}
     (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl
 
+@[simp] theorem eq_mp_eq_cast (h : α = β) : Eq.mp h = cast h :=
+  rfl
+
+@[simp] theorem eq_mpr_eq_cast (h : α = β) : Eq.mpr h = cast h.symm :=
+  rfl
+
+@[simp] theorem cast_cast : ∀ (ha : α = β) (hb : β = γ) (a : α),
+    cast hb (cast ha a) = cast (ha.trans hb) a
+  | rfl, rfl, _ => rfl
+
+theorem heq_of_cast_eq : ∀ (e : α = β) (_ : cast e a = a'), HEq a a'
+  | rfl, h => Eq.recOn h (HEq.refl _)
+
+theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
+  ⟨heq_of_cast_eq _, fun h ↦ by cases h; rfl⟩
+
+section EqRec
+variable {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
+  (x : motive a (rfl : a = a)) {a' : α} (e : a = a')
+
+theorem Eq.rec_eq_cast : @Eq.rec α a motive x a' e = cast (e ▸ rfl) x := by
+  subst e; rfl
+
+--Porting note: new theorem. More general version of `eqRec_heq`
+theorem eqRec_heq' : HEq (@Eq.rec α a motive x a' e) x := by
+  subst e; rfl
+
+@[simp]
+theorem rec_heq_iff_heq {β : Sort _} (y : β) : HEq (@Eq.rec α a motive x a' e) y ↔ HEq x y := by
+  subst e; rfl
+
+@[simp]
+theorem heq_rec_iff_heq {β : Sort _} (y : β) : HEq y (@Eq.rec α a motive x a' e) ↔ HEq y x := by
+  subst e; rfl
+
+end EqRec
+
+protected theorem Eq.congr (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : x₁ = x₂ ↔ y₁ = y₂ := by
+  subst h₁; subst h₂; rfl
+
+theorem Eq.congr_left {x y z : α} (h : x = y) : x = z ↔ y = z := by rw [h]
+
+theorem Eq.congr_right {x y z : α} (h : x = y) : z = x ↔ z = y := by rw [h]
+
+variable {β : α → Sort _} {γ : ∀ a, β a → Sort _} {δ : ∀ a b, γ a b → Sort _}
+
+theorem congr_fun₂ {f g : ∀ a b, γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b :=
+  congr_fun (congr_fun h _) _
+
+theorem congr_fun₃ {f g : ∀ a b c, δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
+    f a b c = g a b c :=
+  congr_fun₂ (congr_fun h _) _ _
+
+theorem funext₂ {f g : ∀ a b, γ a b} (h : ∀ a b, f a b = g a b) : f = g :=
+  funext fun _ ↦ funext <| h _
+
+theorem funext₃ {f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
+  funext fun _ ↦ funext₂ <| h _
+
+end Equality
+
 /-! ## membership -/
 
 section Mem

From fbf3b8273102861e9caa2abefbd10037a481e1bd Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 06:01:29 +0800
Subject: [PATCH 18/26] =?UTF-8?q?no=20`=E2=86=A6`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Std/Logic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Std/Logic.lean b/Std/Logic.lean
index 84fb4c5c7a..f82bdf69f7 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -735,7 +735,7 @@ alias congr_fun := congrFun
 alias congr_arg := congrArg
 
 theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} (h : f x ≠ f y) : x ≠ y :=
-  fun w : x = y ↦ h (congr_arg f w)
+  fun w : x = y => h (congr_arg f w)
 
 theorem congr_arg₂ (f : α → β → γ) {x x' : α} {y y' : β}
     (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl
@@ -754,7 +754,7 @@ theorem heq_of_cast_eq : ∀ (e : α = β) (_ : cast e a = a'), HEq a a'
   | rfl, h => Eq.recOn h (HEq.refl _)
 
 theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
-  ⟨heq_of_cast_eq _, fun h ↦ by cases h; rfl⟩
+  ⟨heq_of_cast_eq _, fun h => by cases h; rfl⟩
 
 section EqRec
 variable {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
@@ -794,10 +794,10 @@ theorem congr_fun₃ {f g : ∀ a b c, δ a b c} (h : f = g) (a : α) (b : β a)
   congr_fun₂ (congr_fun h _) _ _
 
 theorem funext₂ {f g : ∀ a b, γ a b} (h : ∀ a b, f a b = g a b) : f = g :=
-  funext fun _ ↦ funext <| h _
+  funext fun _ => funext <| h _
 
 theorem funext₃ {f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
-  funext fun _ ↦ funext₂ <| h _
+  funext fun _ => funext₂ <| h _
 
 end Equality
 

From 03265b6ed01d06a8a1273b1d127e626e8c4134b9 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sat, 16 Dec 2023 06:04:41 +0800
Subject: [PATCH 19/26] lint

---
 Std/Data/Nat/Bitwise.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index 36f024ca81..da0ed2e75f 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -48,12 +48,9 @@ private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 :=
   if xz : x = 0 then
     simp [xz, zero_and]
   else
-    have andz := and_zero (x/2)
-    simp only [HAnd.hAnd, AndOp.and, land] at andz
     simp only [HAnd.hAnd, AndOp.and, land]
     unfold bitwise
-    cases mod_two_eq_zero_or_one x with | _ p =>
-      simp [xz, p, andz, one_div_two, mod_eq_of_lt]
+    cases mod_two_eq_zero_or_one x with | _ p => simp [xz, p]
 
 /-! ### testBit -/
 

From 661debc2e08d5cdf8c13199aa114886578835718 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Tue, 19 Dec 2023 07:26:58 +0800
Subject: [PATCH 20/26] fix name

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

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 2e7c4fe496..24dd5a2f68 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -172,11 +172,11 @@ theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
       show 1 / 2 = 0 by decide]
     cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
 
-theorem bodd_add_div2 (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
+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]
 
 theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
-  (bit_val _ _).trans (bodd_add_div2 _)
+  (bit_val _ _).trans (div2_add_bodd _)
 
 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.succ_add]
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 35eb33f0e1..a8a3d49e23 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1404,7 +1404,7 @@ theorem div2_eq_div_two (n : Nat) : div2 n = n / 2 := rfl
 theorem div2_succ (n : Nat) : 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]}) [bodd_add_div2, bodd_succ, ← bodd_add_div2 n]
+  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]
 
 theorem bit_div_two (b n) : bit b n / 2 = n := by

From ba2cdc585a0109b4bf5b29f65a1b1009b1398c22 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Tue, 19 Dec 2023 21:20:51 +0800
Subject: [PATCH 21/26] it was not `elab_as_elim` in mathlib but eventually I
 think it should be

---
 Std/Data/Nat/Basic.lean   | 2 +-
 Std/Data/Nat/Bitwise.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 24dd5a2f68..b9c7b46c17 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -194,7 +194,7 @@ theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n :=
   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. -/
-@[specialize]
+@[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 -- `congrArg C _` is `rfl` in non-dependent case
   else congrArg C n.bit_decomp ▸ f n.bodd n.div2 (binaryRec z f n.div2)
diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index da0ed2e75f..253a8b42c0 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -187,7 +187,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by

From f536348a268f33dc4b499027dfd20473589b4a29 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Tue, 19 Dec 2023 21:37:06 +0800
Subject: [PATCH 22/26] implicit

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

diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index a8a3d49e23..3f0793ea3a 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1047,11 +1047,11 @@ theorem one_mod (n : Nat) : 1 % (n + 2) = 1 :=
   Nat.mod_eq_of_lt (succ_lt_succ n.succ_pos)
 
 @[simp]
-theorem mod_two_ne_one (n : Nat) : ¬n % 2 = 1 ↔ n % 2 = 0 := by
+theorem mod_two_ne_one {n : Nat} : ¬n % 2 = 1 ↔ n % 2 = 0 := by
   cases mod_two_eq_zero_or_one n with | _ h => simp [h]
 
 @[simp]
-theorem mod_two_ne_zero (n : Nat) : ¬n % 2 = 0 ↔ n % 2 = 1 := by
+theorem mod_two_ne_zero {n : Nat} : ¬n % 2 = 0 ↔ n % 2 = 1 := by
   cases mod_two_eq_zero_or_one n with | _ h => simp [h]
 
 @[simp]

From bd518d9e03487488af1ae1c4e62633cbbe49557f Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Fri, 29 Dec 2023 16:34:06 +0800
Subject: [PATCH 23/26] suggestion

---
 Std/Data/Bool.lean | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/Std/Data/Bool.lean b/Std/Data/Bool.lean
index fb5a7f5a56..9513d2f516 100644
--- a/Std/Data/Bool.lean
+++ b/Std/Data/Bool.lean
@@ -48,37 +48,37 @@ theorem eq_true_iff : {b : Bool} → b = true ↔ b ≠ false := by decide
 
 /-! ### beq -/
 
-@[simp] theorem beq_false_left : ∀ (x : Bool), (false == x) = !x := by decide
+@[simp] theorem false_beq : ∀ (x : Bool), (false == x) = !x := by decide
 
-@[simp] theorem beq_false_right : ∀ (x : Bool), (x == false) = !x := by decide
+@[simp] theorem beq_false : ∀ (x : Bool), (x == false) = !x := by decide
 
-@[simp] theorem beq_true_left : ∀ (x : Bool), (true == x) = x := by decide
+@[simp] theorem true_beq : ∀ (x : Bool), (true == x) = x := by decide
 
-@[simp] theorem beq_true_right : ∀ (x : Bool), (x == true) = x := by decide
+@[simp] theorem beq_true : ∀ (x : Bool), (x == true) = x := by decide
 
-theorem beq_not_left : ∀ (x y : Bool), ((!x) == y) = !(x == y) := by decide
+theorem not_beq : ∀ (x y : Bool), ((!x) == y) = !(x == y) := by decide
 
-theorem beq_not_right : ∀ (x y : Bool), (x == (!y)) = !(x == y) := by decide
+theorem beq_not : ∀ (x y : Bool), (x == (!y)) = !(x == y) := by decide
 
-@[simp] theorem beq_not_not : ∀ (x y : Bool), ((!x) == (!y)) = (x == y) := by decide
+@[simp] theorem not_beq_not : ∀ (x y : Bool), ((!x) == (!y)) = (x == y) := by decide
 
 theorem beq_eq_not_xor : ∀ (x y : Bool), (x == y) = !xor x y := by decide
 
 /-! ### bne -/
 
-theorem bne_false_left : ∀ (x : Bool), (false != x) = x := by decide
+theorem false_bne : ∀ (x : Bool), (false != x) = x := by decide
 
-theorem bne_false_right : ∀ (x : Bool), (x != false) = x := by decide
+theorem bne_false : ∀ (x : Bool), (x != false) = x := by decide
 
-theorem bne_true_left : ∀ (x : Bool), (true != x) = !x := by decide
+theorem true_bne : ∀ (x : Bool), (true != x) = !x := by decide
 
-theorem bne_true_right : ∀ (x : Bool), (x != true) = !x := by decide
+theorem bne_true : ∀ (x : Bool), (x != true) = !x := by decide
 
-theorem bne_not_left : ∀ (x y : Bool), ((!x) != y) = (x == y) := by decide
+theorem not_bne : ∀ (x y : Bool), ((!x) != y) = (x == y) := by decide
 
-theorem bne_not_right : ∀ (x y : Bool), (x != (!y)) = (x == y) := by decide
+theorem bne_not : ∀ (x y : Bool), (x != (!y)) = (x == y) := by decide
 
-theorem bne_not_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
+theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
 
 theorem bne_eq_xor : ∀ (x y : Bool), (x != y) = xor x y := by decide
 

From 1736834ced5aac7180433bf039180f66336f9aa8 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Fri, 19 Jan 2024 15:09:30 +0800
Subject: [PATCH 24/26] fix merge

---
 Std/Logic.lean | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/Std/Logic.lean b/Std/Logic.lean
index ee3b074820..367f809b46 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -720,8 +720,6 @@ end Classical
 
 /-! ## equality -/
 
-section Equality
-
 theorem heq_iff_eq : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
@@ -730,13 +728,7 @@ theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
 @[simp] theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
     (@Eq.rec α a (fun α _ => β) y a' h) = y := by cases h; rfl
 
-alias congr_fun := congrFun
-alias congr_arg := congrArg
-
-theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} (h : f x ≠ f y) : x ≠ y :=
-  fun w : x = y => h (congr_arg f w)
-
-theorem congr_arg₂ (f : α → β → γ) {x x' : α} {y y' : β}
+theorem congrArg₂ (f : α → β → γ) {x x' : α} {y y' : β}
     (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl
 
 theorem congrFun₂ {β : α → Sort _} {γ : ∀ a, β a → Sort _}

From 86627c627aae5ecb1cd3194150d5482baab5f3e2 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 21 Jan 2024 02:05:41 +0800
Subject: [PATCH 25/26] Update Bool.lean

---
 Std/Data/Bool.lean | 38 +-------------------------------------
 1 file changed, 1 insertion(+), 37 deletions(-)

diff --git a/Std/Data/Bool.lean b/Std/Data/Bool.lean
index 5d1337bfc8..26424373cb 100644
--- a/Std/Data/Bool.lean
+++ b/Std/Data/Bool.lean
@@ -44,43 +44,7 @@ theorem eq_false_or_eq_true : (b : Bool) → b = true ∨ b = false := by decide
 
 theorem eq_false_iff : {b : Bool} → b = false ↔ b ≠ true := by decide
 
-theorem eq_true_iff : {b : Bool} → b = true ↔ b ≠ false := by decide
-
-/-! ### beq -/
-
-@[simp] theorem false_beq : ∀ (x : Bool), (false == x) = !x := by decide
-
-@[simp] theorem beq_false : ∀ (x : Bool), (x == false) = !x := by decide
-
-@[simp] theorem true_beq : ∀ (x : Bool), (true == x) = x := by decide
-
-@[simp] theorem beq_true : ∀ (x : Bool), (x == true) = x := by decide
-
-theorem not_beq : ∀ (x y : Bool), ((!x) == y) = !(x == y) := by decide
-
-theorem beq_not : ∀ (x y : Bool), (x == (!y)) = !(x == y) := by decide
-
-@[simp] theorem not_beq_not : ∀ (x y : Bool), ((!x) == (!y)) = (x == y) := by decide
-
-theorem beq_eq_not_xor : ∀ (x y : Bool), (x == y) = !xor x y := by decide
-
-/-! ### bne -/
-
-theorem false_bne : ∀ (x : Bool), (false != x) = x := by decide
-
-theorem bne_false : ∀ (x : Bool), (x != false) = x := by decide
-
-theorem true_bne : ∀ (x : Bool), (true != x) = !x := by decide
-
-theorem bne_true : ∀ (x : Bool), (x != true) = !x := by decide
-
-theorem not_bne : ∀ (x y : Bool), ((!x) != y) = (x == y) := by decide
-
-theorem bne_not : ∀ (x y : Bool), (x != (!y)) = (x == y) := by decide
-
-theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
-
-theorem bne_eq_xor : ∀ (x y : Bool), (x != y) = xor x y := by decide
+theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
 
 /-! ### and -/
 

From 67605c3ceb27d8aa2f1631ffeca91ad47869d7de Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 21 Jan 2024 02:07:47 +0800
Subject: [PATCH 26/26] fix merge

---
 Std/Data/Nat/Bitwise.lean | 2 +-
 Std/Data/Nat/Lemmas.lean  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index 253a8b42c0..927e7df137 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -85,7 +85,7 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
 theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
   induction y using binaryRec' generalizing x with
   | z =>
-    simp only [zero_testBit, ← Bool.eq_true_iff]
+    simp only [zero_testBit, Bool.ne_false_iff]
     exact ne_zero_implies_bit_true p
   | f yb y h hyp =>
     rw [← x.bit_decomp] at *
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 073435d634..60485a6538 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1470,7 +1470,7 @@ theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (b
 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 = bit_decomp n ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
-  rw [binaryRec, dif_neg h, Eq.rec_eq_cast, Eq.rec_eq_cast]
+  rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]
 
 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)) :