From 455fd0b4488e2adc85f825a52e2ee7d944a5740a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 4 Dec 2025 22:25:17 -0800
Subject: [PATCH] chore: use `not_value` at `Nat.pow_pos` (#11523)

and remove `TODO` from `grind_lint_bitvec.lean`
---
 src/Init/Data/Nat/Lemmas.lean              | 1 +
 tests/lean/run/grind_lint_bitvec.lean      | 4 +---
 tests/lean/run/grind_match_cond_issue.lean | 4 ++++
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index bf38670c6e..76ca3d7782 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1095,6 +1095,7 @@ grind_pattern div_pow_of_pos => a ^ n where
   guard n > 0
 
 grind_pattern Nat.pow_pos => a ^ n where
+  not_value n
   guard a > 0
 
 protected theorem pow_add' (a m n : Nat) : a ^ (m + n) = a ^ n * a ^ m := by
diff --git a/tests/lean/run/grind_lint_bitvec.lean b/tests/lean/run/grind_lint_bitvec.lean
index 1b3f2beebc..2b383ea83b 100644
--- a/tests/lean/run/grind_lint_bitvec.lean
+++ b/tests/lean/run/grind_lint_bitvec.lean
@@ -7,13 +7,11 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 #guard_msgs in
 #grind_lint inspect (min := 30) BitVec.msb_replicate
 
--- TODO: Reduce limit after we add support for `no_value` constraint
--- `BitVec.msb_signExtend` is reasonable at 22.
+-- `BitVec.msb_signExtend` is reasonable at 26.
 #guard_msgs in
 #grind_lint inspect (min := 26)  BitVec.msb_signExtend
 
 /-! Check BitVec namespace: -/
 
--- TODO: Reduce limit after we add support for `no_value` constraint. It was `20`
 #guard_msgs in
 #grind_lint check (min := 23) in BitVec
diff --git a/tests/lean/run/grind_match_cond_issue.lean b/tests/lean/run/grind_match_cond_issue.lean
index 869a9cd489..186c8ef3a4 100644
--- a/tests/lean/run/grind_match_cond_issue.lean
+++ b/tests/lean/run/grind_match_cond_issue.lean
@@ -15,3 +15,7 @@ example {n m a : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False)
 example {n m a : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False)
     (h : a ^ 2 = 4 ^ m * n) : False := by
   grind
+
+example {m a n : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * 4 * n → False)
+    (h : a ^ 2 = 4 ^ (m + 1) * n) : False := by
+  grind