diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 864843c6b1..3b85d79ac9 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -257,6 +257,11 @@ theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a :
 attribute [bv_normalize] BitVec.mul_zero
 attribute [bv_normalize] BitVec.zero_mul
 
+
+attribute [bv_normalize] BitVec.shiftLeft_ofNat_eq
+attribute [bv_normalize] BitVec.ushiftRight_ofNat_eq
+attribute [bv_normalize] BitVec.sshiftRight'_ofNat_eq_sshiftRight
+
 attribute [bv_normalize] BitVec.shiftLeft_zero
 attribute [bv_normalize] BitVec.zero_shiftLeft
 
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 5a28d192b0..6b9977a607 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -52,6 +52,9 @@ example : BitVec.sshiftRight 0#16 n = 0#16 := by bv_normalize
 example {x : BitVec 16} : BitVec.sshiftRight x 0 = x := by bv_normalize
 example {x : BitVec 16} : 0#16 * x = 0 := by bv_normalize
 example {x : BitVec 16} : x * 0#16 = 0 := by bv_normalize
+example {x : BitVec 16} : x >>> (12 : Nat) = x >>> 12#16 := by bv_normalize
+example {x : BitVec 16} : x <<< (12 : Nat) = x <<< 12#16 := by bv_normalize
+example {x : BitVec 16} : x.sshiftRight (12 : Nat) = x.sshiftRight' 12#16 := by bv_normalize
 example {x : BitVec 16} : x <<< 0#16 = x := by bv_normalize
 example {x : BitVec 16} : x <<< 0 = x := by bv_normalize
 example : 0#16 <<< (n : Nat) = 0 := by bv_normalize