feat: revise grind annotations for bitwise operations

src/Init/Data/Bool.lean

@@ -434,9 +434,9 @@ Converts `true` to `1` and `false` to `0`.
 -/
 @[expose] def toNat (b : Bool) : Nat := cond b 1 0
 
-@[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl
+@[simp, bitvec_to_nat, grind =] theorem toNat_false : false.toNat = 0 := rfl
 
-@[simp, bitvec_to_nat] theorem toNat_true : true.toNat = 1 := rfl
+@[simp, bitvec_to_nat, grind =] theorem toNat_true : true.toNat = 1 := rfl
 
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
@@ -457,9 +457,9 @@ Converts `true` to `1` and `false` to `0`.
 -/
 @[expose] def toInt (b : Bool) : Int := cond b 1 0
 
-@[simp] theorem toInt_false : false.toInt = 0 := rfl
+@[simp, grind =] theorem toInt_false : false.toInt = 0 := rfl
 
-@[simp] theorem toInt_true : true.toInt = 1 := rfl
+@[simp, grind =] theorem toInt_true : true.toInt = 1 := rfl
 
 /-! ### ite -/
 

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -21,6 +21,7 @@ theorem natCast_shiftRight (n s : Nat) : (n : Int) >>> s = n >>> s := rfl
 theorem negSucc_shiftRight (m n : Nat) :
     -[m+1] >>> n = -[m >>>n +1] := rfl
 
+@[grind _=_]
 theorem shiftRight_add (i : Int) (m n : Nat) :
     i >>> (m + n) = i >>> m >>> n := by
   simp only [shiftRight_eq, Int.shiftRight]

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -105,7 +105,7 @@ theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
   | b+1 => (shiftLeft_eq _ b).trans <| by
     simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_comm]
 
-@[simp] theorem shiftRight_zero : n >>> 0 = n := rfl
+@[simp, grind =] theorem shiftRight_zero : n >>> 0 = n := rfl
 
 theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -81,10 +81,10 @@ noncomputable def div2Induction {motive : Nat → Sort u}
 
 /-! ### testBit -/
 
-@[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
+@[simp, grind =] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
   simp only [testBit, zero_shiftRight, and_zero, bne_self_eq_false]
 
-@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
+@[simp, grind =] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
   cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
 
 theorem mod_two_eq_one_iff_testBit_zero : (x % 2 = 1) ↔ x.testBit 0 = true := by
@@ -349,12 +349,16 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
   · simp
   · exact Nat.two_pow_pos _
 
-theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
+@[grind =]
+theorem testBit_bool_toNat (b : Bool) (i : Nat) :
     testBit (Bool.toNat b) i = (decide (i = 0) && b) := by
   cases b <;> cases i <;>
-  simp [testBit_eq_decide_div_mod_eq, 
+  simp [testBit_eq_decide_div_mod_eq,
         Nat.mod_eq_of_lt]
 
+@[deprecated testBit_bool_toNat (since := "2025-06-22")]
+abbrev testBit_bool_to_nat := @testBit_bool_toNat
+
 /-- `testBit 1 i` is true iff the index `i` equals 0. -/
 theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
@@ -543,15 +547,12 @@ abbrev and_pow_two_sub_one_of_lt_two_pow := @and_two_pow_sub_one_of_lt_two_pow
   rw [testBit_and]
   simp
 
-@[grind _=_]
 theorem and_div_two_pow : (a &&& b) / 2 ^ n = a / 2 ^ n &&& b / 2 ^ n :=
   bitwise_div_two_pow
 
-@[grind _=_]
 theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 :=
   and_div_two_pow (n := 1)
 
-@[grind _=_]
 theorem and_mod_two_pow : (a &&& b) % 2 ^ n = (a % 2 ^ n) &&& (b % 2 ^ n) :=
   bitwise_mod_two_pow
 
@@ -625,15 +626,12 @@ theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y
   rw [testBit_or]
   simp
 
-@[grind _=_]
 theorem or_div_two_pow : (a ||| b) / 2 ^ n = a / 2 ^ n ||| b / 2 ^ n :=
   bitwise_div_two_pow
 
-@[grind _=_]
 theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 :=
   or_div_two_pow (n := 1)
 
-@[grind _=_]
 theorem or_mod_two_pow : (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n :=
   bitwise_mod_two_pow
 
@@ -693,15 +691,12 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a
   rw [testBit_xor]
   simp
 
-@[grind _=_]
 theorem xor_div_two_pow : (a ^^^ b) / 2 ^ n = a / 2 ^ n ^^^ b / 2 ^ n :=
   bitwise_div_two_pow
 
-@[grind _=_]
 theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 :=
   xor_div_two_pow (n := 1)
 
-@[grind _=_]
 theorem xor_mod_two_pow : (a ^^^ b) % 2 ^ n = a % 2 ^ n ^^^ b % 2 ^ n :=
   bitwise_mod_two_pow
 

src/Init/Data/Nat/Lemmas.lean

@@ -1320,7 +1320,7 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   | k+1 =>
     rw [log2]; split
     · have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›
-      simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), 
+      simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0),
         Nat.pow_succ]
       exact Nat.le_div_iff_mul_le (by decide)
     · simp only [le_zero_eq, succ_ne_zero, false_iff]
@@ -1686,7 +1686,7 @@ theorem div_lt_div_of_lt_of_dvd {a b d : Nat} (hdb : d ∣ b) (h : a < b) : a /
 
 /-! ### shiftLeft and shiftRight -/
 
-@[simp] theorem shiftLeft_zero : n <<< 0 = n := rfl
+@[simp, grind =] theorem shiftLeft_zero : n <<< 0 = n := rfl
 
 /-- Shiftleft on successor with multiple moved inside. -/
 theorem shiftLeft_succ_inside (m n : Nat) : m <<< (n+1) = (2*m) <<< n := rfl
@@ -1705,14 +1705,15 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
   rw [shiftRight_succ _ (k+1)]
   rw [shiftRight_succ_inside _ k, shiftRight_succ]
 
-@[simp] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0
+@[simp, grind =] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0
   | 0 => by simp
   | n + 1 => by simp [zero_shiftLeft n, shiftLeft_succ]
 
-@[simp] theorem zero_shiftRight : ∀ n, 0 >>> n = 0
+@[simp, grind =] theorem zero_shiftRight : ∀ n, 0 >>> n = 0
   | 0 => by simp
   | n + 1 => by simp [zero_shiftRight n, shiftRight_succ]
 
+@[grind _=_]
 theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
   | 0 => rfl
   | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]