fix test

src/Init/Data/Array.lean

@@ -23,3 +23,4 @@ import Init.Data.Array.FinRange
 import Init.Data.Array.Perm
 import Init.Data.Array.Find
 import Init.Data.Array.Lex
+import Init.Data.Array.Zip

src/Init/Data/Array/Basic.lean

@@ -941,13 +941,13 @@ def zipWithAux (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat)
     cs
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-@[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
+@[inline] def zipWith (f : α → β → γ) (as : Array α) (bs : Array β) : Array γ :=
   zipWithAux as bs f 0 #[]
 
 def zip (as : Array α) (bs : Array β) : Array (α × β) :=
-  zipWith as bs Prod.mk
+  zipWith Prod.mk as bs
 
-def zipWithAll (as : Array α) (bs : Array β) (f : Option α → Option β → γ) : Array γ :=
+def zipWithAll (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : Array γ :=
   go as bs 0 #[]
 where go (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :=
   if i < max as.size bs.size then

src/Init/Data/Array/Lemmas.lean

@@ -3543,23 +3543,23 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size)
 /-! ### zipWith -/
 
 @[simp] theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (Array.zipWith as bs f).toList = List.zipWith f as.toList bs.toList := by
+    (zipWith f as bs).toList = List.zipWith f as.toList bs.toList := by
   cases as
   cases bs
   simp
 
 @[simp] theorem toList_zip (as : Array α) (bs : Array β) :
-    (Array.zip as bs).toList = List.zip as.toList bs.toList := by
+    (zip as bs).toList = List.zip as.toList bs.toList := by
   simp [zip, toList_zipWith, List.zip]
 
 @[simp] theorem toList_zipWithAll (f : Option α → Option β → γ) (as : Array α) (bs : Array β) :
-    (Array.zipWithAll as bs f).toList = List.zipWithAll f as.toList bs.toList := by
+    (zipWithAll f as bs).toList = List.zipWithAll f as.toList bs.toList := by
   cases as
   cases bs
   simp
 
 @[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
-    (as.zipWith bs f).size = min as.size bs.size := by
+    (zipWith f as bs).size = min as.size bs.size := by
   rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
 @[simp] theorem size_zip (as : Array α) (bs : Array β) :
@@ -3567,8 +3567,8 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size)
   as.size_zipWith bs Prod.mk
 
 @[simp] theorem getElem_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat)
-    (hi : i < (as.zipWith bs f).size) :
-    (as.zipWith bs f)[i] = f (as[i]'(by simp at hi; omega)) (bs[i]'(by simp at hi; omega)) := by
+    (hi : i < (zipWith f as bs).size) :
+    (zipWith f as bs)[i] = f (as[i]'(by simp at hi; omega)) (bs[i]'(by simp at hi; omega)) := by
   cases as
   cases bs
   simp

src/Init/Data/Array/Zip.lean

@@ -0,0 +1,363 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.TakeDrop
+import Init.Data.List.Zip
+
+/-!
+# Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`.
+-/
+
+namespace Array
+
+open Nat
+
+/-! ## Zippers -/
+
+/-! ### zipWith -/
+
+theorem zipWith_comm (f : α → β → γ) (la : Array α) (lb : Array β) :
+    zipWith f la lb = zipWith (fun b a => f a b) lb la := by
+  cases la
+  cases lb
+  simpa using List.zipWith_comm _ _ _
+
+theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Array α) :
+    zipWith f l l' = zipWith f l' l := by
+  rw [zipWith_comm]
+  simp only [comm]
+
+@[simp]
+theorem zipWith_self (f : α → α → δ) (l : Array α) : zipWith f l l = l.map fun a => f a a := by
+  cases l
+  simp
+
+/--
+See also `getElem?_zipWith'` for a variant
+using `Option.map` and `Option.bind` rather than a `match`.
+-/
+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
+  cases as
+  cases bs
+  simp [List.getElem?_zipWith]
+  rfl
+
+/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/
+theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
+    (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by
+  cases l₁
+  cases l₂
+  simp [List.getElem?_zipWith']
+
+theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} {z : γ} {i : Nat} :
+    (zipWith f l₁ l₂)[i]? = some z ↔
+      ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by
+  cases l₁
+  cases l₂
+  simp [List.getElem?_zipWith_eq_some]
+
+theorem getElem?_zip_eq_some {l₁ : Array α} {l₂ : Array β} {z : α × β} {i : Nat} :
+    (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by
+  cases z
+  rw [zip, getElem?_zipWith_eq_some]; constructor
+  · rintro ⟨x, y, h₀, h₁, h₂⟩
+    simpa [h₀, h₁] using h₂
+  · rintro ⟨h₀, h₁⟩
+    exact ⟨_, _, h₀, h₁, rfl⟩
+
+@[simp]
+theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : Array α) (l₂ : Array β) :
+    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zipWith_map]
+
+theorem zipWith_map_left (l₁ : Array α) (l₂ : Array β) (f : α → α') (g : α' → β → γ) :
+    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zipWith_map_left]
+
+theorem zipWith_map_right (l₁ : Array α) (l₂ : Array β) (f : β → β') (g : α → β' → γ) :
+    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zipWith_map_right]
+
+theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
+    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by
+  cases l₁
+  cases l₂
+  simp [List.zipWith_foldr_eq_zip_foldr]
+
+theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
+    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by
+  cases l₁
+  cases l₂
+  simp [List.zipWith_foldl_eq_zip_foldl]
+
+@[simp]
+theorem zipWith_eq_empty_iff {f : α → β → γ} {l l'} : zipWith f l l' = #[] ↔ l = #[] ∨ l' = #[] := by
+  cases l <;> cases l' <;> simp
+
+theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Array γ) (l' : Array δ) :
+    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
+  cases l
+  cases l'
+  simp [List.map_zipWith]
+
+theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
+  cases l
+  cases l'
+  simp [List.take_zipWith]
+
+theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n) := by
+  cases l
+  cases l'
+  simp [List.drop_zipWith, List.take_zipWith]
+
+theorem zipWith_append (f : α → β → γ) (l la : Array α) (l' lb : Array β)
+    (h : l.size = l'.size) :
+    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
+  cases l
+  cases l'
+  cases la
+  cases lb
+  simp at h
+  simp [List.zipWith_append, h]
+
+theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} :
+    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by
+  cases l₁
+  cases l₂
+  cases l₁'
+  cases l₂'
+  simp only [List.zipWith_toArray, List.append_toArray, mk.injEq, List.zipWith_eq_append_iff,
+    toArray_eq_append_iff]
+  constructor
+  · rintro ⟨w, x, y, z, h, rfl, rfl, rfl, rfl⟩
+    exact ⟨w.toArray, x.toArray, y.toArray, z.toArray, by simp [h]⟩
+  · rintro ⟨⟨w⟩, ⟨x⟩, ⟨y⟩, ⟨z⟩, h, rfl, rfl, h₁, h₂⟩
+    exact ⟨w, x, y, z, by simp_all⟩
+
+@[simp] theorem zipWith_mkArray {a : α} {b : β} {m n : Nat} :
+    zipWith f (mkArray m a) (mkArray n b) = mkArray (min m n) (f a b) := by
+  simp [← List.toArray_replicate]
+
+theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Array α) (l' : Array β) :
+    map (Function.uncurry f) (l.zip l') = zipWith f l l' := by
+  cases l
+  cases l'
+  simp [List.map_uncurry_zip_eq_zipWith]
+
+theorem map_zip_eq_zipWith (f : α × β → γ) (l : Array α) (l' : Array β) :
+    map f (l.zip l') = zipWith (Function.curry f) l l' := by
+  cases l
+  cases l'
+  simp [List.map_zip_eq_zipWith]
+
+theorem lt_size_left_of_zipWith {f : α → β → γ} {i : Nat} {l : Array α} {l' : Array β}
+    (h : i < (zipWith f l l').size) : i < l.size := by rw [size_zipWith] at h; omega
+
+theorem lt_size_right_of_zipWith {f : α → β → γ} {i : Nat} {l : Array α} {l' : Array β}
+    (h : i < (zipWith f l l').size) : i < l'.size := by rw [size_zipWith] at h; omega
+
+theorem zipWith_eq_zipWith_take_min (l₁ : Array α) (l₂ : Array β) :
+    zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size)) := by
+  cases l₁
+  cases l₂
+  simp
+  rw [List.zipWith_eq_zipWith_take_min]
+
+theorem reverse_zipWith (h : l.size = l'.size) :
+    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by
+  cases l
+  cases l'
+  simp [List.reverse_zipWith (by simpa using h)]
+
+/-! ### zip -/
+
+theorem lt_size_left_of_zip {i : Nat} {l : Array α} {l' : Array β} (h : i < (zip l l').size) :
+    i < l.size :=
+  lt_size_left_of_zipWith h
+
+theorem lt_size_right_of_zip {i : Nat} {l : Array α} {l' : Array β} (h : i < (zip l l').size) :
+    i < l'.size :=
+  lt_size_right_of_zipWith h
+
+@[simp]
+theorem getElem_zip {l : Array α} {l' : Array β} {i : Nat} {h : i < (zip l l').size} :
+    (zip l l')[i] =
+      (l[i]'(lt_size_left_of_zip h), l'[i]'(lt_size_right_of_zip h)) :=
+  getElem_zipWith (hi := by simpa using h)
+
+theorem zip_eq_zipWith (l₁ : Array α) (l₂ : Array β) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zip_eq_zipWith]
+
+theorem zip_map (f : α → γ) (g : β → δ) (l₁ : Array α) (l₂ : Array β) :
+    zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g) := by
+  cases l₁
+  cases l₂
+  simp [List.zip_map]
+
+theorem zip_map_left (f : α → γ) (l₁ : Array α) (l₂ : Array β) :
+    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
+
+theorem zip_map_right (f : β → γ) (l₁ : Array α) (l₂ : Array β) :
+    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
+
+theorem zip_append {l₁ r₁ : Array α} {l₂ r₂ : Array β} (_h : l₁.size = l₂.size) :
+    zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂ := by
+  cases l₁
+  cases l₂
+  cases r₁
+  cases r₂
+  simp_all [List.zip_append]
+
+theorem zip_map' (f : α → β) (g : α → γ) (l : Array α) :
+    zip (l.map f) (l.map g) = l.map fun a => (f a, g a) := by
+  cases l
+  simp [List.zip_map']
+
+theorem of_mem_zip {a b} {l₁ : Array α} {l₂ : Array β} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂ := by
+  cases l₁
+  cases l₂
+  simpa using List.of_mem_zip
+
+theorem map_fst_zip (l₁ : Array α) (l₂ : Array β) (h : l₁.size ≤ l₂.size) :
+    map Prod.fst (zip l₁ l₂) = l₁ := by
+  cases l₁
+  cases l₂
+  simp_all [List.map_fst_zip]
+
+theorem map_snd_zip (l₁ : Array α) (l₂ : Array β) (h : l₂.size ≤ l₁.size) :
+    map Prod.snd (zip l₁ l₂) = l₂ := by
+  cases l₁
+  cases l₂
+  simp_all [List.map_snd_zip]
+
+theorem map_prod_left_eq_zip {l : Array α} (f : α → β) :
+    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
+  rw [← zip_map']
+  congr
+  simp
+
+theorem map_prod_right_eq_zip {l : Array α} (f : α → β) :
+    (l.map fun x => (f x, x)) = (l.map f).zip l := by
+  rw [← zip_map']
+  congr
+  simp
+
+@[simp] theorem zip_eq_empty_iff {l₁ : Array α} {l₂ : Array β} :
+    zip l₁ l₂ = #[] ↔ l₁ = #[] ∨ l₂ = #[] := by
+  cases l₁
+  cases l₂
+  simp [List.zip_eq_nil_iff]
+
+theorem zip_eq_append_iff {l₁ : Array α} {l₂ : Array β} :
+    zip l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by
+  simp [zip_eq_zipWith, zipWith_eq_append_iff]
+
+@[simp] theorem zip_mkArray {a : α} {b : β} {m n : Nat} :
+    zip (mkArray m a) (mkArray n b) = mkArray (min m n) (a, b) := by
+  simp [← List.toArray_replicate]
+
+theorem zip_eq_zip_take_min (l₁ : Array α) (l₂ : Array β) :
+    zip l₁ l₂ = zip (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size)) := by
+  cases l₁
+  cases l₂
+  simp only [List.zip_toArray, size_toArray, List.take_toArray, mk.injEq]
+  rw [List.zip_eq_zip_take_min]
+
+
+/-! ### zipWithAll -/
+
+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
+  cases as
+  cases bs
+  simp [List.getElem?_zipWithAll]
+  rfl
+
+theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : Array α) (l₂ : Array β) :
+    zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zipWithAll_map]
+
+theorem zipWithAll_map_left (l₁ : Array α) (l₂ : Array β) (f : α → α') (g : Option α' → Option β → γ) :
+    zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zipWithAll_map_left]
+
+theorem zipWithAll_map_right (l₁ : Array α) (l₂ : Array β) (f : β → β') (g : Option α → Option β' → γ) :
+    zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂ := by
+  cases l₁
+  cases l₂
+  simp [List.zipWithAll_map_right]
+
+theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option δ → α) (l : Array γ) (l' : Array δ) :
+    map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l' := by
+  cases l
+  cases l'
+  simp [List.map_zipWithAll]
+
+
+@[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
+    zipWithAll f (mkArray n a) (mkArray n b) = mkArray n (f a b) := by
+  simp [← List.toArray_replicate]
+
+/-! ### unzip -/
+
+@[simp] 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
+  induction l <;> simp_all
+
+theorem unzip_eq_map (l : Array (α × β)) : unzip l = (l.map Prod.fst, l.map Prod.snd) := by
+  cases l
+  simp [List.unzip_eq_map]
+
+theorem zip_unzip (l : Array (α × β)) : zip (unzip l).1 (unzip l).2 = l := by
+  cases l
+  simp only [List.unzip_toArray, Prod.map_fst, Prod.map_snd, List.zip_toArray, List.zip_unzip]
+
+theorem unzip_zip_left {l₁ : Array α} {l₂ : Array β} (h : l₁.size ≤ l₂.size) :
+    (unzip (zip l₁ l₂)).1 = l₁ := by
+  cases l₁
+  cases l₂
+  simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_fst,
+    List.unzip_zip_left]
+
+theorem unzip_zip_right {l₁ : Array α} {l₂ : Array β} (h : l₂.size ≤ l₁.size) :
+    (unzip (zip l₁ l₂)).2 = l₂ := by
+  cases l₁
+  cases l₂
+  simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_snd,
+    List.unzip_zip_right]
+
+theorem unzip_zip {l₁ : Array α} {l₂ : Array β} (h : l₁.size = l₂.size) :
+    unzip (zip l₁ l₂) = (l₁, l₂) := by
+  cases l₁
+  cases l₂
+  simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, List.unzip_zip, Prod.map_apply]
+
+theorem zip_of_prod {l : Array α} {l' : Array β} {lp : Array (α × β)} (hl : lp.map Prod.fst = l)
+    (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
+  rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
+
+@[simp] theorem unzip_mkArray {n : Nat} {a : α} {b : β} :
+    unzip (mkArray n (a, b)) = (mkArray n a, mkArray n b) := by
+  ext1 <;> simp

src/Init/Data/List/ToArray.lean

@@ -312,7 +312,7 @@ theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List
     simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]
 
 @[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
-    Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by
+    Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray := by
   rw [Array.zipWith]
   simp [zipWithAux_toArray_zero]
 
@@ -355,7 +355,7 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O
   decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
-    Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by
+    Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray := by
   simp [Array.zipWithAll, zipWithAll_go_toArray]
 
 @[simp] theorem toArray_appendList (l₁ l₂ : List α) :

src/Init/Data/List/Zip.lean

@@ -31,16 +31,18 @@ theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y
   simp only [comm]
 
 @[simp]
-theorem zipWith_same (f : α → α → δ) : ∀ l : List α, zipWith f l l = l.map fun a => f a a
+theorem zipWith_self (f : α → α → δ) : ∀ l : List α, zipWith f l l = l.map fun a => f a a
   | [] => rfl
-  | _ :: xs => congrArg _ (zipWith_same f xs)
+  | _ :: xs => congrArg _ (zipWith_self f xs)
+
+@[deprecated zipWith_self (since := "2025-01-29")] abbrev zipWith_same := @zipWith_self
 
 /--
 See also `getElem?_zipWith'` for a variant
 using `Option.map` and `Option.bind` rather than a `match`.
 -/
 theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
-    (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with
+    (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
       | some a, some b => some (f a b) | _, _ => none := by
   induction as generalizing bs i with
   | nil => cases bs with
@@ -257,8 +259,7 @@ 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]; try constructor -- TODO: remove try constructor after update stage0
+  | _ :: _, _ :: _ => by simp only [map, zip_cons_cons, zip_map, Prod.map]
 
 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]

src/Init/Data/Vector.lean

@@ -10,4 +10,5 @@ import Init.Data.Vector.Lex
 import Init.Data.Vector.MapIdx
 import Init.Data.Vector.Count
 import Init.Data.Vector.DecidableEq
+import Init.Data.Vector.Zip
 import Init.Data.Vector.OfFn

src/Init/Data/Vector/Basic.lean

@@ -206,8 +206,11 @@ abbrev zipWithIndex := @zipIdx
   ⟨v.toArray.zip w.toArray, by simp⟩
 
 /-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
-@[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n :=
-  ⟨Array.zipWith a.toArray b.toArray f, by simp⟩
+@[inline] def zipWith (f : α → β → φ) (a : Vector α n) (b : Vector β n) : Vector φ n :=
+  ⟨Array.zipWith f a.toArray b.toArray, by simp⟩
+
+@[inline] def unzip (v : Vector (α × β) n) : Vector α n × Vector β n :=
+  ⟨⟨v.toArray.unzip.1, by simp⟩, ⟨v.toArray.unzip.2, by simp⟩⟩
 
 /-- The vector of length `n` whose `i`-th element is `f i`. -/
 @[inline] def ofFn (f : Fin n → α) : Vector α n :=

src/Init/Data/Vector/Lemmas.lean

@@ -158,8 +158,14 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 abbrev zipWithIndex_mk := @zipIdx_mk
 
 @[simp] theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β)
-      (ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f =
-        Vector.mk (Array.zipWith a b f) (by simp [ha, hb]) := rfl
+      (ha : a.size = n) (hb : b.size = n) : zipWith f (Vector.mk a ha) (Vector.mk b hb) =
+        Vector.mk (Array.zipWith f a b) (by simp [ha, hb]) := rfl
+
+@[simp] theorem mk_zip_mk (a : Array α) (b : Array β) (ha : a.size = n) (hb : b.size = n) :
+    zip (Vector.mk a ha) (Vector.mk b hb) = Vector.mk (Array.zip a b) (by simp [ha, hb]) := rfl
+
+@[simp] theorem unzip_mk (a : Array (α × β)) (h : a.size = n) :
+    (Vector.mk a h).unzip = (Vector.mk a.unzip.1 (by simp_all), Vector.mk a.unzip.2 (by simp_all)) := rfl
 
 @[simp] theorem anyM_mk [Monad m] (p : α → m Bool) (a : Array α) (h : a.size = n) :
     (Vector.mk a h).anyM p = a.anyM p := rfl
@@ -280,7 +286,7 @@ abbrev zipWithIndex_mk := @zipIdx_mk
     (a.zipIdx k).toArray = a.toArray.zipIdx k := rfl
 
 @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
-    (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
+    (Vector.zipWith f a b).toArray = Array.zipWith f a.toArray b.toArray := rfl
 
 @[simp] theorem anyM_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
     v.toArray.anyM p = v.anyM p := by
@@ -417,7 +423,7 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) :
   simp [List.take_of_length_le]
 
 @[simp] theorem toList_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
-    (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
+    (Vector.zipWith f a b).toArray = Array.zipWith f a.toArray b.toArray := rfl
 
 @[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (v : Vector α n) :
     v.toList.anyM p = v.anyM p := by
@@ -2167,7 +2173,7 @@ defeq issues in the implicit size argument.
 /-! ### zipWith -/
 
 @[simp] theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat)
-    (hi : i < n) : (zipWith a b f)[i] = f a[i] b[i] := by
+    (hi : i < n) : (zipWith f a b)[i] = f a[i] b[i] := by
   cases a
   cases b
   simp

src/Init/Data/Vector/Zip.lean

@@ -0,0 +1,287 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Zip
+import Init.Data.Vector.Lemmas
+
+/-!
+# Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`.
+-/
+
+namespace Vector
+
+open Nat
+
+/-! ## Zippers -/
+
+/-! ### zipWith -/
+
+theorem zipWith_comm (f : α → β → γ) (la : Vector α n) (lb : Vector β n) :
+    zipWith f la lb = zipWith (fun b a => f a b) lb la := by
+  rcases la with ⟨la, rfl⟩
+  rcases lb with ⟨lb, h⟩
+  simpa using Array.zipWith_comm _ _ _
+
+theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Vector α n) :
+    zipWith f l l' = zipWith f l' l := by
+  rw [zipWith_comm]
+  simp only [comm]
+
+@[simp]
+theorem zipWith_self (f : α → α → δ) (l : Vector α n) : zipWith f l l = l.map fun a => f a a := by
+  cases l
+  simp
+
+/--
+See also `getElem?_zipWith'` for a variant
+using `Option.map` and `Option.bind` rather than a `match`.
+-/
+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
+  cases as
+  cases bs
+  simp [Array.getElem?_zipWith]
+  rfl
+
+/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/
+theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
+    (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by
+  cases l₁
+  cases l₂
+  simp [Array.getElem?_zipWith']
+
+theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Vector α n} {l₂ : Vector β n} {z : γ} {i : Nat} :
+    (zipWith f l₁ l₂)[i]? = some z ↔
+      ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by
+  cases l₁
+  cases l₂
+  simp [Array.getElem?_zipWith_eq_some]
+
+theorem getElem?_zip_eq_some {l₁ : Vector α n} {l₂ : Vector β n} {z : α × β} {i : Nat} :
+    (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.getElem?_zip_eq_some]
+
+@[simp]
+theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) :
+    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.zipWith_map]
+
+theorem zipWith_map_left (l₁ : Vector α n) (l₂ : Vector β n) (f : α → α') (g : α' → β → γ) :
+    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.zipWith_map_left]
+
+theorem zipWith_map_right (l₁ : Vector α n) (l₂ : Vector β n) (f : β → β') (g : α → β' → γ) :
+    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.zipWith_map_right]
+
+theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
+    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simpa using Array.zipWith_foldr_eq_zip_foldr _
+
+theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
+    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simpa using Array.zipWith_foldl_eq_zip_foldl _
+
+
+theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Vector γ n) (l' : Vector δ n) :
+    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [Array.map_zipWith]
+
+theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [Array.take_zipWith]
+
+theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n) := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [Array.extract_zipWith]
+
+theorem zipWith_append (f : α → β → γ)
+    (l : Vector α n) (la : Vector α m) (l' : Vector β n) (lb : Vector β m) :
+    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  rcases la with ⟨la, rfl⟩
+  rcases lb with ⟨lb, h'⟩
+  simp [Array.zipWith_append, *]
+
+theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} :
+    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by
+  rcases l₁ with ⟨l₁, h₁⟩
+  rcases l₂ with ⟨l₂, h₂⟩
+  rcases l₁' with ⟨l₁', rfl⟩
+  rcases l₂' with ⟨l₂', rfl⟩
+  simp only [mk_zipWith_mk, mk_append_mk, eq_mk, Array.zipWith_eq_append_iff,
+    mk_eq, toArray_append, toArray_zipWith]
+  constructor
+  · rintro ⟨w, x, y, z, h, rfl, rfl, rfl, rfl⟩
+    simp only [Array.size_append, Array.size_zipWith] at h₁ h₂
+    exact ⟨mk w (by simp; omega), mk x (by simp; omega), mk y (by simp; omega), mk z (by simp; omega), by simp⟩
+  · rintro ⟨⟨w, hw⟩, ⟨x, hx⟩, ⟨y, hy⟩, ⟨z, hz⟩, rfl, rfl, w₁, w₂⟩
+    simp only at w₁ w₂
+    exact ⟨w, x, y, z, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩
+
+@[simp] theorem zipWith_mkVector {a : α} {b : β} {n : Nat} :
+    zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b) := by
+  ext
+  simp
+
+theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Vector α n) (l' : Vector β n) :
+    map (Function.uncurry f) (l.zip l') = zipWith f l l' := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [Array.map_uncurry_zip_eq_zipWith]
+
+theorem map_zip_eq_zipWith (f : α × β → γ) (l : Vector α n) (l' : Vector β n) :
+    map f (l.zip l') = zipWith (Function.curry f) l l' := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [Array.map_zip_eq_zipWith]
+
+theorem reverse_zipWith :
+    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h⟩
+  simp [Array.reverse_zipWith, h]
+
+/-! ### zip -/
+
+@[simp]
+theorem getElem_zip {l : Vector α n} {l' : Vector β n} {i : Nat} {h : i < n} :
+    (zip l l')[i] = (l[i], l'[i]) :=
+  getElem_zipWith ..
+
+theorem zip_eq_zipWith (l₁ : Vector α n) (l₂ : Vector β n) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.zip_eq_zipWith, h]
+
+theorem zip_map (f : α → γ) (g : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) :
+    zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g) := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.zip_map, h]
+
+theorem zip_map_left (f : α → γ) (l₁ : Vector α n) (l₂ : Vector β n) :
+    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
+
+theorem zip_map_right (f : β → γ) (l₁ : Vector α n) (l₂ : Vector β n) :
+    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
+
+theorem zip_append {l₁ : Vector α n} {l₂ : Vector β n} {r₁ : Vector α m} {r₂ : Vector β m} :
+    zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  rcases r₁ with ⟨r₁, rfl⟩
+  rcases r₂ with ⟨r₂, h'⟩
+  simp [Array.zip_append, h, h']
+
+theorem zip_map' (f : α → β) (g : α → γ) (l : Vector α n) :
+    zip (l.map f) (l.map g) = l.map fun a => (f a, g a) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.zip_map']
+
+theorem of_mem_zip {a b} {l₁ : Vector α n} {l₂ : Vector β n} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simpa using Array.of_mem_zip
+
+theorem map_fst_zip (l₁ : Vector α n) (l₂ : Vector β n) :
+    map Prod.fst (zip l₁ l₂) = l₁ := by
+  cases l₁
+  cases l₂
+  simp_all [Array.map_fst_zip]
+
+theorem map_snd_zip (l₁ : Vector α n) (l₂ : Vector β n) :
+    map Prod.snd (zip l₁ l₂) = l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.map_snd_zip, h]
+
+theorem map_prod_left_eq_zip {l : Vector α n} (f : α → β) :
+    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
+  rcases l with ⟨l, rfl⟩
+  rw [← zip_map']
+  congr
+  simp
+
+theorem map_prod_right_eq_zip {l : Vector α n} (f : α → β) :
+    (l.map fun x => (f x, x)) = (l.map f).zip l := by
+  rcases l with ⟨l, rfl⟩
+  rw [← zip_map']
+  congr
+  simp
+
+theorem zip_eq_append_iff {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} {l₁' : Vector (α × β) n} {l₂' : Vector (α × β) m} :
+    zip l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by
+  simp [zip_eq_zipWith, zipWith_eq_append_iff]
+
+@[simp] theorem zip_mkVector {a : α} {b : β} {n : Nat} :
+    zip (mkVector n a) (mkVector n b) = mkVector n (a, b) := by
+  ext <;> simp
+
+
+/-! ### unzip -/
+
+@[simp] 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
+  induction l <;> simp_all
+
+theorem unzip_eq_map (l : Vector (α × β) n) : unzip l = (l.map Prod.fst, l.map Prod.snd) := by
+  cases l
+  simp [List.unzip_eq_map]
+
+theorem zip_unzip (l : Vector (α × β) n) : zip (unzip l).1 (unzip l).2 = l := by
+  rcases l with ⟨l, rfl⟩
+  simp only [unzip_mk, mk_zip_mk, Array.zip_unzip]
+
+theorem unzip_zip_left {l₁ : Vector α n} {l₂ : Vector β n}  :
+    (unzip (zip l₁ l₂)).1 = l₁ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.unzip_zip_left, h, Array.map_fst_zip]
+
+theorem unzip_zip_right {l₁ : Vector α n} {l₂ : Vector β n} :
+    (unzip (zip l₁ l₂)).2 = l₂ := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.unzip_zip_right, h, Array.map_snd_zip]
+
+theorem unzip_zip {l₁ : Vector α n} {l₂ : Vector β n} :
+    unzip (zip l₁ l₂) = (l₁, l₂) := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, h⟩
+  simp [Array.unzip_zip, h, Array.map_fst_zip, Array.map_snd_zip]
+
+theorem zip_of_prod {l : Vector α n} {l' : Vector β n} {lp : Vector (α × β) n} (hl : lp.map Prod.fst = l)
+    (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
+  rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
+
+@[simp] theorem unzip_mkVector {n : Nat} {a : α} {b : β} :
+    unzip (mkVector n (a, b)) = (mkVector n a, mkVector n b) := by
+  ext1 <;> simp
+
+end Vector

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -80,7 +80,7 @@ partial def merge (v1 v2 : Value) : Value :=
   | top, _ | _, top => top
   | ctor i1 vs1, ctor i2 vs2 =>
     if i1 == i2 then
-      ctor i1 (vs1.zipWith vs2 merge)
+      ctor i1 (Array.zipWith merge vs1 vs2)
     else
       choice [v1, v2]
   | choice vs1, choice vs2 =>

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -186,7 +186,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       let mut paramsInfo := declsInfo[i]!
       let some mask := m.find? decl.name | unreachable!
       trace[Compiler.specialize.info] "{decl.name} {mask}"
-      paramsInfo := paramsInfo.zipWith mask fun info fixed => if fixed || info matches .user then info else .other
+      paramsInfo := Array.zipWith (fun info fixed => if fixed || info matches .user then info else .other) paramsInfo mask
       for j in [:paramsInfo.size] do
         let mut info := paramsInfo[j]!
         if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then

src/Lean/Elab/Command.lean

@@ -496,8 +496,8 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                     newStx := stxNew
                     newNextMacroScope := nextMacroScope
                     hasTraces
-                    next := cmdPromises.zipWith cmds fun cmdPromise cmd =>
-                      { range? := cmd.getRange?, task := cmdPromise.result }
+                    next := Array.zipWith (fun cmdPromise cmd =>
+                      { range? := cmd.getRange?, task := cmdPromise.result }) cmdPromises cmds
                     : MacroExpandedSnapshot
                   }
                   -- After the first command whose syntax tree changed, we must disable

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -790,7 +790,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
   -- (One for each non-forbiddend arg)
   let basicMeassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess
   let basicMeassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
-  let basicMeasures := Array.zipWith basicMeassures₁ basicMeassures₂ (· ++ ·)
+  let basicMeasures := Array.zipWith (· ++ ·) basicMeassures₁ basicMeassures₂
 
   -- The list of measures, including the measures that order functions.
   -- The function ordering measures come last

src/Lean/Elab/StructInst.lean

@@ -120,7 +120,7 @@ Expands fields.
   let fields? ← fields.mapM expandStructInstField
   if fields?.all (·.isNone) then
     Macro.throwUnsupported
-  let fields := fields?.zipWith fields Option.getD
+  let fields := Array.zipWith Option.getD fields? fields
   let structInstFields := structInstFields.setArg 0 <| Syntax.mkSep fields (mkAtomFrom stx ", ")
   return stx.setArg 2 structInstFields
 

src/Lean/Elab/Tactic/Induction.lean

@@ -286,8 +286,9 @@ where
               diagnostics := .empty
               inner? := none
               finished := { range? := none, task := finished.result }
-              next := altStxs.zipWith altPromises fun stx prom =>
-                { range? := stx.getRange?, task := prom.result }
+              next := Array.zipWith
+                (fun stx prom => { range? := stx.getRange?, task := prom.result })
+                altStxs altPromises
             }
             goWithIncremental <| altPromises.mapIdx fun i prom => {
               old? := do

src/Lean/Meta/ArgsPacker.lean

@@ -471,7 +471,7 @@ Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, re
 ```
 -/
 def uncurryType (argsPacker : ArgsPacker) (types : Array Expr) : MetaM Expr := do
-  let unary ← (Array.zipWith argsPacker.varNamess types Unary.uncurryType).mapM id
+  let unary ← (Array.zipWith Unary.uncurryType argsPacker.varNamess types).mapM id
   Mutual.uncurryType unary
 
 /--
@@ -482,11 +482,11 @@ and `(z : C) → R₂[z]`, returns an expression of type
 ```
 -/
 def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do
-  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
+  let unary ← (Array.zipWith Unary.uncurry argsPacker.varNamess es).mapM id
   Mutual.uncurry unary
 
 def uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr := do
-  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
+  let unary ← (Array.zipWith Unary.uncurry argsPacker.varNamess es).mapM id
   Mutual.uncurryWithType resultType unary
 
 /--
@@ -497,7 +497,7 @@ and `(z : C) → R`, returns an expression of type
 ```
 -/
 def uncurryND (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do
-  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
+  let unary ← (Array.zipWith Unary.uncurry argsPacker.varNamess es).mapM id
   Mutual.uncurryND unary
 
 /--
@@ -533,7 +533,7 @@ Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (non-dependent), return types
 -/
 def curryType (argsPacker : ArgsPacker) (t : Expr) : MetaM (Array Expr) := do
   let unary ← Mutual.curryType argsPacker.numFuncs t
-  (Array.zipWith argsPacker.varNamess unary Unary.curryType).mapM id
+  (Array.zipWith Unary.curryType argsPacker.varNamess unary).mapM id
 
 /--
 Given expression `e` of type `(x : a ⊗' b ⊕' c ⊗' d) → e[x]`, wraps that expression

tests/lean/run/array_isEqvAux.lean

@@ -42,6 +42,6 @@ example : #[0, 1, 2].insertIdx 1 3 = #[0, 3, 1, 2] := by decide
 
 example : #[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true := by decide
 
-example : #[0, 1, 2].zipWith #[3, 4, 5] (· + ·) = #[3, 5, 7] := by decide
+example : Array.zipWith (· + ·) #[0, 1, 2] #[3, 4, 5] = #[3, 5, 7] := by decide
 
 example : #[0, 1, 2].allDiff = true := by decide