more

Author: kim-em

src/Init/Data/Array/Lemmas.lean

@@ -4539,7 +4539,7 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a 
     (zip xs ys).size = min xs.size ys.size :=
   size_zipWith
 
-@[simp] theorem getElem_zipWith {xs : Array α} {ys : Array β} {f : α → β → γ} {i : Nat}
+@[simp, grind =] theorem getElem_zipWith {xs : Array α} {ys : Array β} {f : α → β → γ} {i : Nat}
     (hi : i < (zipWith f xs ys).size) :
     (zipWith f xs ys)[i] = f (xs[i]'(by simp at hi; omega)) (ys[i]'(by simp at hi; omega)) := by
   cases xs

src/Init/Data/Array/MapIdx.lean

@@ -126,7 +126,7 @@ namespace Array
 
 /-! ### zipIdx -/
 
-@[simp] theorem getElem_zipIdx {xs : Array α} {k : Nat} {i : Nat} (h : i < (xs.zipIdx k).size) :
+@[simp, grind =] theorem getElem_zipIdx {xs : Array α} {k : Nat} {i : Nat} (h : i < (xs.zipIdx k).size) :
     (xs.zipIdx k)[i] = (xs[i]'(by simp_all), k + i) := by
   simp [zipIdx]
 
@@ -140,7 +140,7 @@ abbrev getElem_zipWithIndex := @getElem_zipIdx
 @[deprecated zipIdx_toArray (since := "2025-01-21")]
 abbrev zipWithIndex_toArray := @zipIdx_toArray
 
-@[simp] theorem toList_zipIdx {xs : Array α} {k : Nat} :
+@[simp, grind =] theorem toList_zipIdx {xs : Array α} {k : Nat} :
     (xs.zipIdx k).toList = xs.toList.zipIdx k := by
   rcases xs with ⟨xs⟩
   simp

src/Init/Data/List/Range.lean

@@ -225,7 +225,7 @@ theorem zipIdx_eq_nil_iff {l : List α} {i : Nat} : List.zipIdx l i = [] ↔ l =
   | [], _ => rfl
   | _ :: _, _ => congrArg Nat.succ length_zipIdx
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_zipIdx :
     ∀ {l : List α} {i j}, (zipIdx l i)[j]? = l[j]?.map fun a => (a, i + j)
   | [], _, _ => rfl
@@ -234,15 +234,15 @@ theorem getElem?_zipIdx :
     simp only [zipIdx_cons, getElem?_cons_succ]
     exact getElem?_zipIdx.trans <| by rw [Nat.add_right_comm]; rfl
 
-@[simp]
+@[simp, grind =]
 theorem getElem_zipIdx {l : List α} (h : i < (l.zipIdx j).length) :
     (l.zipIdx j)[i] = (l[i]'(by simpa [length_zipIdx] using h), j + i) := by
   simp only [length_zipIdx] at h
   rw [getElem_eq_getElem?_get]
   simp only [getElem?_zipIdx, getElem?_eq_getElem h]
   simp
 
-@[simp]
+@[simp, grind =]
 theorem tail_zipIdx {l : List α} {i : Nat} : (zipIdx l i).tail = zipIdx l.tail (i + 1) := by
   induction l generalizing i with
   | nil => simp

src/Init/Data/Vector/Lemmas.lean

@@ -3076,7 +3076,7 @@ theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
 
 /-! ### zipWith -/
 
-@[simp] theorem getElem_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} {i : Nat}
+@[simp, grind =] theorem getElem_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} {i : Nat}
     (hi : i < n) : (zipWith f as bs)[i] = f as[i] bs[i] := by
   cases as
   cases bs

src/Init/Data/Vector/MapIdx.lean

@@ -61,12 +61,12 @@ namespace Vector
 
 /-! ### zipIdx -/
 
-@[simp] theorem toList_zipIdx {xs : Vector α n} (k : Nat := 0) :
+@[simp, grind =] theorem toList_zipIdx {xs : Vector α n} (k : Nat := 0) :
     (xs.zipIdx k).toList = xs.toList.zipIdx k := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem getElem_zipIdx {xs : Vector α n} {i : Nat} {h : i < n} :
+@[simp, grind =] theorem getElem_zipIdx {xs : Vector α n} {i : Nat} {h : i < n} :
     (xs.zipIdx k)[i] = (xs[i]'(by simp_all), k + i) := by
   rcases xs with ⟨xs, rfl⟩
   simp