chore: change BitVec.intMin/Max from abbrev to def (#5252)

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!
 -/
 ```

src/Init/Data/BitVec/Lemmas.lean

@@ -1962,15 +1962,15 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
 /-! ### intMin -/
 
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
-abbrev intMin (w : Nat) := twoPow w (w - 1)
+def intMin (w : Nat) := twoPow w (w - 1)
 
 theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) := by
-  simp only [getLsbD_twoPow, boolToPropSimps]
+  simp only [intMin, getLsbD_twoPow, boolToPropSimps]
   omega
 
 @[simp, bv_toNat]
 theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
-  simp
+  simp [intMin]
 
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
@@ -1982,7 +1982,7 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
-abbrev intMax (w : Nat) := (twoPow w (w - 1)) - 1
+def intMax (w : Nat) := (twoPow w (w - 1)) - 1
 
 @[simp, bv_toNat]
 theorem toNat_intMax : (intMax w).toNat = 2 ^ (w - 1) - 1 := by