chore: use not_value at Nat.pow_pos

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 a -- Avoid excessive `BitVec` theorem instantiation (See `grind_lint_bitvec.lean`)
   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.
 #guard_msgs in
-#grind_lint inspect (min := 26)  BitVec.msb_signExtend
+#grind_lint inspect (min := 22)  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
+#grind_lint check (min := 20) in BitVec