diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean
index 850b7f8954..b62018dec0 100644
--- a/src/Init/Data/Nat/Bitwise/Basic.lean
+++ b/src/Init/Data/Nat/Bitwise/Basic.lean
@@ -144,7 +144,10 @@ Asserts that the `(n+1)`th least significant bit of `m` is not set.
 
 (This definition is used by Lean internally for compact bitmaps.)
 -/
-@[expose, reducible] protected def hasNotBit (m n : Nat) : Prop :=
-  1 &&& (m >>> n) ≠ 1
+@[expose] protected def hasNotBit (m n : Nat) : Prop :=
+  Nat.land 1 (Nat.shiftRight m n) ≠ 1
+
+@[grind =]
+theorem hasNotBit_eq (m n : Nat) : Nat.hasNotBit m n = (1 &&& (m >>> n) ≠ 1) := rfl
 
 end Nat