From 0fdb81267fcca89e810743c5a32e703b51e586d1 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 10:08:44 +0000
Subject: [PATCH 01/20] feat: testBit_mul_two_pow

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 19 +++++++++++++++++++
 src/Init/Data/Nat/Lemmas.lean         |  6 ++++++
 2 files changed, 25 insertions(+)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 2f7142482a4b..624f612cb83f 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -115,6 +115,11 @@ theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i :=
     rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
       Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]
 
+theorem testBit_mul_two_pow (x i n : Nat) : testBit (x * 2 ^ n) (i + n) = testBit x i := by
+  have h2 : 0 < 2 := by omega
+  rw [testBit_add, Nat.mul_div_cancel]
+  simp [Nat.pow_pos h2 (n := n)]
+
 theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
   simp
 
@@ -452,6 +457,11 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
       case neg =>
         apply Nat.add_lt_add <;> exact hyp1
 
+theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
+  (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
+  apply Nat.eq_of_testBit_eq
+  simp [testBit_bitwise of_false_false, testBit_div_two_pow]
+
 theorem bitwise_div_two_pow (of_false_false : f false false = false := by rfl) :
   (bitwise f x y) / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
@@ -711,6 +721,15 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
   rw [mod_two_eq_one_iff_testBit_zero, testBit_shiftLeft]
   simp
 
+theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
+    (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
+  rw [shiftLeft_eq]
+  sorry
+  simp [shiftRight_eq_div_pow, bitwise_div_two_pow of_false_false]
+
+theorem shiftLeft_or_distrib {a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i :=
+  shiftLeft_bitwise_distrib
+
 @[simp] theorem decide_shiftRight_mod_two_eq_one :
     decide (x >>> i % 2 = 1) = x.testBit i := by
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 2fd5a8d700df..d00807eb332e 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -976,6 +976,12 @@ theorem shiftLeft_succ : ∀(m n), m <<< (n + 1) = 2 * (m <<< n)
   rw [shiftLeft_succ_inside _ (k+1)]
   rw [shiftLeft_succ _ k, shiftLeft_succ_inside]
 
+theorem shiftLeft_prec_inside (m n : Nat) : (m * 2) <<< n = m <<< (n + 1) := by
+  induction n
+  case zero => omega
+  case succ n ih =>
+    simp [shiftLeft_eq, Nat.pow_add, Nat.mul_comm, Nat.mul_assoc]
+
 /-- Shiftright on successor with division moved inside. -/
 theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
 | _, 0 => rfl

From 805a88add26b8696273fdc25896efdfb11ed99e0 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 11:36:05 +0000
Subject: [PATCH 02/20] chore: start proofs

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 624f612cb83f..610d10d93f26 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -115,8 +115,12 @@ theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i :=
     rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
       Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]
 
-theorem testBit_mul_two_pow (x i n : Nat) : testBit (x * 2 ^ n) (i + n) = testBit x i := by
+theorem testBit_mul_two_pow (x i n : Nat) (h : n ≤ i) : testBit (x * 2 ^ n) i = testBit x (i - n) := by
   have h2 : 0 < 2 := by omega
+  let j := i - n
+  have hj : testBit (x * 2 ^ n) i = testBit (x * 2 ^ n) (j + n) := by simp [j]; rw [Nat.sub_add_cancel h]
+  have hj' : testBit x (i - n) = testBit x j := by simp [j]
+  rw [hj, hj']
   rw [testBit_add, Nat.mul_div_cancel]
   simp [Nat.pow_pos h2 (n := n)]
 
@@ -460,12 +464,16 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
 theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
   (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
-  simp [testBit_bitwise of_false_false, testBit_div_two_pow]
+  simp [testBit_bitwise of_false_false, testBit_mul_two_pow (by sorry)]
+
+
+  sorry
 
 theorem bitwise_div_two_pow (of_false_false : f false false = false := by rfl) :
   (bitwise f x y) / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
-  simp [testBit_bitwise of_false_false, testBit_div_two_pow]
+  simp [testBit_bitwise of_false_false]
+  simp [testBit_div_two_pow]
 
 /-! ### and -/
 

From 23f367a2dcd5cb771e38bf3a36c4ed2bb0511ae6 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 16:12:42 +0000
Subject: [PATCH 03/20] feat: proved!

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 57 +++++++++++++++++++--------
 1 file changed, 40 insertions(+), 17 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 610d10d93f26..e95c7e6281db 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -115,14 +115,39 @@ theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i :=
     rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
       Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]
 
-theorem testBit_mul_two_pow (x i n : Nat) (h : n ≤ i) : testBit (x * 2 ^ n) i = testBit x (i - n) := by
-  have h2 : 0 < 2 := by omega
-  let j := i - n
-  have hj : testBit (x * 2 ^ n) i = testBit (x * 2 ^ n) (j + n) := by simp [j]; rw [Nat.sub_add_cancel h]
-  have hj' : testBit x (i - n) = testBit x j := by simp [j]
-  rw [hj, hj']
-  rw [testBit_add, Nat.mul_div_cancel]
-  simp [Nat.pow_pos h2 (n := n)]
+theorem testBit_mul_two_pow (x i n : Nat) :
+    testBit (x * 2 ^ n) i = if n ≤ i then testBit x (i - n) else false := by
+  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero, Bool.if_false_right]
+  by_cases hni : n ≤ i
+  · simp only [hni, decide_true, Bool.true_and]
+    congr 2
+    let j := i - n
+    have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp [j]; rw [Nat.sub_add_cancel]; omega
+    have hj' : x >>> (i - n) = x >>> j :=  by simp [j]
+    rw [hj, hj', ← shiftLeft_eq, Nat.add_comm, shiftRight_add, shiftLeft_shiftRight]
+  · simp only [hni, decide_false, Bool.false_and, beq_eq_false_iff_ne, ne_eq]
+    simp at hni
+    rw [← shiftLeft_eq]
+    let k := n - i
+    have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp [k]; rw [Nat.sub_add_cancel]; omega
+    rw [hk]
+    rw [Nat.shiftLeft_add]
+    rw [Nat.shiftLeft_shiftRight]
+    rw [shiftLeft_eq]
+    have hk' : 0 < k := by omega
+    have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
+      rw [Nat.mul_comm, Nat.div_mul_cancel]
+
+      suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
+        exact ⟨_, hs.symm⟩
+
+      let j := k - 1
+      have hj : 2 ^ (k - 1) = 2 ^ j := by simp [j]
+      have hj' : 2 ^ k = 2 ^ (j + 1) := by simp [j]; rw [Nat.sub_add_cancel]; omega
+      rw [hj, hj']
+      simp [Nat.pow_add]
+      rw [Nat.mul_comm, Nat.mul_assoc]
+    omega
 
 theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
   simp
@@ -464,16 +489,16 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
 theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
   (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
-  simp [testBit_bitwise of_false_false, testBit_mul_two_pow (by sorry)]
-
-
-  sorry
+  simp only [testBit_mul_two_pow, testBit_bitwise of_false_false, Bool.if_false_right]
+  intro i
+  by_cases hn : n ≤ i
+  · simp [hn]
+  · simp [hn, of_false_false]
 
 theorem bitwise_div_two_pow (of_false_false : f false false = false := by rfl) :
   (bitwise f x y) / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
-  simp [testBit_bitwise of_false_false]
-  simp [testBit_div_two_pow]
+  simp [testBit_bitwise of_false_false, testBit_div_two_pow]
 
 /-! ### and -/
 
@@ -731,9 +756,7 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
 
 theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
     (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
-  rw [shiftLeft_eq]
-  sorry
-  simp [shiftRight_eq_div_pow, bitwise_div_two_pow of_false_false]
+  simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]
 
 theorem shiftLeft_or_distrib {a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i :=
   shiftLeft_bitwise_distrib

From 427df3f6b90a7ebb9c0e86695bd4914682044ee8 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 16:24:11 +0000
Subject: [PATCH 04/20] chore: update simp onlys and remove useless lemma

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 21 ++++++++-------------
 src/Init/Data/Nat/Lemmas.lean         |  6 ------
 2 files changed, 8 insertions(+), 19 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index e95c7e6281db..d362e2c26ed6 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -122,30 +122,25 @@ theorem testBit_mul_two_pow (x i n : Nat) :
   · simp only [hni, decide_true, Bool.true_and]
     congr 2
     let j := i - n
-    have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp [j]; rw [Nat.sub_add_cancel]; omega
-    have hj' : x >>> (i - n) = x >>> j :=  by simp [j]
+    have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp only [j]; rw [Nat.sub_add_cancel]; omega
+    have hj' : x >>> (i - n) = x >>> j :=  by simp only [j]
     rw [hj, hj', ← shiftLeft_eq, Nat.add_comm, shiftRight_add, shiftLeft_shiftRight]
   · simp only [hni, decide_false, Bool.false_and, beq_eq_false_iff_ne, ne_eq]
-    simp at hni
+    simp only [Nat.not_le] at hni
     rw [← shiftLeft_eq]
     let k := n - i
-    have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp [k]; rw [Nat.sub_add_cancel]; omega
-    rw [hk]
-    rw [Nat.shiftLeft_add]
-    rw [Nat.shiftLeft_shiftRight]
-    rw [shiftLeft_eq]
+    have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel]; omega
+    rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
     have hk' : 0 < k := by omega
     have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
       rw [Nat.mul_comm, Nat.div_mul_cancel]
-
       suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
         exact ⟨_, hs.symm⟩
-
       let j := k - 1
-      have hj : 2 ^ (k - 1) = 2 ^ j := by simp [j]
-      have hj' : 2 ^ k = 2 ^ (j + 1) := by simp [j]; rw [Nat.sub_add_cancel]; omega
+      have hj : 2 ^ (k - 1) = 2 ^ j := by simp only [j]
+      have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel]; omega
       rw [hj, hj']
-      simp [Nat.pow_add]
+      simp only [Nat.pow_add, Nat.pow_one, j, k]
       rw [Nat.mul_comm, Nat.mul_assoc]
     omega
 
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index d00807eb332e..2fd5a8d700df 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -976,12 +976,6 @@ theorem shiftLeft_succ : ∀(m n), m <<< (n + 1) = 2 * (m <<< n)
   rw [shiftLeft_succ_inside _ (k+1)]
   rw [shiftLeft_succ _ k, shiftLeft_succ_inside]
 
-theorem shiftLeft_prec_inside (m n : Nat) : (m * 2) <<< n = m <<< (n + 1) := by
-  induction n
-  case zero => omega
-  case succ n ih =>
-    simp [shiftLeft_eq, Nat.pow_add, Nat.mul_comm, Nat.mul_assoc]
-
 /-- Shiftright on successor with division moved inside. -/
 theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
 | _, 0 => rfl

From 6743930d780a1715bfe8fbe63df9c71e167a9c48 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 17:43:02 +0000
Subject: [PATCH 05/20] feat: add and and xor distrib

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index d362e2c26ed6..8321fa771b6c 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -753,9 +753,15 @@ theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false =
     (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
   simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]
 
+theorem shiftLeft_and_distrib {a b : Nat} : (a &&& b) <<< i = a <<< i &&& b <<< i :=
+  shiftLeft_bitwise_distrib
+
 theorem shiftLeft_or_distrib {a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i :=
   shiftLeft_bitwise_distrib
 
+theorem shiftLeft_xor_distrib {a b : Nat} : (a ^^^ b) <<< i = a <<< i ^^^ b <<< i :=
+  shiftLeft_bitwise_distrib
+
 @[simp] theorem decide_shiftRight_mod_two_eq_one :
     decide (x >>> i % 2 = 1) = x.testBit i := by
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]

From e7973a4538951c9a12f75419f44747eb540570de Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 17:43:43 +0000
Subject: [PATCH 06/20] chore: fix formatting in bitwise_mul_two_pow

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

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 8321fa771b6c..57d9cf0b009e 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -482,7 +482,7 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
         apply Nat.add_lt_add <;> exact hyp1
 
 theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
-  (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
+    (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
   simp only [testBit_mul_two_pow, testBit_bitwise of_false_false, Bool.if_false_right]
   intro i

From 70d4a4543e59f009550f43a3423804999ad78af8 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 17:59:58 +0000
Subject: [PATCH 07/20] chore: split proof of testBit_mul_two_pow and rtemove
 useless hypotheses

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 52 ++++++++++++++-------------
 1 file changed, 27 insertions(+), 25 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 57d9cf0b009e..af72b2797848 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -115,34 +115,36 @@ theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i :=
     rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
       Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]
 
+theorem testBit_mul_two_pow_le {x i n : Nat} (h : n ≤ i) :
+    testBit (x * 2 ^ n) i = testBit x (i - n) := by
+  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
+  let j := i - n
+  have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp only [j]; rw [Nat.sub_add_cancel]; omega
+  have hj' : x >>> (i - n) = x >>> j :=  by simp only [j]
+  rw [hj, hj', ← shiftLeft_eq, Nat.add_comm, shiftRight_add, shiftLeft_shiftRight]
+
+theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
+    testBit (x * 2 ^ n) i = false := by
+  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero, beq_eq_false_iff_ne, ne_eq, ← shiftLeft_eq]
+  let k := n - i
+  have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel]; omega
+  rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
+  have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
+    rw [Nat.mul_comm, Nat.div_mul_cancel]
+    suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
+      exact ⟨_, hs.symm⟩
+    let j := k - 1
+    have hj : 2 ^ (k - 1) = 2 ^ j := by simp only [j]
+    have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel]; omega
+    rw [hj, hj', Nat.pow_add, Nat.pow_one, Nat.mul_comm, Nat.mul_assoc]
+  omega
+
 theorem testBit_mul_two_pow (x i n : Nat) :
     testBit (x * 2 ^ n) i = if n ≤ i then testBit x (i - n) else false := by
-  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero, Bool.if_false_right]
   by_cases hni : n ≤ i
-  · simp only [hni, decide_true, Bool.true_and]
-    congr 2
-    let j := i - n
-    have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp only [j]; rw [Nat.sub_add_cancel]; omega
-    have hj' : x >>> (i - n) = x >>> j :=  by simp only [j]
-    rw [hj, hj', ← shiftLeft_eq, Nat.add_comm, shiftRight_add, shiftLeft_shiftRight]
-  · simp only [hni, decide_false, Bool.false_and, beq_eq_false_iff_ne, ne_eq]
-    simp only [Nat.not_le] at hni
-    rw [← shiftLeft_eq]
-    let k := n - i
-    have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel]; omega
-    rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
-    have hk' : 0 < k := by omega
-    have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
-      rw [Nat.mul_comm, Nat.div_mul_cancel]
-      suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
-        exact ⟨_, hs.symm⟩
-      let j := k - 1
-      have hj : 2 ^ (k - 1) = 2 ^ j := by simp only [j]
-      have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel]; omega
-      rw [hj, hj']
-      simp only [Nat.pow_add, Nat.pow_one, j, k]
-      rw [Nat.mul_comm, Nat.mul_assoc]
-    omega
+  · simp [hni, testBit_mul_two_pow_le hni]
+  · have : i < n := by omega
+    simp [hni, testBit_mul_two_pow_gt this]
 
 theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
   simp

From 43f82c4e473c7815b4f193c55d0e0af8d3c73e59 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 18:09:55 +0000
Subject: [PATCH 08/20] chore: remove useless rw in testBit_mul_two_pow_gt

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index af72b2797848..0b11e229d147 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -133,10 +133,8 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
     rw [Nat.mul_comm, Nat.div_mul_cancel]
     suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
       exact ⟨_, hs.symm⟩
-    let j := k - 1
-    have hj : 2 ^ (k - 1) = 2 ^ j := by simp only [j]
-    have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel]; omega
-    rw [hj, hj', Nat.pow_add, Nat.pow_one, Nat.mul_comm, Nat.mul_assoc]
+    rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel]
+    omega
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 17f153108899b2c4a0872ab12e438c8ca2392499 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Mon, 13 Jan 2025 18:15:24 +0000
Subject: [PATCH 09/20] chore: inline redundant omega

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 0b11e229d147..6981bc56406c 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -125,7 +125,8 @@ theorem testBit_mul_two_pow_le {x i n : Nat} (h : n ≤ i) :
 
 theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
     testBit (x * 2 ^ n) i = false := by
-  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero, beq_eq_false_iff_ne, ne_eq, ← shiftLeft_eq]
+  simp only [testBit, ← shiftLeft_eq, one_and_eq_mod_two, mod_two_bne_zero, beq_eq_false_iff_ne,
+    ne_eq]
   let k := n - i
   have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel]; omega
   rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
@@ -133,8 +134,7 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
     rw [Nat.mul_comm, Nat.div_mul_cancel]
     suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
       exact ⟨_, hs.symm⟩
-    rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel]
-    omega
+    rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 57edc99e8b4dcd38f68a5f0a27aea902f22c90de Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 08:20:14 +0000
Subject: [PATCH 10/20] chore: simplify suffices further

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 6981bc56406c..19cb734776e0 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -131,10 +131,14 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
   have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel]; omega
   rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
   have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
-    rw [Nat.mul_comm, Nat.div_mul_cancel]
-    suffices hs : 2 * (x * 2 ^ (k - 1)) = x * 2 ^ k by
-      exact ⟨_, hs.symm⟩
-    rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
+    rw [Nat.mul_comm, Nat.mul_div_assoc, ← Nat.pow_one (a := 2), Nat.pow_div (by omega) (by omega)]
+    · rw [Nat.mul_assoc, ← Nat.pow_add, Nat.sub_add_cancel]
+      omega
+    · suffices hs : 2 * (2 ^ (k - 1)) = 2 ^ k by
+        exact ⟨_, hs.symm⟩
+      rw [← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.pow_one]
+      congr 1
+      omega
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 1fa28d564bd1188484bc4535c155614a644537a1 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 08:22:02 +0000
Subject: [PATCH 11/20] chore: remove omega where res suffice

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 19cb734776e0..79a63be3159b 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -136,9 +136,7 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
       omega
     · suffices hs : 2 * (2 ^ (k - 1)) = 2 ^ k by
         exact ⟨_, hs.symm⟩
-      rw [← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.pow_one]
-      congr 1
-      omega
+      rw [← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.pow_one, ← Nat.add_sub_assoc (by omega), Nat.add_comm, Nat.add_sub_cancel]
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 465522be6938d855973483c27ec8a460d14da101 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 08:26:14 +0000
Subject: [PATCH 12/20] chore: inline more omegas where possible

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 79a63be3159b..8b011b4a83a7 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -119,7 +119,7 @@ theorem testBit_mul_two_pow_le {x i n : Nat} (h : n ≤ i) :
     testBit (x * 2 ^ n) i = testBit x (i - n) := by
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
   let j := i - n
-  have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp only [j]; rw [Nat.sub_add_cancel]; omega
+  have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp only [j]; rw [Nat.sub_add_cancel (by omega)]
   have hj' : x >>> (i - n) = x >>> j :=  by simp only [j]
   rw [hj, hj', ← shiftLeft_eq, Nat.add_comm, shiftRight_add, shiftLeft_shiftRight]
 
@@ -128,15 +128,17 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
   simp only [testBit, ← shiftLeft_eq, one_and_eq_mod_two, mod_two_bne_zero, beq_eq_false_iff_ne,
     ne_eq]
   let k := n - i
-  have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel]; omega
+  have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel (by omega)]
   rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
   have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
     rw [Nat.mul_comm, Nat.mul_div_assoc, ← Nat.pow_one (a := 2), Nat.pow_div (by omega) (by omega)]
