feat: improvements to grind annotations for Fin (#11299)

This PR add many `@[grind]` annotations for `Fin`, and updates the
tests.

Author: kim-em

src/Init/Data/BitVec/Lemmas.lean

@@ -1056,7 +1056,7 @@ theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
 @[simp, grind =] theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
     (setWidth' p x).toFin = x.toFin.castLE (Nat.pow_le_pow_right (by omega) (by omega)) := by
   ext
-  rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.coe_castLE, val_toFin,
+  rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.val_castLE, val_toFin,
     Nat.mod_eq_of_lt (by apply BitVec.toNat_lt_twoPow_of_le p)]
 
 theorem toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w ≤ w') : (b.setWidth w').toNat = b.toNat := by

src/Init/Data/Fin/Basic.lean

@@ -246,6 +246,11 @@ instance neg (n : Nat) : Neg (Fin n) :=
 
 theorem neg_def (a : Fin n) : -a = ⟨(n - a) % n, Nat.mod_lt _ a.pos⟩ := rfl
 
+-- Later we give another version called `Fin.val_neg` that splits on `a = 0`.
+protected theorem val_neg' (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
+  rfl
+
+@[deprecated Fin.val_neg' (since := "2025-11-21")]
 protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
   rfl
 

src/Init/Data/Fin/Lemmas.lean

@@ -108,7 +108,7 @@ instance : ToInt (Fin n) (.co 0 n) where
   toInt_inj x y w := Fin.eq_of_val_eq (Int.ofNat_inj.mp w)
   toInt_mem := by simp
 
-@[simp] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
+@[simp, grind =] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
 
 instance [NeZero n] : ToInt.Zero (Fin n) (.co 0 n) where
   toInt_zero := rfl

src/Init/GrindInstances/ToInt.lean

@@ -2264,6 +2264,7 @@ structure Fin (n : Nat) where
   isLt : LT.lt val n
 
 attribute [coe] Fin.val
+grind_pattern Fin.isLt => self.val
 
 theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl