diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 497c06b8674d..e74d513e329b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -939,6 +939,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext i
   simp
 
+@[simp]
+theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
+  ext i
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -1072,6 +1077,16 @@ theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
   cases h₅ : decide (i < n + m) <;>
     simp at * <;> omega
 
+@[simp]
+theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} {n : Nat} :
+    BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by
+  simp [← BitVec.shiftLeft_and_distrib]
+
+@[simp]
+theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
+    BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
+  simp [← shiftLeft_or_distrib]
+
 @[deprecated shiftLeft_add (since := "2024-06-02")]
 theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
     (x <<< n) <<< m = x <<< (n + m) := by
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index c6b9835ddd7a..2813f36f4b2e 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -61,6 +61,8 @@ attribute [bv_normalize] BitVec.getLsbD_zero_length
 attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
+attribute [bv_normalize] BitVec.not_not
+
 
 end Constant
 
@@ -141,11 +143,6 @@ theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
 theorem BitVec.zero_mul (a : BitVec w) : 0#w * a = 0#w := by
   simp [bv_toNat]
 
-@[bv_normalize]
-theorem BitVec.not_not (a : BitVec w) : ~~~(~~~a) = a := by
-  ext
-  simp
-
 @[bv_normalize]
 theorem BitVec.shiftLeft_zero (n : BitVec w) : n <<< 0#w' = n := by
   ext i