more

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/Array/Zip.lean

@@ -45,6 +45,7 @@ theorem zipWith_self {f : α → α → δ} {xs : Array α} : zipWith f xs xs =
 See also `getElem?_zipWith'` for a variant
 using `Option.map` and `Option.bind` rather than a `match`.
 -/
+@[grind =]
 theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
     (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
       | some a, some b => some (f a b) | _, _ => none := by
@@ -76,31 +77,35 @@ theorem getElem?_zip_eq_some {as : Array α} {bs : Array β} {z : α × β} {i :
   · rintro ⟨h₀, h₁⟩
     exact ⟨_, _, h₀, h₁, rfl⟩
 
-@[simp]
+@[simp, grind =]
 theorem zipWith_map {μ} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {as : Array α} {bs : Array β} :
     zipWith f (as.map g) (bs.map h) = zipWith (fun a b => f (g a) (h b)) as bs := by
   cases as
   cases bs
   simp [List.zipWith_map]
 
+@[grind =]
 theorem zipWith_map_left {as : Array α} {bs : Array β} {f : α → α'} {g : α' → β → γ} :
     zipWith g (as.map f) bs = zipWith (fun a b => g (f a) b) as bs := by
   cases as
   cases bs
   simp [List.zipWith_map_left]
 
+@[grind =]
 theorem zipWith_map_right {as : Array α} {bs : Array β} {f : β → β'} {g : α → β' → γ} :
     zipWith g as (bs.map f) = zipWith (fun a b => g a (f b)) as bs := by
   cases as
   cases bs
   simp [List.zipWith_map_right]
 
+@[grind =]
 theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} {i : δ} :
     (zipWith f as bs).foldr g i = (zip as bs).foldr (fun p r => g (f p.1 p.2) r) i := by
   cases as
   cases bs
   simp [List.zipWith_foldr_eq_zip_foldr]
 
+@[grind =]
 theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} {i : δ} :
     (zipWith f as bs).foldl g i = (zip as bs).foldl (fun r p => g r (f p.1 p.2)) i := by
   cases as
@@ -111,22 +116,26 @@ theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} {i : δ} :
 theorem zipWith_eq_empty_iff {f : α → β → γ} {as : Array α} {bs : Array β} : zipWith f as bs = #[] ↔ as = #[] ∨ bs = #[] := by
   cases as <;> cases bs <;> simp
 
+@[grind =]
 theorem map_zipWith {δ : Type _} {f : α → β} {g : γ → δ → α} {cs : Array γ} {ds : Array δ} :
     map f (zipWith g cs ds) = zipWith (fun x y => f (g x y)) cs ds := by
   cases cs
   cases ds
   simp [List.map_zipWith]
 
+@[grind =]
 theorem take_zipWith : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i) := by
   cases as
   cases bs
   simp [List.take_zipWith]
 
+@[grind =]
 theorem extract_zipWith : (zipWith f as bs).extract i j = zipWith f (as.extract i j) (bs.extract i j) := by
   cases as
   cases bs
   simp [List.drop_zipWith, List.take_zipWith]
 
+@[grind =]
 theorem zipWith_append {f : α → β → γ} {as as' : Array α} {bs bs' : Array β}
     (h : as.size = bs.size) :
     zipWith f (as ++ as') (bs ++ bs') = zipWith f as bs ++ zipWith f as' bs' := by
