feat: align List/Array/Vector.zip/zipWith/zipWithAll/unzip (#6840)

This PR completes the alignment of
`List/Array/Vector.zip/zipWith/zipWithAll/unzip` lemmas.

Author: kim-em

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,32 +3543,32 @@ 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 β) :
     (as.zip bs).size = min as.size bs.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