chore: split proof of testBit_mul_two_pow and rtemove useless hypotheses

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