@@ -152,7 +161,7 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Array α} {bs : Array
   · rintro ⟨⟨ws⟩, ⟨xs⟩, ⟨ys⟩, ⟨zs⟩, h, rfl, rfl, h₁, h₂⟩
     exact ⟨ws, xs, ys, zs, by simp_all⟩
 
-@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
+@[simp, grind =] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
     zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
   simp [← List.toArray_replicate]
 
@@ -184,6 +193,7 @@ theorem zipWith_eq_zipWith_take_min (as : Array α) (bs : Array β) :
   simp
   rw [List.zipWith_eq_zipWith_take_min]
 
+@[grind =]
 theorem reverse_zipWith (h : as.size = bs.size) :
     (zipWith f as bs).reverse = zipWith f as.reverse bs.reverse := by
   cases as
@@ -200,7 +210,7 @@ theorem lt_size_right_of_zip {i : Nat} {as : Array α} {bs : Array β} (h : i <
     i < bs.size :=
   lt_size_right_of_zipWith h
 
-@[simp]
+@[simp, grind =]
 theorem getElem_zip {as : Array α} {bs : Array β} {i : Nat} {h : i < (zip as bs).size} :
     (zip as bs)[i] =
       (as[i]'(lt_size_left_of_zip h), bs[i]'(lt_size_right_of_zip h)) :=
@@ -211,18 +221,22 @@ theorem zip_eq_zipWith {as : Array α} {bs : Array β} : zip as bs = zipWith Pro
   cases bs
   simp [List.zip_eq_zipWith]
 
+@[grind _=_]
 theorem zip_map {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β} :
     zip (as.map f) (bs.map g) = (zip as bs).map (Prod.map f g) := by
   cases as
   cases bs
   simp [List.zip_map]
 
+@[grind _=_]
 theorem zip_map_left {f : α → γ} {as : Array α} {bs : Array β} :
     zip (as.map f) bs = (zip as bs).map (Prod.map f id) := by rw [← zip_map, map_id]
 
+@[grind _=_]
 theorem zip_map_right {f : β → γ} {as : Array α} {bs : Array β} :
     zip as (bs.map f) = (zip as bs).map (Prod.map id f) := by rw [← zip_map, map_id]
 
+@[grind =]
 theorem zip_append {as bs : Array α} {cs ds : Array β} (_h : as.size = cs.size) :
     zip (as ++ bs) (cs ++ ds) = zip as cs ++ zip bs ds := by
   cases as
@@ -231,6 +245,7 @@ theorem zip_append {as bs : Array α} {cs ds : Array β} (_h : as.size = cs.size
   cases ds
   simp_all [List.zip_append]
 
+@[grind =]
 theorem zip_map' {f : α → β} {g : α → γ} {xs : Array α} :
     zip (xs.map f) (xs.map g) = xs.map fun a => (f a, g a) := by
   cases xs
@@ -276,7 +291,7 @@ theorem zip_eq_append_iff {as : Array α} {bs : Array β} :
       ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
   simp [zip_eq_zipWith, zipWith_eq_append_iff]
 
-@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
+@[simp, grind =] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
     zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
   simp [← List.toArray_replicate]
 
@@ -293,6 +308,7 @@ theorem zip_eq_zip_take_min {as : Array α} {bs : Array β} :
 
 /-! ### zipWithAll -/
 
+@[grind =]
 theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
     (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
       | none, none => .none | a?, b? => some (f a? b?) := by
@@ -301,31 +317,35 @@ theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
   simp [List.getElem?_zipWithAll]
   rfl
 
+@[grind =]
 theorem zipWithAll_map {μ} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {as : Array α} {bs : Array β} :
     zipWithAll f (as.map g) (bs.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) as bs := by
   cases as
   cases bs
   simp [List.zipWithAll_map]
 
+@[grind =]
 theorem zipWithAll_map_left {as : Array α} {bs : Array β} {f : α → α'} {g : Option α' → Option β → γ} :
     zipWithAll g (as.map f) bs = zipWithAll (fun a b => g (f <$> a) b) as bs := by
   cases as
   cases bs
   simp [List.zipWithAll_map_left]
 
+@[grind =]
 theorem zipWithAll_map_right {as : Array α} {bs : Array β} {f : β → β'} {g : Option α → Option β' → γ} :
     zipWithAll g as (bs.map f) = zipWithAll (fun a b => g a (f <$> b)) as bs := by
   cases as
   cases bs
   simp [List.zipWithAll_map_right]
 
+@[grind =]
 theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option δ → α} {cs : Array γ} {ds : Array δ} :
     map f (zipWithAll g cs ds) = zipWithAll (fun x y => f (g x y)) cs ds := by
   cases cs
   cases ds
   simp [List.map_zipWithAll]
 
-@[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
+@[simp, grind =] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
     zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b)) := by
   simp [← List.toArray_replicate]
 
@@ -342,6 +362,7 @@ theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
 theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
   simp
 
+@[grind =]
 theorem unzip_eq_map {xs : Array (α × β)} : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by
   cases xs
   simp [List.unzip_eq_map]
@@ -375,9 +396,11 @@ theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
   rw [← hl, ← hr, ← zip_unzip xs, ← fst_unzip, ← snd_unzip, zip_unzip, zip_unzip]
 
-@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
+@[simp, grind =] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp
 
 @[deprecated unzip_replicate (since := "2025-03-18")]
 abbrev unzip_mkArray := @unzip_replicate
+
+end Array

src/Init/Data/List/Nat/TakeDrop.lean

@@ -538,7 +538,7 @@ theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
 
 /-! ### zipWith -/
 
-@[simp] theorem length_zipWith {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
+@[simp, grind =] theorem length_zipWith {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
     length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
   induction l₁ generalizing l₂ <;> cases l₂ <;>
     simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
@@ -549,7 +549,7 @@ theorem lt_length_left_of_zipWith {f : α → β → γ} {i : Nat} {l : List α}
 theorem lt_length_right_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
     (h : i < (zipWith f l l').length) : i < l'.length := by rw [length_zipWith] at h; omega
 
-@[simp]
+@[simp, grind =]
 theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β}
     {i : Nat} {h : i < (zipWith f l l').length} :
     (zipWith f l l')[i] =
@@ -566,6 +566,7 @@ theorem zipWith_eq_zipWith_take_min : ∀ {l₁ : List α} {l₂ : List β},
   | _, [] => by simp
   | a :: l₁, b :: l₂ => by simp [succ_min_succ, zipWith_eq_zipWith_take_min (l₁ := l₁) (l₂ := l₂)]
 
+@[grind =]
 theorem reverse_zipWith (h : l.length = l'.length) :
     (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by
   induction l generalizing l' with
@@ -578,14 +579,14 @@ theorem reverse_zipWith (h : l.length = l'.length) :
       have : tl.reverse.length = tl'.reverse.length := by simp [h]
       simp [hl h, zipWith_append this]
 
-@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
+@[simp, grind =] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
     zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
   rw [zipWith_eq_zipWith_take_min]
   simp
 
 /-! ### zip -/
 
-@[simp] theorem length_zip {l₁ : List α} {l₂ : List β} :
+@[simp, grind =] theorem length_zip {l₁ : List α} {l₂ : List β} :
     length (zip l₁ l₂) = min (length l₁) (length l₂) := by
   simp [zip]
 
@@ -597,7 +598,7 @@ theorem lt_length_right_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (
     i < l'.length :=
   lt_length_right_of_zipWith h
 
-@[simp]
+@[simp, grind =]
 theorem getElem_zip {l : List α} {l' : List β} {i : Nat} {h : i < (zip l l').length} :
     (zip l l')[i] =
       (l[i]'(lt_length_left_of_zip h), l'[i]'(lt_length_right_of_zip h)) :=
@@ -609,7 +610,7 @@ theorem zip_eq_zip_take_min : ∀ {l₁ : List α} {l₂ : List β},
   | _, [] => by simp
   | a :: l₁, b :: l₂ => by simp [succ_min_succ, zip_eq_zip_take_min (l₁ := l₁) (l₂ := l₂)]
 
-@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
+@[simp, grind =] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
     zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
   rw [zip_eq_zip_take_min]
   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,7 +234,7 @@ 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
@@ -242,7 +242,7 @@ theorem getElem_zipIdx {l : List α} (h : i < (l.zipIdx j).length) :
   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/List/Zip.lean

@@ -46,6 +46,7 @@ theorem zipWith_self {f : α → α → δ} : ∀ {l : List α}, zipWith f l l =
 See also `getElem?_zipWith'` for a variant
 using `Option.map` and `Option.bind` rather than a `match`.
 -/
+@[grind =]
 theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
     (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
       | some a, some b => some (f a b) | _, _ => none := by
@@ -83,33 +84,39 @@ theorem getElem?_zip_eq_some {l₁ : List α} {l₂ : List β} {z : α × β} {i
   · rintro ⟨h₀, h₁⟩
     exact ⟨_, _, h₀, h₁, rfl⟩
 
+@[grind =]
 theorem head?_zipWith {f : α → β → γ} :
     (List.zipWith f as bs).head? = match as.head?, bs.head? with
       | some a, some b => some (f a b) | _, _ => none := by
   simp [head?_eq_getElem?, getElem?_zipWith]
 
+@[grind =]
 theorem head_zipWith {f : α → β → γ} (h):
     (List.zipWith f as bs).head h = f (as.head (by rintro rfl; simp_all)) (bs.head (by rintro rfl; simp_all)) := by
   apply Option.some.inj
   rw [← head?_eq_head, head?_zipWith, head?_eq_head, head?_eq_head]
 
-@[simp]
+@[simp, grind =]
 theorem zipWith_map {μ} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
     zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem zipWith_map_left {l₁ : List α} {l₂ : List β} {f : α → α'} {g : α' → β → γ} :
     zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem zipWith_map_right {l₁ : List α} {l₂ : List β} {f : β → β'} {g : α → β' → γ} :
     zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} {i : δ} {g : γ → δ → δ} :
     (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} {i : δ} {g : δ → γ → δ} :
     (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by
   induction l₁ generalizing i l₂ <;> cases l₂ <;> simp_all
@@ -118,6 +125,7 @@ theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} {i : δ} {g : δ →
 theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = [] := by
   cases l <;> cases l' <;> simp
 
+@[grind =]
 theorem map_zipWith {δ : Type _} {f : α → β} {g : γ → δ → α} {l : List γ} {l' : List δ} :
     map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
   induction l generalizing l' with
@@ -127,6 +135,7 @@ theorem map_zipWith {δ : Type _} {f : α → β} {g : γ → δ → α} {l : Li
       · simp
       · simp [hl]
 
+@[grind =]
 theorem take_zipWith : (zipWith f l l').take i = zipWith f (l.take i) (l'.take i) := by
   induction l generalizing l' i with
   | nil => simp
@@ -137,6 +146,7 @@ theorem take_zipWith : (zipWith f l l').take i = zipWith f (l.take i) (l'.take i
       · simp
       · simp [hl]
 
+@[grind =]
 theorem drop_zipWith : (zipWith f l l').drop i = zipWith f (l.drop i) (l'.drop i) := by
   induction l generalizing l' i with
   | nil => simp
@@ -147,10 +157,11 @@ theorem drop_zipWith : (zipWith f l l').drop i = zipWith f (l.drop i) (l'.drop i
         · simp
         · simp [hl]
 
-@[simp]
+@[simp, grind =]
 theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
   rw [← drop_one]; simp [drop_zipWith]
 
+@[grind =]
 theorem zipWith_append {f : α → β → γ} {l₁ l₁' : List α} {l₂ l₂' : List β}
     (h : l₁.length = l₂.length) :
     zipWith f (l₁ ++ l₁') (l₂ ++ l₂') = zipWith f l₁ l₂ ++ zipWith f l₁' l₂' := by
@@ -254,22 +265,26 @@ theorem zip_eq_zipWith : ∀ {l₁ : List α} {l₂ : List β}, zip l₁ l₂ =
   | _, [] => rfl
   | a :: l₁, b :: l₂ => by simp [zip_cons_cons, zip_eq_zipWith (l₁ := l₁)]
 
+@[grind _=_]
 theorem zip_map {f : α → γ} {g : β → δ} :
     ∀ {l₁ : List α} {l₂ : List β}, zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
   | [], _ => rfl
   | _, [] => by simp only [map, zip_nil_right]
   | _ :: _, _ :: _ => by simp only [map, zip_cons_cons, zip_map, Prod.map]
 
+@[grind _=_]
 theorem zip_map_left {f : α → γ} {l₁ : List α} {l₂ : List β} :
     zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
 
+@[grind _=_]
 theorem zip_map_right {f : β → γ} {l₁ : List α} {l₂ : List β} :
     zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
 
-@[simp] theorem tail_zip {l₁ : List α} {l₂ : List β} :
+@[simp, grind =] theorem tail_zip {l₁ : List α} {l₂ : List β} :
     (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
   cases l₁ <;> cases l₂ <;> simp
 
+@[grind =]
 theorem zip_append :
     ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
       zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
@@ -278,6 +293,7 @@ theorem zip_append :
   | _ :: _, _, _ :: _, _, h => by
     simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
 
+@[grind =]
 theorem zip_map' {f : α → β} {g : α → γ} :
     ∀ {l : List α}, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
   | [] => rfl
@@ -353,6 +369,7 @@ theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
 
 /-! ### zipWithAll -/
 
+@[grind =]
 theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
     (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
       | none, none => .none | a?, b? => some (f a? b?) := by
@@ -366,33 +383,38 @@ theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
       cases i <;> simp_all
     | cons b bs => cases i <;> simp_all
 
+@[grind =]
 theorem head?_zipWithAll {f : Option α → Option β → γ} :
     (zipWithAll f as bs).head? = match as.head?, bs.head? with
       | none, none => .none | a?, b? => some (f a? b?) := by
   simp [head?_eq_getElem?, getElem?_zipWithAll]
 
-@[simp] theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
+@[simp, grind =] theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
     (zipWithAll f as bs).head h = f as.head? bs.head? := by
   apply Option.some.inj
   rw [← head?_eq_head, head?_zipWithAll]
   split <;> simp_all
 
-@[simp] theorem tail_zipWithAll {f : Option α → Option β → γ} :
+@[simp, grind =] theorem tail_zipWithAll {f : Option α → Option β → γ} :
     (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail := by
   cases as <;> cases bs <;> simp
 
+@[grind =]
 theorem zipWithAll_map {μ} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
     zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem zipWithAll_map_left {l₁ : List α} {l₂ : List β} {f : α → α'} {g : Option α' → Option β → γ} :
     zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem zipWithAll_map_right {l₁ : List α} {l₂ : List β} {f : β → β'} {g : Option α → Option β' → γ} :
     zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂ := by
   induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
 
+@[grind =]
 theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option δ → α} {l : List γ} {l' : List δ} :
     map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l' := by
   induction l generalizing l' with
@@ -400,7 +422,7 @@ theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option
   | cons hd tl hl =>
     cases l' <;> simp_all
 
-@[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
+@[simp, grind =] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
     zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b)) := by
   induction n with
   | zero => rfl
@@ -408,12 +430,13 @@ theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option
 
 /-! ### unzip -/
 
-@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
+@[simp, grind =] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
   induction l <;> simp_all
 
-@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
+@[simp, grind =] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
   induction l <;> simp_all
 
+@[grind =]
 theorem unzip_eq_map : ∀ {l : List (α × β)}, unzip l = (l.map Prod.fst, l.map Prod.snd)
   | [] => rfl
   | (a, b) :: l => by simp only [unzip_cons, map_cons, unzip_eq_map (l := l)]
@@ -453,6 +476,6 @@ theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 :=
 theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by
   simp
 
-@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
+@[simp, grind =] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> 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

src/Init/Data/Vector/Zip.lean

@@ -46,6 +46,7 @@ theorem zipWith_self {f : α → α → δ} {xs : Vector α n} : zipWith f xs xs
 See also `getElem?_zipWith'` for a variant
 using `Option.map` and `Option.bind` rather than a `match`.
 -/
+@[grind =]
 theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
     (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
       | some a, some b => some (f a b) | _, _ => none := by
@@ -74,53 +75,61 @@ theorem getElem?_zip_eq_some {as : Vector α n} {bs : Vector β n} {z : α × β
   rcases bs with ⟨bs, h⟩
   simp [Array.getElem?_zip_eq_some]
 
-@[simp]
+@[simp, grind =]
 theorem zipWith_map {μ} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {as : Vector α n} {bs : Vector β n} :
     zipWith f (as.map g) (bs.map h) = zipWith (fun a b => f (g a) (h b)) as bs := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.zipWith_map]
 
+@[grind =]
 theorem zipWith_map_left {as : Vector α n} {bs : Vector β n} {f : α → α'} {g : α' → β → γ} :
     zipWith g (as.map f) bs = zipWith (fun a b => g (f a) b) as bs := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.zipWith_map_left]
 
+@[grind =]
 theorem zipWith_map_right {as : Vector α n} {bs : Vector β n} {f : β → β'} {g : α → β' → γ} :
     zipWith g as (bs.map f) = zipWith (fun a b => g a (f b)) as bs := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.zipWith_map_right]
 
+@[grind =]
 theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} {i : δ} :
     (zipWith f as bs).foldr g i = (zip as bs).foldr (fun p r => g (f p.1 p.2) r) i := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simpa using Array.zipWith_foldr_eq_zip_foldr
 
+@[grind =]
 theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} {i : δ} :
     (zipWith f as bs).foldl g i = (zip as bs).foldl (fun r p => g r (f p.1 p.2)) i := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simpa using Array.zipWith_foldl_eq_zip_foldl
 
+@[grind =]
 theorem map_zipWith {δ : Type _} {f : α → β} {g : γ → δ → α} {as : Vector γ n} {bs : Vector δ n} :
     map f (zipWith g as bs) = zipWith (fun x y => f (g x y)) as bs := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.map_zipWith]
 
+@[grind =]
 theorem take_zipWith : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i) := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.take_zipWith]
 
+@[grind =]
 theorem extract_zipWith : (zipWith f as bs).extract i j = zipWith f (as.extract i j) (bs.extract i j) := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.extract_zipWith]
 
+@[grind =]
 theorem zipWith_append {f : α → β → γ}
     {as : Vector α n} {as' : Vector α m} {bs : Vector β n} {bs' : Vector β m} :
     zipWith f (as ++ as') (bs ++ bs') = zipWith f as bs ++ zipWith f as' bs' := by
@@ -147,7 +156,8 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Vector α (n + m)} {b
     simp only at w₁ w₂
     exact ⟨as₁, as₂, bs₁, bs₂, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩
 
-@[simp] theorem zipWith_replicate {a : α} {b : β} {n : Nat} :
+@[simp, grind =]
+theorem zipWith_replicate {a : α} {b : β} {n : Nat} :
     zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
   ext
   simp
@@ -167,6 +177,7 @@ theorem map_zip_eq_zipWith {f : α × β → γ} {as : Vector α n} {bs : Vector
   rcases bs with ⟨bs, h⟩
   simp [Array.map_zip_eq_zipWith]
 
+@[grind =]
 theorem reverse_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} :
     (zipWith f as bs).reverse = zipWith f as.reverse bs.reverse := by
   rcases as with ⟨as, rfl⟩
@@ -175,7 +186,7 @@ theorem reverse_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector
 
 /-! ### zip -/
 
-@[simp]
+@[simp, grind =]
 theorem getElem_zip {as : Vector α n} {bs : Vector β n} {i : Nat} {h : i < n} :
     (zip as bs)[i] = (as[i], bs[i]) :=
   getElem_zipWith ..
@@ -185,18 +196,22 @@ theorem zip_eq_zipWith {as : Vector α n} {bs : Vector β n} : zip as bs = zipWi
   rcases bs with ⟨bs, h⟩
   simp [Array.zip_eq_zipWith, h]
 
+@[grind _=_]
 theorem zip_map {f : α → γ} {g : β → δ} {as : Vector α n} {bs : Vector β n} :
     zip (as.map f) (bs.map g) = (zip as bs).map (Prod.map f g) := by
   rcases as with ⟨as, rfl⟩
   rcases bs with ⟨bs, h⟩
   simp [Array.zip_map, h]
 
+@[grind _=_]
 theorem zip_map_left {f : α → γ} {as : Vector α n} {bs : Vector β n} :
     zip (as.map f) bs = (zip as bs).map (Prod.map f id) := by rw [← zip_map, map_id]
 
+@[grind _=_]
 theorem zip_map_right {f : β → γ} {as : Vector α n} {bs : Vector β n} :
     zip as (bs.map f) = (zip as bs).map (Prod.map id f) := by rw [← zip_map, map_id]
 
+@[grind =]
 theorem zip_append {as : Vector α n} {bs : Vector β n} {as' : Vector α m} {bs' : Vector β m} :
     zip (as ++ as') (bs ++ bs') = zip as bs ++ zip as' bs' := by
   rcases as with ⟨as, rfl⟩
@@ -205,6 +220,7 @@ theorem zip_append {as : Vector α n} {bs : Vector β n} {as' : Vector α m} {bs
   rcases bs' with ⟨bs', h'⟩
   simp [Array.zip_append, h, h']
 
+@[grind =]
 theorem zip_map' {f : α → β} {g : α → γ} {xs : Vector α n} :
     zip (xs.map f) (xs.map g) = xs.map fun a => (f a, g a) := by
   rcases xs with ⟨xs, rfl⟩
@@ -248,7 +264,8 @@ theorem zip_eq_append_iff {as : Vector α (n + m)} {bs : Vector β (n + m)} {xs
       ∃ as₁ as₂ bs₁ bs₂, as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zip as₁ bs₁ ∧ ys = zip as₂ bs₂ := by
   simp [zip_eq_zipWith, zipWith_eq_append_iff]
 
-@[simp] theorem zip_replicate {a : α} {b : β} {n : Nat} :
+@[simp, grind =]
+theorem zip_replicate {a : α} {b : β} {n : Nat} :
     zip (replicate n a) (replicate n b) = replicate n (a, b) := by
   ext <;> simp
 
@@ -257,14 +274,17 @@ abbrev zip_mkVector := @zip_replicate
 
 /-! ### unzip -/
 
-@[simp] theorem unzip_fst : (unzip xs).fst = xs.map Prod.fst := by
+@[simp, grind =]
+theorem unzip_fst : (unzip xs).fst = xs.map Prod.fst := by
   cases xs
   simp_all
 
-@[simp] theorem unzip_snd : (unzip xs).snd = xs.map Prod.snd := by
+@[simp, grind =]
+theorem unzip_snd : (unzip xs).snd = xs.map Prod.snd := by
   cases xs
   simp_all
 
+@[grind =]
 theorem unzip_eq_map {xs : Vector (α × β) n} : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by
   cases xs
   simp [List.unzip_eq_map]
@@ -296,7 +316,8 @@ theorem zip_of_prod {as : Vector α n} {bs : Vector β n} {xs : Vector (α × β
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
   rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem unzip_replicate {a : α} {b : β} {n : Nat} :
+@[simp, grind =]
+theorem unzip_replicate {a : α} {b : β} {n : Nat} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp