From 90389a8d90f1367cc27c79532e496a7d6c421e65 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sat, 22 Nov 2025 13:48:48 +1100
Subject: [PATCH] feat: improvements to `grind` annotations for `Fin` (#11299)

This PR add many `@[grind]` annotations for `Fin`, and updates the
tests.
---
 src/Init/Data/BitVec/Lemmas.lean         |   2 +-
 src/Init/Data/Fin/Basic.lean             |   5 +
 src/Init/Data/Fin/Lemmas.lean            | 119 +++--
 src/Init/GrindInstances/ToInt.lean       |   2 +-
 src/Init/Prelude.lean                    |   1 +
 tests/lean/grind/grind_fin.lean          | 435 +++--------------
 tests/lean/run/grind_cutsat_toint_1.lean |  10 +-
 tests/lean/run/grind_fin.lean            | 573 +++++++++++++++++++++--
 8 files changed, 706 insertions(+), 441 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f54cb55926..3f39df519e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/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
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index ba12a6027b..c6bdde60c7 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/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
 
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index fb9effeb8c..0b1025bbc5 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -16,17 +16,25 @@ open Std
 
 namespace Fin
 
-@[simp] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
+@[simp, grind =] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
 
 @[deprecated ofNat_zero (since := "2025-05-28")] abbrev ofNat'_zero := @ofNat_zero
 
 theorem mod_def (a m : Fin n) : a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
   rfl
 
+theorem val_mod (a m : Fin n) : (a % m).val = a.val % m.val := rfl
+
 theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := rfl
 
+theorem val_mul (a b : Fin n) : (a * b).val = (a.val * b.val) % n := rfl
+
 theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := rfl
 
+@[grind =]
+theorem val_sub (a b : Fin n) : (a - b).val = ((n - b.val) + a.val) % n := rfl
+
+@[grind →]
 theorem pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.pos
 
 @[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
@@ -38,7 +46,8 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
 
 @[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
 
-@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
+@[ext, grind ext]
+protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
 
 theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
 
@@ -69,7 +78,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 
 @[deprecated val_ofNat (since := "2025-05-28")] abbrev val_ofNat' := @val_ofNat
 
-@[simp] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
+@[simp, grind =] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
   ext
   simp
   congr
@@ -89,7 +98,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
   rfl
 
-@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
+@[simp, grind =] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
   rfl
 
 @[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
@@ -259,7 +268,9 @@ instance : LawfulOrderLT (Fin n) where
   lt_iff := by
     simp [← Fin.not_le, Decidable.imp_iff_not_or, Std.Total.total]
 
-@[simp, grind =] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
+@[simp] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
+
+grind_pattern val_rev => i.rev
 
 @[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
   rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
@@ -284,6 +295,8 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
 
 @[simp] theorem val_last (n : Nat) : (last n).1 = n := rfl
 
+grind_pattern val_last => last n
+
 @[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
   ext
   simp
@@ -393,6 +406,8 @@ theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt zero_lt_one
 
 @[simp] theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := rfl
 
+grind_pattern val_succ => j.succ
+
 @[simp] theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by
   simp [Fin.lt_def]
 
@@ -453,12 +468,18 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
 theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
   Fin.ne_of_gt (one_lt_succ_succ a)
 
-@[simp] theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
+@[simp, grind =] theorem val_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
+
+@[deprecated val_castLT (since := "2025-11-21")]
+theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
 
 @[simp] theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ :=
   rfl
 
-@[simp, grind =] theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
+@[simp, grind =] theorem val_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
+
+@[deprecated val_castLE (since := "2025-11-21")]
+theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
 
 @[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
     castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := rfl
@@ -470,13 +491,16 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
     Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
-  Fin.ext (by simp only [coe_castLE])
+  Fin.ext (by simp only [val_castLE])
 
 @[simp] theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
     Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
   funext (castLE_castLE km mn)
 
-@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
+@[simp, grind =] theorem val_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
+
+@[deprecated val_cast (since := "2025-11-21")]
+theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
 @[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
     Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
@@ -489,7 +513,7 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
-  Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
+  Fin.ext (by rw [val_cast, val_last, val_last, Nat.succ.inj h])
 
 @[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
 
@@ -504,7 +528,10 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
 
-@[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
+@[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
+
+@[deprecated val_castAdd (since := "2025-11-21")]
+theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
 @[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := rfl
 
@@ -540,7 +567,10 @@ the reverse direction. -/
 theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
     (i.cast h).succ = i.succ.cast (by rw [h]) := rfl
 
-@[simp] theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
+@[simp, grind =] theorem val_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
+
+@[deprecated val_castSucc (since := "2025-11-21")]
+theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
 
 @[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt_succ_of_lt h⟩ := rfl
 
@@ -548,7 +578,7 @@ theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
     i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
 
 theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ :=
-  lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
+  lt_def.2 <| by simp only [val_castSucc, val_succ, Nat.lt_succ_self]
 
 theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by
   simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
@@ -602,7 +632,7 @@ theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
 
 @[deprecated castSucc_lt_succ (since := "2025-10-29")]
 theorem lt_succ {a : Fin n} : a.castSucc < a.succ := by
-  rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
+  rw [castSucc, lt_def, val_castAdd, val_succ]; exact Nat.lt_succ_self a.val
 
 theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n :=
   ⟨fun ⟨j, hj⟩ => hj ▸ Fin.ne_of_lt j.castSucc_lt_last,
@@ -610,7 +640,10 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
 
 theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
 
-@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+
+@[deprecated val_addNat (since := "2025-11-21")]
+theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
 
 @[simp] theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by
   ext
@@ -638,7 +671,10 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
     (addNat i m').cast h = addNat i m :=
   Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
 
-@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
+@[simp, grind =] theorem val_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
+
+@[deprecated val_natAdd (since := "2025-11-21")]
+theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
 
 @[simp] theorem natAdd_mk (n i : Nat) (hi : i < m) :
     natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := rfl
@@ -695,7 +731,7 @@ theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSu
   omega
 
 theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
-  rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
+  rw [val_rev, val_castAdd, val_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
 
 theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
   rw [← rev_rev (castAdd ..), rev_castAdd, rev_rev]
@@ -717,7 +753,12 @@ theorem castSucc_natAdd (n : Nat) (i : Fin k) :
 
 /-! ### pred -/
 
-@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
+@[simp] theorem val_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
+
+grind_pattern val_pred => j.pred h
+
+@[deprecated val_pred (since := "2025-11-21")]
+theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
 
 @[simp] theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
   | ⟨0, _⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
@@ -735,7 +776,7 @@ theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin
 theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
     Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
       ⟨i, h⟩ := by
-  simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]
+  simp only [Fin.ext_iff, val_pred, Nat.add_sub_cancel]
 
 @[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
     Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := pred_mk_succ i _
@@ -762,10 +803,13 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
 
 theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
-  rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
+  rw [Fin.ext_iff, val_pred, val_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
   exact Nat.add_lt_add_right h 1
 
-@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
+@[simp, grind =] theorem val_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
+
+@[deprecated val_subNat (since := "2025-11-21")]
+theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
 
 @[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
     subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := rfl
@@ -830,11 +874,11 @@ step. `Fin.succRec` is a version of this induction principle that takes the `Fin
     (zero : ∀ n, motive (n + 1) 0) (succ : ∀ n i, motive n i → motive (Nat.succ n) i.succ) :
     motive n i := i.succRec zero succ
 
-@[simp] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
+@[simp, grind =] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
     @Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by
   cases n <;> rfl
 
-@[simp] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
+@[simp, grind =] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
@@ -862,11 +906,11 @@ where
   | 0, hi => by rwa [Fin.mk_zero]
   | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
 
-@[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+@[simp, grind =] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     (induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := rfl
 
-@[simp] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+@[simp, grind =] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
     induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
 
@@ -898,13 +942,13 @@ The corresponding induction principle is `Fin.induction`.
     (zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
     ∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
 
-@[simp] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
+@[simp, grind =] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
     @Fin.cases n motive zero succ 0 = zero := rfl
 
-@[simp] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
+@[simp, grind =] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
     @Fin.cases n motive zero succ i.succ = succ i := rfl
 
-@[simp] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
+@[simp, grind =] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
     {i : Nat} (h : i + 1 < n + 1) :
     @Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
 
@@ -954,7 +998,7 @@ For the induction:
       | j + 1 => go j (by omega) (by omega) (cast ⟨j, by omega⟩ x)
   go _ _ (by omega) last
 
-@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
+@[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
     (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
   rw [reverseInduction, reverseInduction.go]; simp
 
@@ -971,7 +1015,7 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) 
     dsimp only
     rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
 
-@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
+@[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
     (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
       succ i (reverseInduction zero succ i.succ) := by
   rw [reverseInduction, reverseInduction_castSucc_aux _ _ _ i.isLt, reverseInduction]
@@ -990,11 +1034,11 @@ The corresponding induction principle is `Fin.reverseInduction`.
     (cast : ∀ i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
   reverseInduction last (fun i _ => cast i) i
 
-@[simp] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
+@[simp, grind =] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
     (Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last :=
   reverseInduction_last ..
 
-@[simp] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
+@[simp, grind =] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
     (i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
   reverseInduction_castSucc ..
 
@@ -1014,11 +1058,11 @@ as `Fin.natAdd m (j : Fin n)`.
   if hi : (i : Nat) < m then (castAdd_castLT n i hi) ▸ (left (castLT i hi))
   else (natAdd_subNat_cast (Nat.le_of_not_lt hi)) ▸ (right _)
 
-@[simp] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
+@[simp, grind =] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
     addCases (motive := motive) left right (Fin.castAdd n i) = left i := by
   rw [addCases, dif_pos (castAdd_lt _ _)]; rfl
 
-@[simp]
+@[simp, grind =]
 theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
     addCases (motive := motive) left right (natAdd m i) = right i := by
   have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
@@ -1051,6 +1095,7 @@ theorem add_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 
 /-! ### sub -/
 
+@[deprecated val_sub (since := "2025-11-21")]
 protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
   cases a; cases b; rfl
 
@@ -1102,6 +1147,7 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
 
 /-! ### neg -/
 
+@[grind =]
 theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
     (-x).val = if x = 0 then 0 else n - x.val := by
   change (n - ↑x) % n = _
@@ -1117,7 +1163,7 @@ protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by
     apply elim0 x
   · replace h : NeZero n := ⟨h⟩
     ext
-    rw [Fin.coe_sub, Fin.val_add, val_neg]
+    rw [Fin.val_sub, Fin.val_add, val_neg]
     split
     · simp_all
     · simp [Nat.add_comm]
@@ -1138,9 +1184,6 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 
 @[deprecated mul_ofNat (since := "2025-05-28")] abbrev mul_ofNat' := @mul_ofNat
 
-theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
-  | ⟨_, _⟩, ⟨_, _⟩ => rfl
-
 @[deprecated val_mul (since := "2025-10-26")]
 theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
diff --git a/src/Init/GrindInstances/ToInt.lean b/src/Init/GrindInstances/ToInt.lean
index e48d1fd2c1..626b1c2ac3 100644
--- a/src/Init/GrindInstances/ToInt.lean
+++ b/src/Init/GrindInstances/ToInt.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
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a09c3986b5..a9620a757e 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.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
diff --git a/tests/lean/grind/grind_fin.lean b/tests/lean/grind/grind_fin.lean
index 4508d9b961..3047a1a88c 100644
--- a/tests/lean/grind/grind_fin.lean
+++ b/tests/lean/grind/grind_fin.lean
@@ -5,409 +5,108 @@ Many of these will remain out of scope, and can be deleted as this is decided.
 
 open Fin
 
-example (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := by grind
+namespace Fin'
 
-example {n a : Nat} {ha : a < n} [NeZero n] :
+/-! Challenge problems: -/
+
+theorem mk_eq_zero {n a : Nat} {ha : a < n} [NeZero n] :
     (⟨a, ha⟩ : Fin n) = 0 ↔ a = 0 := by grind
 
-example {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by grind
+theorem zero_eq_mk {n a : Nat} {ha : a < n} [NeZero n] :
+    0 = (⟨a, ha⟩ : Fin n) ↔ a = 0 := by grind
 
-example [NeZero n] (x : Fin n) : (Fin.ofNat n x.val) = x := by grind
+theorem zero_eq_one_iff {n : Nat} [NeZero n] : (0 : Fin n) = 1 ↔ n = 1 := by grind
 
-example (a : Fin (2 * n + 1)) : a.val + (-a).val = 2 * n + 1 := by grind
+theorem one_eq_zero_iff {n : Nat} [NeZero n] : (1 : Fin n) = 0 ↔ n = 1 := by grind
 
-example [NeZero n] {a : Fin n} : 0 < a ↔ a ≠ 0 := by grind
+theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by grind
 
-example (i : Fin n) : rev (rev i) = i := by grind
+theorem last_add_one : ∀ n, last n + 1 = 0 := by grind
 
-example {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by grind
+theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
+    ((i + 1 : Fin (n + 1)) : Nat) = if i = last _ then (0 : Nat) else i + 1 := by grind
 
-example {i j : Fin n} : rev i = rev j ↔ i = j := by grind
+theorem val_two {n : Nat} : (2 : Fin (n + 3)).val = 2 := by grind
 
-example (n : Nat) : (last n).1 = n := by grind
+theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1 := by grind
 
-example {n : Nat} : (0 : Fin (n + 1)) = last n ↔ n = 0 := by grind
+theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := by grind
 
-example {n : Nat} : Fin.last n = 0 ↔ n = 0 := by grind
+theorem succ_one_eq_two : Fin.succ (1 : Fin (n + 2)) = 2 := by grind
 
-example (i : Fin (n + 1)) : i ≤ last n := by grind
+theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by grind
 
-example : (0 : Fin (n + 2)) < last (n + 1) := by grind
+theorem add_one_le_iff {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _ := by grind
 
-example {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n := by grind
+theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by grind
 
-example {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n := by grind
+theorem castSucc_inj {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by grind
 
-example (n : Nat) : rev (last n) = 0 := by grind
+theorem castSucc_eq_zero_iff [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0 := by grind
 
-example (n : Nat) : rev 0 = last n := by grind
+theorem castSucc_ne_zero_iff [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 := by grind
 
-example {n : Nat} : (2 : Fin (n + 3)).val = 2 := by grind
-example {n : Nat} : (17 : Fin (n + 18)).val = 17 := by grind
+theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by grind
 
-example : (0 : Fin (n + 2)) < 1 := by grind
+theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n := by grind
 
-example (j : Fin n) : (j.succ : Nat) = j + 1 := by grind
-
-example (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by grind
-
-example {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b := by grind
-
-example {a b : Fin n} : a.succ < b.succ ↔ a < b := by grind
-
-example {a b : Fin n} : a.succ = b.succ ↔ a = b := by grind
-
-example {n} : ∀ k : Fin n, Fin.succ k ≠ 0 := by grind
-
-example {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by grind
-
-example {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _ := by grind
-
-example {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by grind
-
-example {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by grind
-
-example (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := by grind
-
-example (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ := by grind
-
-example (i n m : Nat) (hn : i < n) (h : n ≤ m) :
-    castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := by grind
-
-example {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by grind
-
-example {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
-    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by grind
-
-example {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
-    Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i := by grind
-
-example {k m n} (km : k ≤ m) (mn : m ≤ n) :
-    Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) := by grind
-
-example (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := by grind
-
-example {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
-    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) := by grind
-
-example {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
-    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) := by grind
-
-example [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := by grind
-
-example {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' := by grind
-
-example (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := by grind
-
-example (n : Nat) (h : n = n) : Fin.cast h = id := by grind
-
-example {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := by grind
-
-example (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := by grind
-
-example : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := by grind
-
-example {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by grind
-
-example (m : Nat) (i : Nat) (h : i < n) :
-    castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right m h⟩ := by grind
-
-example (m : Nat) (i : Fin (n + m)) (hi : i.val < n) :
-    castAdd m (castLT i hi) = i := by grind
-
-example (m : Nat) (i : Fin n) :
-    castLT (castAdd m i) (castAdd_lt m i) = i := by grind
-
-example {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
-    castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := by grind
-
-example {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
-    (i.castAdd m).cast h = (i.cast (Nat.add_right_cancel h)).castAdd m := by grind
-
-example {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
-    (i.castAdd m').cast h = i.castAdd m := by grind
-
-example {m n p : Nat} (i : Fin m) :
-    (i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm  := by grind
-
-example {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
-    i.succ.cast h = (i.cast (Nat.succ.inj h)).succ := by grind
-
-example {n' : Nat} (i : Fin n) (h : n = n') :
-    (i.cast h).succ = i.succ.cast (by rw [h]) := by grind
-
-example (i : Fin n) : (i.castSucc : Nat) = i := by grind
-
-example (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt.step h⟩ := by grind
-
-example {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
-    i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := by grind
-
-example (i : Fin n) : i.castSucc < i.succ := by grind
-
-example {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by grind
-
-example {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
-    i.castSucc < j ↔ i.succ ≤ j := by grind
-
-example (n : Nat) : (last n).succ = last n.succ := by grind
-
-example {n : Nat} {i : Fin n.succ} :
-    i.succ = last (n + 1) ↔ i = last n := by grind
-
-example (i : Fin (n + 1)) (h : (i : Nat) < n) :
-    (castLT i h).castSucc = i := by grind
-
-example {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
-    castLT a.castSucc h = a := by grind
-
-example {a b : Fin n} :
-    a.castSucc < b.castSucc ↔ a < b := by grind
-
-example {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by grind
-
-example (a : Fin n) : a.castSucc < last n := by grind
-
-example [NeZero n] : castSucc (0 : Fin n) = 0 := by grind
-
-example {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := by grind
-
-example [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by grind
-
-example [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0 := by grind
-
-example [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 := by grind
-
-example {a : Fin n} : a.castSucc + 1 = a.succ := by grind
-
-example {a : Fin n} : a.castSucc < a.succ := by grind
-
-example {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n := by grind
-
-example (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := by grind
-
-example (n : Nat) (i : Fin n) : addNat i 0 = i := by grind
-
-example {i : Fin n} : addNat i 1 = i.succ := by grind
-
-example (m : Nat) (i : Fin n) : m ≤ addNat i m := by grind
-
-example (n i : Nat) (hi : i < m) :
-    addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := by grind
-
-example {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
-    (addNat i 0).cast h = i.cast ((Nat.add_zero _).symm.trans h) := by grind
-
-example {n n' m : Nat} (i : Fin n') (h : n' = n) :
-    addNat (i.cast h) m = (addNat i m).cast (congrArg (. + m) h) := by grind
-
-example {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
-    (addNat i m).cast h = addNat (i.cast (Nat.add_right_cancel h)) m := by grind
-
-example {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
-    (addNat i m').cast h = addNat i m := by grind
-
-example (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := by grind
-
-example (n i : Nat) (hi : i < m) :
-    natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := by grind
-
-example (m : Nat) (i : Fin n) : m ≤ natAdd m i := by grind
-
-example {n : Nat} : natAdd 0 = Fin.cast (Nat.zero_add n).symm := by grind
-
-example {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
-    natAdd m (i.cast h) = (natAdd m i).cast (congrArg _ h) := by grind
-
-example {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
-    (natAdd m i).cast h  = natAdd m (i.cast (Nat.add_left_cancel h)) := by grind
-
-example {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
-    (natAdd m' i).cast h = natAdd m i := by grind
-
-example (p m : Nat) {n : Nat} (i : Fin n) :
-    castAdd p (natAdd m i) = (natAdd m (castAdd p i)).cast (Nat.add_assoc ..).symm := by grind
-
-example (p m : Nat) {n : Nat} (i : Fin n) :
-    natAdd m (castAdd p i) = (castAdd p (natAdd m i)).cast (Nat.add_assoc ..) := by grind
-
-example (m n : Nat) {p : Nat} (i : Fin p) :
-    natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) := by grind
-
-example {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
-    (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by grind
-
-example (n : Nat) {m : Nat} (i : Fin m) :
-    (natAdd n i).cast (Nat.add_comm ..) = addNat i n := by grind
-
-example {n : Nat} (m : Nat) (i : Fin n) :
-    (addNat i m).cast (Nat.add_comm ..) = natAdd m i := by grind
-
-example {m n : Nat} : natAdd n (last m) = last (n + m) := by grind
-
-example (n : Nat) :
-    addNat (last n) m = (last (n + m)).cast (by grind) := by grind
-
-example (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n := by grind
-
-example (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := by grind
-
-example (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by grind
-
-example (k : Fin n) : rev (castSucc k) = succ (rev k) := by grind
-
-example (k : Fin n) : rev (succ k) = castSucc (rev k) := by grind
-
-example (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := by grind
-
-example : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i := by grind
-
-example (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by grind
-
-example {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} :
-    i.pred hi = j ↔ i = j.succ := by grind
-
-example (i : Nat) (h : i < n + 1) :
-    Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
-      ⟨i, h⟩ := by grind
-
-example (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
-    Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := by grind
-
-example {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w =
-    ⟨i - 1, Nat.sub_lt_right_of_lt_add (Nat.pos_iff_ne_zero.2 (Fin.val_ne_of_ne w)) h⟩ := by grind
-
-example {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
-    a.pred ha ≤ b.pred hb ↔ a ≤ b := by grind
-
-example {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
-    a.pred ha < b.pred hb ↔ a < b := by grind
-
-example :
-    ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b := by grind
-
-example {n : Nat} :
-    Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := by grind
-
-example (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
+theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by grind
 
-example (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := by grind
-
-example {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
-    subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := by grind
-
-example (i : Fin n) (h : 0 ≤ (i : Nat)): Fin.subNat 0 i h = i := by grind
-
-example (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by grind
-
-example (i : Fin n) :
-    pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := by grind
-
-example {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i := by grind
-
-example (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
-    subNat m (addNat i m) h = i := by grind
-
-example {i : Fin (n + m)} (h : n ≤ i) :
-    natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i := by grind
-
-/-! ### Recursion and induction principles -/
-
-example {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
-    @Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by grind
-
-example {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
-    @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by grind
-
-example {motive : Fin (n + 1) → Sort _} (zero : motive 0)
-    (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
-    (induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := by grind
-
-example {motive : Fin (n + 1) → Sort _} (zero : motive 0)
-    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
-    induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := by grind
-
-example {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
-    @Fin.cases n motive zero succ 0 = zero := by grind
-
-example {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
-    @Fin.cases n motive zero succ i.succ = succ i := by grind
-
-example {n} {motive : Fin (n + 1) → Sort _} {zero succ}
-    {i : Nat} (h : i + 1 < n + 1) :
-    @Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by grind
-
-example {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P 0 ∧ ∀ i : Fin n, P i.succ := by grind
-
-example {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i : Fin n, P i.succ := by grind
-
-example {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 := by grind
-
-example {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 := by grind
-
-example {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 := by grind
-
-example {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 := by grind
-
-example {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
-    (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by grind
-
-example {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
-    (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
-      succ i (reverseInduction zero succ i.succ) := by grind
-
-example {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
-    (Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last := by grind
-
-example {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
-    (i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i := by grind
-
-example {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
-    addCases (motive := motive) left right (Fin.castAdd n i) = left i := by grind
-
-example {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
-    addCases (motive := motive) left right (natAdd m i) = right i := by grind
-
-example [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0 := by grind
-
-example [NeZero n] {a : Fin n} : a.val ≠ 0 ↔ a ≠ 0 := by grind
-
-example [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat_add [NeZero n] (x : Nat) (y : Fin n) :
     Fin.ofNat n x + y = Fin.ofNat n (x + y.val) := by grind
 
-example [NeZero n] (x : Fin n) (y : Nat) :
+theorem add_ofNat [NeZero n] (x : Fin n) (y : Nat) :
     x + Fin.ofNat n y = Fin.ofNat n (x.val + y) := by grind
 
-
-example (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by grind
-
-example [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat_sub [NeZero n] (x : Nat) (y : Fin n) :
     Fin.ofNat n x - y = Fin.ofNat n ((n - y.val) + x) := by grind
 
-example [NeZero n] (x : Fin n) (y : Nat) :
-    x - Fin.ofNat n y = Fin.ofNat n ((n - y % n) + x.val) := by grind
-
-example {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
+private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
     x % n = x - n := by grind
 
-example {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by grind
+theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by grind
 
-example {a b : Fin n} : b ≤ a → (a - b).val = a.val - b.val := by grind
+theorem sub_val_of_le {a b : Fin n} : b ≤ a → (a - b).val = a.val - b.val := by grind
 
-example {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by grind
+theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by grind
 
-/-! ### neg -/
+theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by grind [Fin.val_add]
 
-example {n : Nat} [NeZero n] (x : Fin n) :
-    (-x).val = if x = 0 then 0 else n - x.val := by grind
-
-example {n : Nat} (x y : Fin n) : x - y = x + -y := by grind
-
-/-! ### mul -/
-
-example [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat_mul [NeZero n] (x : Nat) (y : Fin n) :
     Fin.ofNat n x * y = Fin.ofNat n (x * y.val) := by grind
 
-example [NeZero n] (x : Fin n) (y : Nat) :
+theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
     x * Fin.ofNat n y = Fin.ofNat n (x.val * y) := by grind
+
+/-! Shouldn't expect to work by `grind`: -/
+
+theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) := by grind
+
+theorem eq_zero_or_eq_succ {n : Nat} : ∀ i : Fin (n + 1), i = 0 ∨ ∃ j : Fin n, i = j.succ := by grind
+
+theorem eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j : Fin n, i = j.succ := by grind
+
+theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by grind
+
+instance subsingleton_zero : Subsingleton (Fin 0) := by grind
+
+instance subsingleton_one : Subsingleton (Fin 1) := by grind
+
+theorem forall_fin_succ {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P 0 ∧ ∀ i : Fin n, P i.succ := by grind
+
+theorem exists_fin_succ {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i : Fin n, P i.succ := by grind
+
+theorem forall_fin_zero {p : Fin 0 → Prop} : (∀ i, p i) ↔ True := by grind
+
+theorem exists_fin_zero {p : Fin 0 → Prop} : (∃ i, p i) ↔ False := by grind
+
+theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 := by grind
+
+theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 := by grind
+
+theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 := by grind
+
+theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 := by grind
+
+end Fin'
diff --git a/tests/lean/run/grind_cutsat_toint_1.lean b/tests/lean/run/grind_cutsat_toint_1.lean
index 10df6531fe..3a00503b77 100644
--- a/tests/lean/run/grind_cutsat_toint_1.lean
+++ b/tests/lean/run/grind_cutsat_toint_1.lean
@@ -83,6 +83,11 @@ example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := by
 /--
 trace: [grind.lia.model] a := 2
 [grind.lia.model] b := 0
+[grind.lia.model] ↑a := 2
+[grind.lia.model] ↑b := 0
+[grind.lia.model] ↑0 := 0
+[grind.lia.model] ↑1 := 1
+[grind.lia.model] ↑(a + b) := 2
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.lia.model true in
@@ -90,7 +95,10 @@ example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → Fa
   grind
 
 -- We use `↑a` when pretty printing `ToInt.toInt a`
-/-- trace: [grind.debug.ring.basis] ↑a + ↑b + -1 * ((↑a + ↑b) % 3) + -3 * ((↑a + ↑b) / 3) = 0 -/
+/--
+trace: [grind.debug.ring.basis] ↑a + ↑b + -1 * ((↑a + ↑b) % 3) + -3 * ((↑a + ↑b) / 3) = 0
+[grind.debug.ring.basis] b = 0
+-/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.debug.ring.basis true in
 example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → False := by
diff --git a/tests/lean/run/grind_fin.lean b/tests/lean/run/grind_fin.lean
index 66a07b3135..9d5ba05846 100644
--- a/tests/lean/run/grind_fin.lean
+++ b/tests/lean/run/grind_fin.lean
@@ -48,46 +48,555 @@ example (i : Fin (n + 1)) : i.1 ≤ n := by grind
 
 example {x y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x := by grind
 
-example : (Fin.last 0 : Fin 1) = 0 := by grind
-
-example (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := by grind
-
-example {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
-    (i.cast h).cast h' = i.cast (Eq.trans h h') := by grind
-
-example (n : Nat) (j : Fin n) :
-    j.succ.castSucc = (j.castSucc).succ := by grind
-
-example {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := by grind
-
-example {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) := by grind
-
-example (i : Fin n) : i.succ.castSucc = i.castSucc.succ := by grind
-
-example (h : n ≤ n) (i : Fin n) : i.castLE h = i := by grind
-
-example (h : n ≤ m) (i : Fin n) :
-    (i.castLE h).castSucc = i.castLE (by omega) := by grind
-
-example (n : Nat) (i : Fin k) :
-    (i.natAdd n).castSucc = (i.castSucc).natAdd n := by grind
-
-example : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by grind
-
 example [NeZero n] {x : Fin n} : x - x = 0 := by grind
 
 example {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n := by grind
 
 example {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n := by grind
 
-example [i : NeZero n] (k : Fin n) : k * 1 = k := by grind
+open Std Fin
 
-example (a b : Fin n) : a * b = b * a := by grind
+namespace Fin'
 
-example (a b c : Fin n) : a * b * c = a * (b * c) := by grind
+theorem is_lt (a : Fin n) : (a : Nat) < n := by grind
 
-example [NeZero n] (k : Fin n) : (1 : Fin n) * k = k := by grind
+/-! ### coercions and constructions -/
 
-example [NeZero n] (k : Fin n) : k * 0 = 0 := by grind
+theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := by grind
 
-example [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by grind
+theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := by grind
+
+theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := by grind
+
+theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ := by grind [cases Fin]
+
+theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
+    (⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := by grind
+
+theorem val_mk {m n : Nat} (h : m < n) : (⟨m, h⟩ : Fin n).val = m := by grind
+
+theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := by grind
+
+theorem val_ofNat (n : Nat) [NeZero n] (a : Nat) :
+  (Fin.ofNat n a).val = a % n := by grind
+
+theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val := by grind
+
+theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val := by grind
+
+theorem val_eq_zero (a : Fin 1) : a.val = 0 := by grind
+
+theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
+    (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by grind
+
+theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
+    (if c then x else y).val = if c then x.val else y.val := by grind
+
+open IntCast in
+theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
+    (x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := by grind [Fin.intCast_def]
+
+/-! ### order -/
+
+theorem le_def {a b : Fin n} : a ≤ b ↔ a.1 ≤ b.1 := by grind
+
+theorem lt_def {a b : Fin n} : a < b ↔ a.1 < b.1 := by grind
+
+theorem not_le {a b : Fin n} : ¬ a ≤ b ↔ b < a := by grind
+
+theorem not_lt {a b : Fin n} : ¬ a < b ↔ b ≤ a := by grind
+
+theorem le_refl (a : Fin n) : a ≤ a := by grind
+
+theorem lt_irrefl (a : Fin n) : ¬ a < a := by grind
+
+theorem le_trans {a b c : Fin n} : a ≤ b → b ≤ c → a ≤ c := by grind
+
+theorem lt_trans {a b c : Fin n} : a < b → b < c → a < c := by grind
+
+theorem le_total (a b : Fin n) : a ≤ b ∨ b ≤ a := by grind
+
+theorem lt_asymm {a b : Fin n} (h : a < b) : ¬ b < a := by grind
+
+theorem ne_of_lt {a b : Fin n} (h : a < b) : a ≠ b := by grind
+
+theorem ne_of_gt {a b : Fin n} (h : a < b) : b ≠ a := by grind
+
+theorem le_of_lt {a b : Fin n} (h : a < b) : a ≤ b := by grind
+
+theorem lt_of_le_of_lt {a b c : Fin n} : a ≤ b → b < c → a < c := by grind
+
+theorem lt_of_lt_of_le {a b c : Fin n} : a < b → b ≤ c → a < c := by grind
+
+theorem le_rfl {a : Fin n} : a ≤ a := by grind
+
+theorem lt_iff_le_and_ne {a b : Fin n} : a < b ↔ a ≤ b ∧ a ≠ b := by grind
+
+theorem lt_or_lt_of_ne {a b : Fin n} (h : a ≠ b) : a < b ∨ b < a := by grind
+
+theorem lt_or_le (a b : Fin n) : a < b ∨ b ≤ a := by grind
+
+theorem le_or_lt (a b : Fin n) : a ≤ b ∨ b < a := by grind
+
+theorem le_of_eq {a b : Fin n} (hab : a = b) : a ≤ b := by grind
+
+theorem ge_of_eq {a b : Fin n} (hab : a = b) : b ≤ a := by grind
+
+theorem eq_or_lt_of_le {a b : Fin n} : a ≤ b → a = b ∨ a < b := by grind
+
+theorem lt_or_eq_of_le {a b : Fin n} : a ≤ b → a < b ∨ a = b := by grind
+
+theorem is_le (i : Fin (n + 1)) : i.1 ≤ n := by grind
+
+theorem is_le' {a : Fin n} : a ≤ n := by grind
+
+theorem le_antisymm_iff {x y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x := by grind
+
+theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := by grind
+
+theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := by grind
+
+theorem rev_rev (i : Fin n) : rev (rev i) = i := by grind
+
+theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by grind
+
+theorem rev_inj {i j : Fin n} : rev i = rev j ↔ i = j := by grind
+
+theorem rev_lt_rev {i j : Fin n} : rev i < rev j ↔ j < i := by grind
+
+theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by grind
+
+theorem fin_one_eq_zero (a : Fin 1) : a = 0 := by grind
+
+theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := by grind
+
+theorem zero_add [NeZero n] (k : Fin n) : (0 : Fin n) + k = k := by grind
+
+theorem add_zero [NeZero n] (k : Fin n) : k + 0 = k := by grind
+
+theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := by grind
+
+theorem cast_cast {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
+    (i.cast h).cast h' = i.cast (Eq.trans h h') := by grind
+
+theorem castLE_refl (h : n ≤ n) (i : Fin n) : i.castLE h = i := by grind
+
+theorem castSucc_castLE (h : n ≤ m) (i : Fin n) :
+    (i.castLE h).castSucc = i.castLE (by omega) := by grind
+
+theorem castSucc_natAdd (n : Nat) (i : Fin k) :
+    (i.natAdd n).castSucc = (i.castSucc).natAdd n := by grind
+
+theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := by grind
+
+theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) := by grind
+
+theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by grind
+
+theorem sub_self [NeZero n] {x : Fin n} : x - x = 0 := by grind
+
+theorem mul_one [i : NeZero n] (k : Fin n) : k * 1 = k := by grind
+
+theorem mul_comm (a b : Fin n) : a * b = b * a := by grind
+
+theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by grind
+
+theorem one_mul [NeZero n] (k : Fin n) : (1 : Fin n) * k = k := by grind
+
+theorem mul_zero [NeZero n] (k : Fin n) : k * 0 = 0 := by grind
+
+theorem zero_mul [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by grind
+
+theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := by grind
+
+theorem mod_def (a m : Fin n) :
+    a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) := by grind
+
+theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := by grind
+
+theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := by grind
+
+theorem pos' [Nonempty (Fin n)] : 0 < n := by grind
+
+theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
+    a = ⟨k, hk⟩ ↔ (a : Nat) = k := by grind
+
+theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by grind
+
+theorem ofNat_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat n x.val) = x := by
+  -- mod_eq_of_lt might be plausible for the implication gadget?
+  grind [Nat.mod_eq_of_lt]
+
+theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b := by grind
+
+theorem mk_lt_of_lt_val {b : Fin n} {a : Nat} (h : a < b) :
+    (⟨a, Nat.lt_trans h b.is_lt⟩ : Fin n) < b := by grind
+
+theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
+    (⟨a, Nat.lt_of_le_of_lt h b.is_lt⟩ : Fin n) ≤ b := by grind
+
+theorem mk_le_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) ≤ ⟨y, hy⟩ ↔ x ≤ y := by grind
+
+theorem mk_lt_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) < ⟨y, hy⟩ ↔ x < y := by grind
+
+theorem val_last (n : Nat) : (last n).1 = n := by grind
+
+theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.pos) := by grind
+
+theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := by grind
+
+theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ := by grind
+
+theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
+    castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := by grind
+
+theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
+    Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i := by grind
+
+theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
+    Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) := by grind
+
+theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := by grind
+
+theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
+    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) := by grind
+
+theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
+    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) := by grind
+
+theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := by grind
+
+theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := by grind
+
+theorem cast_refl (n : Nat) (h : n = n) : Fin.cast h = id := by grind
+
+theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := by grind
+
+theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := by grind
+
+theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by grind
+
+theorem castLT_castAdd (m : Nat) (i : Fin n) :
+    castLT (castAdd m i) (castAdd_lt m i) = i := by grind
+
+theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := by grind
+
+theorem succ_last (n : Nat) : (last n).succ = last n.succ := by grind
+
+theorem succ_eq_last_succ {n : Nat} {i : Fin n.succ} :
+    i.succ = last (n + 1) ↔ i = last n := by grind
+
+theorem castLT_castSucc {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
+    castLT a.castSucc h = a := by grind
+
+theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := by grind
+
+theorem le_coe_addNat (m : Nat) (i : Fin n) : m ≤ addNat i m := by grind
+
+theorem cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
+    (addNat i 0).cast h = i.cast ((Nat.add_zero _).symm.trans h) := by grind
+
+theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := by grind
+
+theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := by grind
+
+theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by grind
+
+theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
+    (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by grind
+
+theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w =
+    ⟨i - 1, Nat.sub_lt_right_of_lt_add (Nat.pos_iff_ne_zero.2 (Fin.val_ne_of_ne w)) h⟩ := by grind
+
+theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := by grind
+
+theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
+    subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := by grind
+
+theorem subNat_zero (i : Fin n) (h : 0 ≤ (i : Nat)): Fin.subNat 0 i h = i := by grind
+
+theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by grind
+
+theorem pred_castSucc_succ (i : Fin n) :
+    pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := by grind
+
+theorem subNat_addNat (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
+    subNat m (addNat i m) h = i := by grind
+
+theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
+    @Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by grind
+
+theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
+    @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by grind
+
+theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
+    (induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := by grind
+
+theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
+    induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := by grind
+
+theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
+    @Fin.cases n motive zero succ 0 = zero := by grind
+
+theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
+    @Fin.cases n motive zero succ i.succ = succ i := by grind
+
+theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
+    {i : Nat} (h : i + 1 < n + 1) :
+    @Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by grind
+
+theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
+    (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by grind
+
+theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
+    (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
+      succ i (reverseInduction zero succ i.succ) := by grind
+
+theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
+    (Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last := by grind
+
+theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
+    (i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i := by grind
+
+theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
+    addCases (motive := motive) left right (Fin.castAdd n i) = left i := by grind
+
+theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
+    addCases (motive := motive) left right (natAdd m i) = right i := by grind
+
+theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
+    (-x).val = if x = 0 then 0 else n - x.val := by grind
+
+theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by grind
+
+theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
+  | ⟨_, _⟩, ⟨_, _⟩ => by grind
+
+theorem le_last (i : Fin (n + 1)) : i ≤ last n := by grind
+
+theorem eq_last_of_not_lt {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n := by grind
+
+theorem val_lt_last {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n := by grind
+
+theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := by grind
+
+theorem succ_le_succ_iff {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b := by grind
+
+theorem succ_lt_succ_iff {a b : Fin n} : a.succ < b.succ ↔ a < b := by grind
+
+theorem succ_inj {a b : Fin n} : a.succ = b.succ ↔ a = b := by grind
+
+theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := by grind
+
+theorem le_coe_natAdd (m : Nat) (i : Fin n) : m ≤ natAdd m i := by grind
+
+theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by grind
+
+-- From this point onwards we need `@[grind ext]` on `Fin.ext`.
+
+
+theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
+    rev i = ⟨a, Nat.lt_succ_of_le (h ▸ Nat.le_add_right ..)⟩ := by grind
+
+theorem castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
+    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by grind
+
+theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' := by grind
+
+theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := by grind
+
+theorem castAdd_mk (m : Nat) (i : Nat) (h : i < n) :
+    castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right m h⟩ := by grind
+
+theorem castAdd_castLT (m : Nat) (i : Fin (n + m)) (hi : i.val < n) :
+    castAdd m (castLT i hi) = i := by grind
+
+theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
+    castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := by grind
+
+theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
+    (i.castAdd m).cast h = (i.cast (Nat.add_right_cancel h)).castAdd m := by grind
+
+theorem cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
+    (i.castAdd m').cast h = i.castAdd m := by grind
+
+theorem castAdd_castAdd {m n p : Nat} (i : Fin m) :
+    (i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm := by grind
+
+theorem cast_succ_eq {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
+    i.succ.cast h = (i.cast (Nat.succ.inj h)).succ := by grind
+
+theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
+    (i.cast h).succ = i.succ.cast (by rw [h]) := by grind
+
+theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt_succ_of_lt h⟩ := by grind
+
+theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
+    i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := by grind
+
+theorem castSucc_castLT (i : Fin (n + 1)) (h : (i : Nat) < n) :
+    (castLT i h).castSucc = i := by grind
+
+theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by grind
+
+theorem addNat_one {i : Fin n} : addNat i 1 = i.succ := by grind
+
+theorem addNat_mk (n i : Nat) (hi : i < m) :
+    addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := by grind
+
+theorem addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :
+    addNat (i.cast h) m = (addNat i m).cast (congrArg (. + m) h) := by grind
+
+theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
+    (addNat i m).cast h = addNat (i.cast (Nat.add_right_cancel h)) m := by grind
+
+theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
+    (addNat i m').cast h = addNat i m := by grind
+
+theorem natAdd_mk (n i : Nat) (hi : i < m) :
+    natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := by grind
+
+theorem natAdd_zero {n : Nat} : natAdd 0 = Fin.cast (Nat.zero_add n).symm := by grind
+
+theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
+    natAdd m (i.cast h) = (natAdd m i).cast (congrArg _ h) := by grind
+
+theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
+    (natAdd m i).cast h  = natAdd m (i.cast (Nat.add_left_cancel h)) := by grind
+
+theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
+    (natAdd m' i).cast h = natAdd m i := by grind
+
+theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
+    castAdd p (natAdd m i) = (natAdd m (castAdd p i)).cast (Nat.add_assoc ..).symm := by grind
+
+theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
+    natAdd m (castAdd p i) = (castAdd p (natAdd m i)).cast (Nat.add_assoc ..) := by grind
+
+theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
+    natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) := by grind
+
+theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
+    (natAdd n i).cast (Nat.add_comm ..) = addNat i n := by grind
+
+theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
+    (addNat i m).cast (Nat.add_comm ..) = natAdd m i := by grind
+
+theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := by grind
+
+theorem addNat_last (n : Nat) :
+    addNat (last n) m = (last (n + m)).cast (by omega) := by grind
+
+theorem natAdd_eq_addNat (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n := by grind
+
+theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := by grind
+
+theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by grind
+
+theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := by grind
+
+theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
+    Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
+      ⟨i, h⟩ := by grind
+
+theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
+    Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := by grind
+theorem addNat_subNat {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i := by grind
+
+theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
+    natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i := by grind
+
+theorem sub_ofNat [NeZero n] (x : Fin n) (y : Nat) :
+    x - Fin.ofNat n y = Fin.ofNat n ((n - y % n) + x.val) := by grind
+
+theorem succ_mk (n i : Nat) (h : i < n) :
+    Fin.succ ⟨i, h⟩ = ⟨i + 1, Nat.succ_lt_succ h⟩ := by grind
+
+/-! These could work, but need additional help from `grind`, because these annotations are bad: -/
+attribute [grind =] Fin.val_zero Fin.val_one Fin.le_def Fin.lt_def
+
+theorem val_zero (n : Nat) [NeZero n] : ((0 : Fin n) : Nat) = 0 := by grind
+
+theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := by grind
+
+theorem zero_le [NeZero n] (a : Fin n) : 0 ≤ a := by grind
+
+theorem zero_lt_one : (0 : Fin (n + 2)) < 1 := by grind
+
+theorem not_lt_zero [NeZero n] (a : Fin n) : ¬a < 0 := by grind
+
+theorem pos_iff_ne_zero [NeZero n] {a : Fin n} : 0 < a ↔ a ≠ 0 := by grind
+
+theorem zero_eq_last_iff {n : Nat} : (0 : Fin (n + 1)) = last n ↔ n = 0 := by grind
+
+theorem last_eq_zero_iff {n : Nat} : Fin.last n = 0 ↔ n = 0 := by grind
+
+theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := by grind
+
+theorem rev_last (n : Nat) : rev (last n) = 0 := by grind
+
+theorem rev_zero (n : Nat) : rev 0 = last n := by grind
+
+theorem val_one (n : Nat) : (1 : Fin (n + 2)).val = 1 := by grind
+
+theorem mk_one : (⟨1, Nat.succ_lt_succ (Nat.succ_pos n)⟩ : Fin (n + 2)) = (1 : Fin _) := by grind
+
+theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by grind
+
+theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0 := by grind
+
+theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := by grind
+
+theorem mk_succ_pos (i : Nat) (h : i < n) :
+    (0 : Fin (n + 1)) < ⟨i.succ, Nat.add_lt_add_right h 1⟩ := by grind
+
+theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by grind
+
+theorem le_zero_iff {n : Nat} {k : Fin (n + 1)} : k ≤ 0 ↔ k = 0 := by grind
+
+theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 := by grind
+
+theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by grind
+
+theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ := by grind
+
+theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by grind
+
+theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
+    i.castSucc < j ↔ i.succ ≤ j := by grind
+
+theorem castSucc_lt_castSucc_iff {a b : Fin n} :
+    a.castSucc < b.castSucc ↔ a < b := by grind
+
+theorem castSucc_lt_last (a : Fin n) : a.castSucc < last n := by grind
+
+theorem castSucc_zero [NeZero n] : castSucc (0 : Fin n) = 0 := by grind
+
+theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := by grind
+
+theorem castSucc_pos [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by grind
+
+theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := by grind
+
+theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i := by grind
+
+theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} :
+    i.pred hi = j ↔ i = j.succ := by grind
+
+theorem pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+    a.pred ha ≤ b.pred hb ↔ a ≤ b := by grind
+
+theorem pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+    a.pred ha < b.pred hb ↔ a < b := by grind
+
+theorem pred_inj :
+    ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b := by grind
+
+theorem pred_one {n : Nat} :
+    Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt zero_lt_one)) = 0 := by grind
+
+theorem val_eq_zero_iff [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0 := by grind
+
+theorem val_ne_zero_iff [NeZero n] {a : Fin n} : a.val ≠ 0 ↔ a ≠ 0 := by grind