diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 658b5bdb4e..5e8d98f8fc 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -375,5 +375,49 @@ theorem BitVec.mul_ones (a : BitVec w) : a * -1#w = -a := by
   rw [_root_.BitVec.mul_neg]
   simp
 
+-- All push a to the lhs as the rhs is guaranteed to be a constant so this form improves sharing.
+@[bv_normalize]
+theorem BitVec.add_const_beq_const {a : BitVec w} :
+    ((a + BitVec.ofNat w b) == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
+  rw [Bool.eq_iff_iff]
+  simp [BitVec.eq_sub_iff_add_eq]
+
+@[bv_normalize]
+theorem BitVec.const_add_beq_const :
+    ((BitVec.ofNat w b + a) == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
+  rw [Bool.eq_iff_iff, BitVec.add_comm _ a]
+  simp [BitVec.eq_sub_iff_add_eq]
+
+@[bv_normalize]
+theorem BitVec.const_beq_add_const_beq :
+    (BitVec.ofNat w c == (a + BitVec.ofNat w b)) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
+  rw [Bool.eq_iff_iff, Bool.beq_comm]
+  simp [BitVec.eq_sub_iff_add_eq]
+
+@[bv_normalize]
+theorem BitVec.const_beq_const_add_beq :
+    (BitVec.ofNat w c == (BitVec.ofNat w b + a)) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
+  rw [Bool.eq_iff_iff, BitVec.add_comm _ a, Bool.beq_comm]
+  simp [BitVec.eq_sub_iff_add_eq]
+
+@[bv_normalize]
+theorem BitVec.and_const_left :
+    BitVec.ofNat w a &&& (BitVec.ofNat w b &&& c) = (BitVec.ofNat w a &&& BitVec.ofNat w b) &&& c := by
+  ac_rfl
+
+@[bv_normalize]
+theorem BitVec.and_const_right :
+    BitVec.ofNat w a &&& (b &&& BitVec.ofNat w c) = (BitVec.ofNat w a &&& BitVec.ofNat w c) &&& b := by
+  ac_rfl
+
+@[bv_normalize]
+theorem BitVec.and_const_left' :
+    (BitVec.ofNat w a &&& b) &&& BitVec.ofNat w c = (BitVec.ofNat w a &&& BitVec.ofNat w c) &&& b := by
+  ac_rfl
+
+@[bv_normalize]
+theorem BitVec.and_const_right' {a : BitVec w} :
+    (a &&& BitVec.ofNat w b) &&& BitVec.ofNat w c = (BitVec.ofNat w b &&& BitVec.ofNat w c) &&& a := by
+  ac_rfl
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index e57fbe3de5..4222f8c54e 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -291,16 +291,16 @@ example (a : BitVec 16) : a + a = a <<< 1 := by
   bv_normalize
 
 -- NOT_EQUAL_BV1_BOOL
-example : ∀ (a : Bool), (!(a == true)) = (a == false) := by
+example : ∀ (a : Bool), (!(a == true)) = (!a) := by
   bv_normalize
 
-example : ∀ (a : Bool), (!(a == false)) = (a == true) := by
+example : ∀ (a : Bool), (!(a == false)) = a := by
   bv_normalize
 
-example : ∀ (a : Bool), (!(true == a)) = (a == false) := by
+example : ∀ (a : Bool), (!(true == a)) = !a := by
   bv_normalize
 
-example : ∀ (a : Bool), (!(false == a)) = (a == true) := by
+example : ∀ (a : Bool), (!(false == a)) = a := by
   bv_normalize
 
 example : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
@@ -561,6 +561,18 @@ example {a : BitVec 8} : a <<< 3 = BitVec.extractLsb' 0 5 a ++ 0#3 := by bv_norm
 example {a : BitVec 8} : a <<< 8 = 0 := by bv_normalize
 example {a : BitVec 8} : a <<< 12 = 0 := by bv_normalize
 
+-- EQUAL_CONST_BV_ADD
+example {a : BitVec 8} (h : a + 5 = 7) : a = 2 := by bv_normalize
+example {a : BitVec 8} (h : 5 + a = 7) : a = 2 := by bv_normalize
+example {a : BitVec 8} (h : 7 = a + 5) : a = 2 := by bv_normalize
+example {a : BitVec 8} (h : 7 = 5 + a) : a = 2 := by bv_normalize
+
+-- BV_AND_CONST
+example {x : BitVec 8} : (10 &&& x) &&& 2 = 2 &&& x := by bv_normalize
+example {x : BitVec 8} : (x &&& 10) &&& 2 = 2 &&& x := by bv_normalize
+example {x : BitVec 8} : 2 &&& (x &&& 10) = 2 &&& x := by bv_normalize
+example {x : BitVec 8} : 2 &&& (10 &&& x) = 2 &&& x := by bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by