feat: grind annotations relating Nat/Fin fold operations to List

src/Init/Data/List/FinRange.lean

@@ -62,7 +62,7 @@ end List
 
 namespace Fin
 
-theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α) :
+@[grind =] theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α) :
     foldlM n f x = (List.finRange n).foldlM f x := by
   induction n generalizing x with
   | zero => simp
@@ -72,21 +72,21 @@ theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α)
     funext y
     simp [ih, List.foldlM_map]
 
-theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
+@[grind =] theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
     foldrM n f x = (List.finRange n).foldrM f x := by
   induction n generalizing x with
   | zero => simp
   | succ n ih =>
     simp [foldrM_succ, List.finRange_succ, ih, List.foldrM_map]
 
-theorem foldl_eq_finRange_foldl (f : α → Fin n → α) (x : α) :
+@[grind =] theorem foldl_eq_finRange_foldl (f : α → Fin n → α) (x : α) :
     foldl n f x = (List.finRange n).foldl f x := by
   induction n generalizing x with
   | zero => simp
   | succ n ih =>
     simp [foldl_succ, List.finRange_succ, ih, List.foldl_map]
 
-theorem foldr_eq_finRange_foldr (f : Fin n → α → α) (x : α) :
+@[grind =] theorem foldr_eq_finRange_foldr (f : Fin n → α → α) (x : α) :
     foldr n f x = (List.finRange n).foldr f x := by
   induction n generalizing x with
   | zero => simp

src/Init/Data/Nat/Fold.lean

@@ -205,7 +205,7 @@ theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bo
 @[simp] theorem fold_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1 → α → α) (init : α) :
     fold (n + 1) f init = f n (by omega) (fold n (fun i h => f i (by omega)) init) := by simp [fold]
 
-theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
+@[grind =] theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
     fold n f init = (List.finRange n).foldl (fun acc ⟨i, h⟩ => f i h acc) init := by
   induction n with
   | zero => simp
@@ -221,7 +221,7 @@ theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n
     foldRev (n + 1) f init = foldRev n (fun i h => f i (by omega)) (f n (by omega) init) := by
   simp [foldRev]
 
-theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
+@[grind =] theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
     foldRev n f init = (List.finRange n).foldr (fun ⟨i, h⟩ acc => f i h acc) init := by
   induction n generalizing init with
   | zero => simp
@@ -234,7 +234,7 @@ theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i <
 @[simp] theorem any_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
     any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
 
-theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
+@[grind =] theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
     any n f = (List.finRange n).any (fun ⟨i, h⟩ => f i h) := by
   induction n with
   | zero => simp
@@ -247,7 +247,7 @@ theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
 @[simp] theorem all_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
     all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
 
-theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
+@[grind =] theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
     all n f = (List.finRange n).all (fun ⟨i, h⟩ => f i h) := by
   induction n with
   | zero => simp