From 0bfbb71796e0e411e40e56d11532cb87a5eb140c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 13 Dec 2025 18:00:33 +0100
Subject: [PATCH] perf: restore kernel-reduction friendly Nat.hasNotBit
 definition (#11657)

This PR improves upon #11652 by keeping the kernel-reduction-optimized
definition.
---
 src/Init/Data/Nat/Bitwise/Basic.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

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