-- 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
α : 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

Tactic:
constructor

Result:
case mk.mk.mk.mk.mp
α : 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

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

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 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

Tactic:
exact ⟨w, x, y, z, by simpa [hw, hy] using ⟨w₁, w₂⟩⟩

Result:
no goals

Proof state:
case mk.mk.mk.mk.mp
α : 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

Tactic:
rintro ⟨w, x, y, z, h, rfl, rfl, rfl, rfl⟩

Result:
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 ++ x).size = (Array.zipWith f w y).size + (Array.zipWith f x z).size
h₂ : (y ++ z).size = (Array.zipWith f w y).size + (Array.zipWith f x 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

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 = min x.size z.size

Tactic:
omega

Result:
no goals

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 ++ x).size = (Array.zipWith f w y).size + (Array.zipWith f x z).size
h₂ : (y ++ z).size = (Array.zipWith f w y).size + (Array.zipWith f x 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:
simp only [Array.size_append, Array.size_zipWith] at h₁ h₂

Result:
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

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
⊢ w.size = min w.size y.size

Tactic:
omega

Result:
no goals

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

Tactic:
rcases l₂ with ⟨l₂, h₂⟩

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

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
⊢ w.size = (Array.zipWith f w y).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
⊢ w.size = min w.size y.size