-- 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:
α : 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.size = y.size ∧
    { toArray := w, size_toArray := hw }.toArray ++ { toArray := x, size_toArray := hx }.toArray = w ++ x ∧
      { toArray := y, size_toArray := hy }.toArray ++ { toArray := z, size_toArray := hz }.toArray = y ++ z ∧
        l₁' = Array.zipWith f w y ∧ l₂' = Array.zipWith f x z

Tactic:
simpa [hw, hy] using ⟨w₁, w₂⟩

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
⊢ w ++ x = { toArray := w, size_toArray := ⋯ }.toArray ++ { toArray := x, size_toArray := ⋯ }.toArray ∧
    y ++ z = { toArray := y, size_toArray := ⋯ }.toArray ++ { toArray := z, size_toArray := ⋯ }.toArray ∧
      Array.zipWith f w y =
          Array.zipWith f { toArray := w, size_toArray := ⋯ }.toArray { toArray := y, size_toArray := ⋯ }.toArray ∧
        Array.zipWith f x z =
          Array.zipWith f { toArray := x, size_toArray := ⋯ }.toArray { toArray := z, size_toArray := ⋯ }.toArray

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

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : Nat
l₂' : Vector γ m
f : α → β → γ
l₁ : Array α
l₂ : Array β
l₁' : Array γ
h₁ : l₁.size = l₁'.size + m
h₂ : l₂.size = l₁'.size + m
⊢ zipWith f { toArray := l₁, size_toArray := h₁ } { toArray := l₂, size_toArray := h₂ } =
      { toArray := l₁', size_toArray := ⋯ } ++ l₂' ↔
    ∃ 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 ∧ l₂' = zipWith f x z

Tactic:
rcases l₂' with ⟨l₂', rfl⟩

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

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

Proof state:
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

Tactic:
rcases l₁' with ⟨l₁', rfl⟩

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : Nat
l₂' : Vector γ m
f : α → β → γ
l₁ : Array α
l₂ : Array β
l₁' : Array γ
h₁ : l₁.size = l₁'.size + m
h₂ : l₂.size = l₁'.size + m
⊢ zipWith f { toArray := l₁, size_toArray := h₁ } { toArray := l₂, size_toArray := h₂ } =
      { toArray := l₁', size_toArray := ⋯ } ++ l₂' ↔
    ∃ 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 ∧ l₂' = zipWith f x z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n m : Nat
l₁' : Vector γ n
l₂' : Vector γ m
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

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

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