-    · rw [Nat.mul_assoc, ← Nat.pow_add, Nat.sub_add_cancel]
-      omega
+    · rw [Nat.mul_assoc, ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
     · suffices hs : 2 * (2 ^ (k - 1)) = 2 ^ k by
         exact ⟨_, hs.symm⟩
-      rw [← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.pow_one, ← Nat.add_sub_assoc (by omega), Nat.add_comm, Nat.add_sub_cancel]
+      let j := k - 1
+      have hj : 2 * 2 ^ (k - 1) = 2 * 2 ^ j := by simp only [j, k]
+      have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel (by omega)]
+      rw [hj, hj', Nat.pow_succ, Nat.mul_comm]
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 79ba4babe74a34a0c0b0e0366916f26c6c972418 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 08:40:07 +0000
Subject: [PATCH 13/20] chore: simplify _gt proof further

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 8b011b4a83a7..c9aa0f503f30 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -130,15 +130,14 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
   let k := n - i
   have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel (by omega)]
   rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
-  have hx : 2 * (x * 2 ^ k / 2) = x * 2 ^ k := by
-    rw [Nat.mul_comm, Nat.mul_div_assoc, ← Nat.pow_one (a := 2), Nat.pow_div (by omega) (by omega)]
-    · rw [Nat.mul_assoc, ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
-    · suffices hs : 2 * (2 ^ (k - 1)) = 2 ^ k by
-        exact ⟨_, hs.symm⟩
-      let j := k - 1
-      have hj : 2 * 2 ^ (k - 1) = 2 * 2 ^ j := by simp only [j, k]
-      have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel (by omega)]
-      rw [hj, hj', Nat.pow_succ, Nat.mul_comm]
+  have hx : 2 * (x * 2 ^ k / 2 ^ 1) = x * 2 ^ k := by
+    rw [Nat.mul_div_assoc, Nat.pow_div (by omega) (by omega), Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
+    suffices hs : 2 * (2 ^ (k - 1)) = 2 ^ k by
+      exact ⟨_, hs.symm⟩
+    let j := k - 1
+    have hj : 2 * 2 ^ (k - 1) = 2 * 2 ^ (j) := by simp only [j, k]
+    have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel (by omega)]
+    rw [hj, hj', Nat.pow_succ, Nat.mul_comm]
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 340e8d6c51d9407c2f699883d5fde8ea51a5fc28 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 08:42:05 +0000
Subject: [PATCH 14/20] chore: remove ugly suffices

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index c9aa0f503f30..9a8b27c53139 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -132,12 +132,7 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
   rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
   have hx : 2 * (x * 2 ^ k / 2 ^ 1) = x * 2 ^ k := by
     rw [Nat.mul_div_assoc, Nat.pow_div (by omega) (by omega), Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
-    suffices hs : 2 * (2 ^ (k - 1)) = 2 ^ k by
-      exact ⟨_, hs.symm⟩
-    let j := k - 1
-    have hj : 2 * 2 ^ (k - 1) = 2 * 2 ^ (j) := by simp only [j, k]
-    have hj' : 2 ^ k = 2 ^ (j + 1) := by simp only [j]; rw [Nat.sub_add_cancel (by omega)]
-    rw [hj, hj', Nat.pow_succ, Nat.mul_comm]
+    simp only [Nat.pow_one, Nat.pow_dvd_pow (m := 1) (n := k) (a := 2) (by omega), k]
   omega
 
 theorem testBit_mul_two_pow (x i n : Nat) :

From 159a9f2b8b2de0b40ad1d3ccbe59eeff2351db76 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Tue, 14 Jan 2025 16:13:50 +0000
Subject: [PATCH 15/20] chore: golf testBit_mul_two_pow proof

Co-authored-by: Alex Keizer <alex@keizer.dev>
---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 9a8b27c53139..e90f97c38a17 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -137,10 +137,9 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
 
 theorem testBit_mul_two_pow (x i n : Nat) :
     testBit (x * 2 ^ n) i = if n ≤ i then testBit x (i - n) else false := by
-  by_cases hni : n ≤ i
-  · simp [hni, testBit_mul_two_pow_le hni]
-  · have : i < n := by omega
-    simp [hni, testBit_mul_two_pow_gt this]
+  split
+  · simpa [*] using testBit_mul_two_pow_le (by assumption)
+  · simpa [*] using testBit_mul_two_pow_gt (by omega)
 
 theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
   simp

From 4946b2e9f4c0d15673637df7f780688fc2113e45 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Tue, 14 Jan 2025 16:41:43 +0000
Subject: [PATCH 16/20] chore: replace testBit_mul_pow_ge proof strategy with
 calc and suffices

Co-authored-by: Alex Keizer <alex@keizer.dev>
---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index e90f97c38a17..0374314ecf0f 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -127,13 +127,14 @@ theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
     testBit (x * 2 ^ n) i = false := by
   simp only [testBit, ← shiftLeft_eq, one_and_eq_mod_two, mod_two_bne_zero, beq_eq_false_iff_ne,
     ne_eq]
+  suffices ∃ y, x <<< n >>> i = 2 * y by omega
   let k := n - i
-  have hk : x <<< n >>> i = x <<< (k + i) >>> i := by simp only [k]; rw [Nat.sub_add_cancel (by omega)]
-  rw [hk, Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
-  have hx : 2 * (x * 2 ^ k / 2 ^ 1) = x * 2 ^ k := by
-    rw [Nat.mul_div_assoc, Nat.pow_div (by omega) (by omega), Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_one (a := 2), ← Nat.pow_add, Nat.sub_add_cancel (by omega)]
-    simp only [Nat.pow_one, Nat.pow_dvd_pow (m := 1) (n := k) (a := 2) (by omega), k]
-  omega
+  refine ⟨x * 2 ^ (k - 1), ?_⟩
+  calc  x <<< n >>> i
+    _ = x <<< (k + i) >>> i := by rw [Nat.sub_add_cancel (by omega)]
+    _ = x * 2 ^ k           := by rw [Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
+    _ = x * 2 ^ (k - 1 + 1) := by rw [Nat.sub_add_cancel (by omega)]
+    _ = 2 * _               := by rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_comm]
 
 theorem testBit_mul_two_pow (x i n : Nat) :
     testBit (x * 2 ^ n) i = if n ≤ i then testBit x (i - n) else false := by

From f585dd63bbc0518553a88ebbb4ea6e8ba1afa863 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 17:02:07 +0000
Subject: [PATCH 17/20] chore: replace haves with calc in
 testBit_mul_two_pow_le strategy

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

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 0374314ecf0f..8e3f80ba3b88 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -119,9 +119,10 @@ theorem testBit_mul_two_pow_le {x i n : Nat} (h : n ≤ i) :
     testBit (x * 2 ^ n) i = testBit x (i - n) := by
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
   let j := i - n
-  have hj : (x * 2 ^ n) >>> i = (x * 2 ^ n) >>> (j + n) :=  by simp only [j]; rw [Nat.sub_add_cancel (by omega)]
-  have hj' : x >>> (i - n) = x >>> j :=  by simp only [j]
-  rw [hj, hj', ← shiftLeft_eq, Nat.add_comm, shiftRight_add, shiftLeft_shiftRight]
+  congr 2
+  calc (x * 2 ^ n) >>> i
+    _ = (x * 2 ^ n) >>> (n + j) :=  by simp [Nat.shiftRight_add, Nat.shiftRight_eq_div_pow, Nat.pow_add, Nat.mul_div_cancel, show i = n + j by omega]
+    _ = x >>> j :=  by rw [Nat.shiftRight_add, shiftRight_eq_div_pow (n := n), Nat.mul_div_cancel]; simp [Nat.pow_pos (a := 2) (n := n) (by omega)];
 
 theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
     testBit (x * 2 ^ n) i = false := by

From 3203e11ff866c6900f761e6523b3ad45879465fa Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Tue, 14 Jan 2025 17:02:32 +0000
Subject: [PATCH 18/20] chore: replace haves with calc in
 testBit_mul_two_pow_le strategy

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

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 8e3f80ba3b88..bc9bdfa53004 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -121,8 +121,8 @@ theorem testBit_mul_two_pow_le {x i n : Nat} (h : n ≤ i) :
   let j := i - n
   congr 2
   calc (x * 2 ^ n) >>> i
-    _ = (x * 2 ^ n) >>> (n + j) :=  by simp [Nat.shiftRight_add, Nat.shiftRight_eq_div_pow, Nat.pow_add, Nat.mul_div_cancel, show i = n + j by omega]
-    _ = x >>> j :=  by rw [Nat.shiftRight_add, shiftRight_eq_div_pow (n := n), Nat.mul_div_cancel]; simp [Nat.pow_pos (a := 2) (n := n) (by omega)];
+    _ = (x * 2 ^ n) >>> (n + j) :=  by simp [show i = n + j by omega, shiftRight_eq_div_pow, Nat.pow_add]
+    _ = x >>> j :=  by simp [Nat.shiftRight_add, shiftRight_eq_div_pow (n := n), Nat.mul_div_cancel, Nat.pow_pos (a := 2) (n := n) (by omega)];
 
 theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
     testBit (x * 2 ^ n) i = false := by

From e299ea1defaf688b82a864adcebbf176ee944d6d Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 15 Jan 2025 08:18:36 +0000
Subject: [PATCH 19/20] chore: remove useless theorem, simplify
 testBit_mul_two_pow

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 33 ++++-----------------------
 1 file changed, 5 insertions(+), 28 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index bc9bdfa53004..18902ca66d83 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -115,34 +115,6 @@ theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i :=
     rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
       Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]
 
-theorem testBit_mul_two_pow_le {x i n : Nat} (h : n ≤ i) :
-    testBit (x * 2 ^ n) i = testBit x (i - n) := by
-  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
-  let j := i - n
-  congr 2
-  calc (x * 2 ^ n) >>> i
-    _ = (x * 2 ^ n) >>> (n + j) :=  by simp [show i = n + j by omega, shiftRight_eq_div_pow, Nat.pow_add]
-    _ = x >>> j :=  by simp [Nat.shiftRight_add, shiftRight_eq_div_pow (n := n), Nat.mul_div_cancel, Nat.pow_pos (a := 2) (n := n) (by omega)];
-
-theorem testBit_mul_two_pow_gt {x i n : Nat} (h : i < n) :
-    testBit (x * 2 ^ n) i = false := by
-  simp only [testBit, ← shiftLeft_eq, one_and_eq_mod_two, mod_two_bne_zero, beq_eq_false_iff_ne,
-    ne_eq]
-  suffices ∃ y, x <<< n >>> i = 2 * y by omega
-  let k := n - i
-  refine ⟨x * 2 ^ (k - 1), ?_⟩
-  calc  x <<< n >>> i
-    _ = x <<< (k + i) >>> i := by rw [Nat.sub_add_cancel (by omega)]
-    _ = x * 2 ^ k           := by rw [Nat.shiftLeft_add, Nat.shiftLeft_shiftRight, shiftLeft_eq]
-    _ = x * 2 ^ (k - 1 + 1) := by rw [Nat.sub_add_cancel (by omega)]
-    _ = 2 * _               := by rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_comm]
-
-theorem testBit_mul_two_pow (x i n : Nat) :
-    testBit (x * 2 ^ n) i = if n ≤ i then testBit x (i - n) else false := by
-  split
-  · simpa [*] using testBit_mul_two_pow_le (by assumption)
-  · simpa [*] using testBit_mul_two_pow_gt (by omega)
-
 theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
   simp
 
@@ -748,6 +720,10 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
   rw [mod_two_eq_one_iff_testBit_zero, testBit_shiftLeft]
   simp
 
+theorem testBit_mul_two_pow (x i n : Nat) :
+    (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n)) := by
+  rw [← testBit_shiftLeft, shiftLeft_eq]
+
 theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
     (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
   simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]
@@ -761,6 +737,7 @@ theorem shiftLeft_or_distrib {a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i
 theorem shiftLeft_xor_distrib {a b : Nat} : (a ^^^ b) <<< i = a <<< i ^^^ b <<< i :=
   shiftLeft_bitwise_distrib
 
+
 @[simp] theorem decide_shiftRight_mod_two_eq_one :
     decide (x >>> i % 2 = 1) = x.testBit i := by
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]

From 4dc929007e4924b5c75c41992620294f6202fcd0 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Wed, 15 Jan 2025 08:26:47 +0000
Subject: [PATCH 20/20] chore: fix theorems ordering

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 18902ca66d83..4970c5b9d7e8 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -452,15 +452,6 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
       case neg =>
         apply Nat.add_lt_add <;> exact hyp1
 
-theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
-    (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
-  apply Nat.eq_of_testBit_eq
-  simp only [testBit_mul_two_pow, testBit_bitwise of_false_false, Bool.if_false_right]
-  intro i
-  by_cases hn : n ≤ i
-  · simp [hn]
-  · simp [hn, of_false_false]
-
 theorem bitwise_div_two_pow (of_false_false : f false false = false := by rfl) :
   (bitwise f x y) / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
@@ -724,6 +715,15 @@ theorem testBit_mul_two_pow (x i n : Nat) :
     (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n)) := by
   rw [← testBit_shiftLeft, shiftLeft_eq]
 
+theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
+    (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
+  apply Nat.eq_of_testBit_eq
+  simp only [testBit_mul_two_pow, testBit_bitwise of_false_false, Bool.if_false_right]
+  intro i
+  by_cases hn : n ≤ i
+  · simp [hn]
+  · simp [hn, of_false_false]
+
 theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
     (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
   simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]