chore: change BitVec.intMin/Max from abbrev to def

[kim-em]

I don't think we gain anything from having them as abbrev here, and the simpNF linter complains:

-- Init.Data.BitVec.Lemmas
#check @BitVec.toNat_intMin /- simp can prove this:
  by simp only [BitVec.toNat_twoPow]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/
#check @BitVec.toNat_intMax /- Left-hand side simplifies from
  (BitVec.intMax w).toNat
to
  (2 ^ w - 1 % 2 ^ w + 2 ^ (w - 1)) % 2 ^ w
using
  simp only [@BitVec.toNat_sub, @BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat, BitVec.toNat_twoPow, Nat.add_mod_mod]
Try to change the left-hand side to the simplified term!
 -/

[kim-em]

@tobiasgrosser?

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c219303270c8db12c7f84e6ccc6e8b0b03f54216 --onto 66688e10ceef553f48b935a74d9bbd096edf96f5. (2024-09-04 04:13:18)