diff --git a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
index 17c74fddb2..7227775416 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Init.Data.BitVec
+import Std.Tactic.BVDecide.Syntax
 
 /-!
 This contains theorems responsible for turning both `Bool` and `BitVec` goals into the
@@ -97,6 +98,9 @@ attribute [bv_normalize] BitVec.neg_eq
 attribute [bv_normalize] BitVec.mul_eq
 attribute [bv_normalize] BitVec.udiv_eq
 attribute [bv_normalize] BitVec.umod_eq
+attribute [bv_normalize ←] BitVec.shiftLeft_eq'
+attribute [bv_normalize ←] BitVec.sshiftRight_eq'
+attribute [bv_normalize ←] BitVec.ushiftRight_eq'
 
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean
index ac848b25bd..fc90416f20 100644
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -95,6 +95,12 @@ syntax (name := bvNormalize) "bv_normalize" optConfig : tactic
 
 end Tactic
 
+/--
+Theorems tagged with the `bv_normalize` attribute are used during the rewriting step of the
+`bv_decide` tactic. 
+-/
+syntax (name := bv_normalize) "bv_normalize" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+
 /--
 Auxiliary attribute for builtin `bv_normalize` simprocs.
 -/
diff --git a/tests/lean/run/bv_decide_shift_to_nat.lean b/tests/lean/run/bv_decide_shift_to_nat.lean
new file mode 100644
index 0000000000..442f240440
--- /dev/null
+++ b/tests/lean/run/bv_decide_shift_to_nat.lean
@@ -0,0 +1,21 @@
+import Std.Tactic.BVDecide
+
+theorem test2 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    b <<< s.toNat = 0 := by
+  bv_decide
+
+theorem test2' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    b >>> s.toNat = 0 := by
+  bv_decide
+
+theorem test2'' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    BitVec.sshiftRight b s.toNat = 0 := by
+  bv_decide
+
+theorem test2''' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    BitVec.shiftLeft b s.toNat = 0 := by
+  bv_decide
+
+theorem test2'''' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    BitVec.ushiftRight b s.toNat = 0 := by
+  bv_decide