feat: grind annotations for List/Array/Vector.finRange theorems

Author: kim-em

src/Init/Data/Array/FinRange.lean

@@ -23,10 +23,10 @@ Examples:
 -/
 protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
 
-@[simp] theorem size_finRange {n} : (Array.finRange n).size = n := by
+@[simp, grind =] theorem size_finRange {n} : (Array.finRange n).size = n := by
   simp [Array.finRange]
 
-@[simp] theorem getElem_finRange {i : Nat} (h : i < (Array.finRange n).size) :
+@[simp, grind =] theorem getElem_finRange {i : Nat} (h : i < (Array.finRange n).size) :
     (Array.finRange n)[i] = Fin.cast size_finRange ⟨i, h⟩ := by
   simp [Array.finRange]
 
@@ -49,6 +49,7 @@ theorem finRange_succ_last {n} :
     · simp_all
       omega
 
+@[grind _=_]
 theorem finRange_reverse {n} : (Array.finRange n).reverse = (Array.finRange n).map Fin.rev := by
   ext i h
   · simp

src/Init/Data/List/FinRange.lean

@@ -23,14 +23,14 @@ Examples:
 -/
 def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
 
-@[simp] theorem length_finRange {n : Nat} : (List.finRange n).length = n := by
+@[simp, grind =] theorem length_finRange {n : Nat} : (List.finRange n).length = n := by
   simp [List.finRange]
 
-@[simp] theorem getElem_finRange {i : Nat} (h : i < (List.finRange n).length) :
+@[simp, grind =] theorem getElem_finRange {i : Nat} (h : i < (List.finRange n).length) :
     (finRange n)[i] = Fin.cast length_finRange ⟨i, h⟩ := by
   simp [List.finRange]
 
-@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange]
+@[simp, grind =] theorem finRange_zero : finRange 0 = [] := by simp [finRange]
 
 theorem finRange_succ {n} : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
   apply List.ext_getElem; simp; intro i; cases i <;> simp
@@ -46,6 +46,7 @@ theorem finRange_succ_last {n} :
     · rfl
     · next h => exact Fin.eq_last_of_not_lt h
 
+@[grind _=_]
 theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev := by
   induction n with
   | zero => simp

src/Init/Data/Vector/FinRange.lean

@@ -17,7 +17,7 @@ namespace Vector
 /-- `finRange n` is the vector of all elements of `Fin n` in order. -/
 protected def finRange (n : Nat) : Vector (Fin n) n := ofFn fun i => i
 
-@[simp] theorem getElem_finRange {i : Nat} (h : i < n) :
+@[simp, grind =] theorem getElem_finRange {i : Nat} (h : i < n) :
     (Vector.finRange n)[i] = ⟨i, h⟩ := by
   simp [Vector.finRange]
 
@@ -39,6 +39,7 @@ theorem finRange_succ_last {n} :
     · simp_all
       omega
 
+@[grind _=_]
 theorem finRange_reverse {n} : (Vector.finRange n).reverse = (Vector.finRange n).map Fin.rev := by
   ext i h
   simp