diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 693926a4e445..dedf3c5a3454 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1512,7 +1512,6 @@ theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
   ext i
   simp [Nat.add_assoc n m i]
 
-@[simp]
 theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
     x >>> n <<< n = x &&& BitVec.allOnes w <<< n := by
   induction n generalizing x