chore: use not_value at Nat.pow_pos (#11523)

and remove `TODO` from `grind_lint_bitvec.lean`

Author: leodemoura

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

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

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