-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
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

Proof state:
case mk.mk.mk.mk.mpr.intro.mk.intro.mk.intro.mk.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁' l₂' : Array γ
w : Array α
hw : w.size = l₁'.size
x : Array α
hx : x.size = l₂'.size
y : Array β
hy : y.size = l₁'.size
z : Array β
hz : z.size = l₂'.size
h₁ :
  ({ toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray).size =
    l₁'.size + l₂'.size
h₂ :
  ({ toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray).size =
    l₁'.size + l₂'.size
w₁ : l₁' = Array.zipWith f { toArray := w, size_toArray := hw }.toArray { toArray := y, size_toArray := hy }.toArray
w₂ : l₂' = Array.zipWith f { toArray := x, size_toArray := hx }.toArray { toArray := z, size_toArray := hz }.toArray
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.size = y_1.size ∧
      { toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray = w_1 ++ x_1 ∧
        { toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray = y_1 ++ z_1 ∧
          l₁' = Array.zipWith f w_1 y_1 ∧ l₂' = Array.zipWith f x_1 z_1

Tactic:
simp only at w₁ w₂

Result:
case mk.mk.mk.mk.mpr.intro.mk.intro.mk.intro.mk.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁' l₂' : Array γ
w : Array α
hw : w.size = l₁'.size
x : Array α
hx : x.size = l₂'.size
y : Array β
hy : y.size = l₁'.size
z : Array β
hz : z.size = l₂'.size
h₁ :
  ({ toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray).size =
    l₁'.size + l₂'.size
h₂ :
  ({ toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray).size =
    l₁'.size + l₂'.size
w₁ : l₁' = Array.zipWith f w y
w₂ : l₂' = Array.zipWith f x z
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.size = y_1.size ∧
      { toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray = w_1 ++ x_1 ∧
        { toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray = y_1 ++ z_1 ∧
          l₁' = Array.zipWith f w_1 y_1 ∧ l₂' = Array.zipWith f x_1 z_1

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : Array α
l₂ : Array β
l₁' l₂' : Array γ
h₁ : l₁.size = l₁'.size + l₂'.size
h₂ : l₂.size = l₁'.size + l₂'.size
⊢ zipWith f { toArray := l₁, size_toArray := h₁ } { toArray := l₂, size_toArray := h₂ } =
      { toArray := l₁', size_toArray := ⋯ } ++ { toArray := l₂', size_toArray := ⋯ } ↔
    ∃ w x y z,
      { toArray := l₁, size_toArray := h₁ } = w ++ x ∧
        { toArray := l₂, size_toArray := h₂ } = y ++ z ∧
          { toArray := l₁', size_toArray := ⋯ } = zipWith f w y ∧ { toArray := l₂', size_toArray := ⋯ } = zipWith f x z

Tactic:
simp only [mk_zipWith_mk, mk_append_mk, eq_mk, Array.zipWith_eq_append_iff,
  mk_eq, toArray_append, toArray_zipWith]

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : Array α
l₂ : Array β
l₁' l₂' : Array γ
h₁ : l₁.size = l₁'.size + l₂'.size
h₂ : l₂.size = l₁'.size + l₂'.size
⊢ (∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = Array.zipWith f w y ∧ l₂' = Array.zipWith f x z) ↔
    ∃ w x y z,
      l₁ = w.toArray ++ x.toArray ∧
        l₂ = y.toArray ++ z.toArray ∧
          l₁' = Array.zipWith f w.toArray y.toArray ∧ l₂' = Array.zipWith f x.toArray z.toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : Array α
y z : Array β
h : w.size = y.size
h₁ : w.size + x.size = min w.size y.size + min x.size z.size
h₂ : y.size + z.size = min w.size y.size + min x.size z.size
⊢ x.size = min x.size z.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : Array α
y z : Array β
h : w.size = y.size
h₁ : w.size + x.size = min w.size y.size + min x.size z.size
h₂ : y.size + z.size = min w.size y.size + min x.size z.size
⊢ y.size = min w.size y.size

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mk.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : Array α
l₂ : Array β
l₁' l₂' : Array γ
h₁ : l₁.size = l₁'.size + l₂'.size
h₂ : l₂.size = l₁'.size + l₂'.size
⊢ (∃ w x y z,
      l₁ = w.toArray ++ x.toArray ∧
        l₂ = y.toArray ++ z.toArray ∧
          l₁' = Array.zipWith f w.toArray y.toArray ∧ l₂' = Array.zipWith f x.toArray z.toArray) →
    ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = Array.zipWith f w y ∧ l₂' = Array.zipWith f x z

Tactic:
rintro ⟨⟨w, hw⟩, ⟨x, hx⟩, ⟨y, hy⟩, ⟨z, hz⟩, rfl, rfl, w₁, w₂⟩

Result:
case mk.mk.mk.mk.mpr.intro.mk.intro.mk.intro.mk.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁' l₂' : Array γ
w : Array α
hw : w.size = l₁'.size
x : Array α
hx : x.size = l₂'.size
y : Array β
hy : y.size = l₁'.size
z : Array β
hz : z.size = l₂'.size
h₁ :
  ({ toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray).size =
    l₁'.size + l₂'.size
h₂ :
  ({ toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray).size =
    l₁'.size + l₂'.size
w₁ : l₁' = Array.zipWith f { toArray := w, size_toArray := hw }.toArray { toArray := y, size_toArray := hy }.toArray
w₂ : l₂' = Array.zipWith f { toArray := x, size_toArray := hx }.toArray { toArray := z, size_toArray := hz }.toArray
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.size = y_1.size ∧
      { toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray = w_1 ++ x_1 ∧
        { toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray = y_1 ++ z_1 ∧
          l₁' = Array.zipWith f w_1 y_1 ∧ l₂' = Array.zipWith f x_1 z_1

Proof state:
case mk.mk.mk.mk.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : Array α
y z : Array β
h : w.size = y.size
h₁ : w.size + x.size = min w.size y.size + min x.size z.size
h₂ : y.size + z.size = min w.size y.size + min x.size z.size
⊢ ∃ w_1 x_1 y_1 z_1,
    w ++ x = w_1.toArray ++ x_1.toArray ∧
      y ++ z = y_1.toArray ++ z_1.toArray ∧
        Array.zipWith f w y = Array.zipWith f w_1.toArray y_1.toArray ∧
          Array.zipWith f x z = Array.zipWith f x_1.toArray z_1.toArray

Tactic:
exact ⟨mk w (by simp; omega), mk x (by simp; omega), mk y (by simp; omega), mk z (by simp; omega), by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : Array α
y z : Array β
h : w.size = y.size
h₁ : w.size + x.size = min w.size y.size + min x.size z.size
h₂ : y.size + z.size = min w.size y.size + min x.size z.size
⊢ z.size = (Array.zipWith f x z).size

Tactic:
simp

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : Array α
y z : Array β
h : w.size = y.size
h₁ : w.size + x.size = min w.size y.size + min x.size z.size
h₂ : y.size + z.size = min w.size y.size + min x.size z.size
⊢ z.size = min x.size z.size