chore: remove grind annotations of List/Array/Vector.zip_map_left/right

src/Init/Data/Array/Zip.lean

@@ -231,11 +231,9 @@ theorem zip_map {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β}
   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]
 

src/Init/Data/List/Zip.lean

@@ -274,11 +274,9 @@ theorem zip_map {f : α → γ} {g : β → δ} :
   | _, [] => 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]
 

src/Init/Data/Vector/Zip.lean

@@ -207,11 +207,9 @@ theorem zip_map {f : α → γ} {g : β → δ} {as : Vector α n} {bs : Vector
   rcases bs with ⟨bs, h⟩
   simp [Array.zip_map]
 
-@[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]