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

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

Tactic:
cases l₁'

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : Array γ
f : α → β → γ
toList✝² : List α
toList✝¹ : List β
toList✝ : List γ
⊢ zipWith f { toList := toList✝² } { toList := toList✝¹ } = { toList := toList✝ } ++ l₂' ↔
    ∃ w x y z,
      w.size = y.size ∧
        { toList := toList✝² } = w ++ x ∧
          { toList := toList✝¹ } = y ++ z ∧ { toList := toList✝ } = zipWith f w y ∧ l₂' = zipWith f x z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : List α
y z : List β
h : w.length = y.length
⊢ w.toArray.size = y.toArray.size ∧
    w ++ x = w.toArray.toList ++ x.toArray.toList ∧
      y ++ z = y.toArray.toList ++ z.toArray.toList ∧
        { toList := List.zipWith f w y } = zipWith f w.toArray y.toArray ∧
          { toList := List.zipWith f x z } = zipWith f x.toArray z.toArray

Tactic:
simp [h]

Result:
no goals

Proof state:
case mk.mk.mk.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ (∃ w x y z,
      w.length = y.length ∧
        toList✝³ = w ++ x ∧ toList✝² = y ++ z ∧ toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z) →
    ∃ w x y z,
      w.size = y.size ∧
        toList✝³ = w.toList ++ x.toList ∧
          toList✝² = y.toList ++ z.toList ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z

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 : List α
y z : List β
h : w.length = y.length
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.size = y_1.size ∧
      w ++ x = w_1.toList ++ x_1.toList ∧
        y ++ z = y_1.toList ++ z_1.toList ∧
          { toList := List.zipWith f w y } = zipWith f w_1 y_1 ∧ { toList := List.zipWith f x z } = zipWith f x_1 z_1

Proof state:
case mk.mk.mk.mk.mpr.intro.mk.intro.mk.intro.mk.intro.mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ toList✝ : List γ
w x : List α
y z : List β
h : { toList := w }.size = { toList := y }.size
h₁ : { toList := toList✝¹ } = zipWith f { toList := w } { toList := y }
h₂ : { toList := toList✝ } = zipWith f { toList := x } { toList := z }
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.length = y_1.length ∧
      { toList := w }.toList ++ { toList := x }.toList = w_1 ++ x_1 ∧
        { toList := y }.toList ++ { toList := z }.toList = y_1 ++ z_1 ∧
          toList✝¹ = List.zipWith f w_1 y_1 ∧ toList✝ = List.zipWith f x_1 z_1

Tactic:
exact ⟨w, x, y, z, by simp_all⟩

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ zipWith f { toList := toList✝³ } { toList := toList✝² } = { toList := toList✝¹ } ++ { toList := toList✝ } ↔
    ∃ w x y z,
      w.size = y.size ∧
        { toList := toList✝³ } = w ++ x ∧
          { toList := toList✝² } = y ++ z ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z

Tactic:
simp only [List.zipWith_toArray, List.append_toArray, mk.injEq, List.zipWith_eq_append_iff,
  toArray_eq_append_iff]

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ (∃ w x y z,
      w.length = y.length ∧
        toList✝³ = w ++ x ∧ toList✝² = y ++ z ∧ toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z) ↔
    ∃ w x y z,
      w.size = y.size ∧
        toList✝³ = w.toList ++ x.toList ∧
          toList✝² = y.toList ++ z.toList ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ toList✝ : List γ
w x : List α
y z : List β
h : { toList := w }.size = { toList := y }.size
h₁ : { toList := toList✝¹ } = zipWith f { toList := w } { toList := y }
h₂ : { toList := toList✝ } = zipWith f { toList := x } { toList := z }
⊢ w.length = y.length ∧
    { toList := w }.toList ++ { toList := x }.toList = w ++ x ∧
      { toList := y }.toList ++ { toList := z }.toList = y ++ z ∧
        toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ (∃ w x y z,
      w.length = y.length ∧
        toList✝³ = w ++ x ∧ toList✝² = y ++ z ∧ toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z) ↔
    ∃ w x y z,
      w.size = y.size ∧
        toList✝³ = w.toList ++ x.toList ∧
          toList✝² = y.toList ++ z.toList ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z

Tactic:
constructor

Result:
case mk.mk.mk.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ (∃ w x y z,
      w.length = y.length ∧
        toList✝³ = w ++ x ∧ toList✝² = y ++ z ∧ toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z) →
    ∃ w x y z,
      w.size = y.size ∧
        toList✝³ = w.toList ++ x.toList ∧
          toList✝² = y.toList ++ z.toList ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z

case mk.mk.mk.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ (∃ w x y z,
      w.size = y.size ∧
        toList✝³ = w.toList ++ x.toList ∧
          toList✝² = y.toList ++ z.toList ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z) →
    ∃ w x y z,
      w.length = y.length ∧
        toList✝³ = w ++ x ∧ toList✝² = y ++ z ∧ toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z

Proof state:
case mk.mk.mk.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ (∃ w x y z,
      w.size = y.size ∧
        toList✝³ = w.toList ++ x.toList ∧
          toList✝² = y.toList ++ z.toList ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z) →
    ∃ w x y z,
      w.length = y.length ∧
        toList✝³ = w ++ x ∧ toList✝² = y ++ z ∧ toList✝¹ = List.zipWith f w y ∧ toList✝ = List.zipWith f x z

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

Result:
case mk.mk.mk.mk.mpr.intro.mk.intro.mk.intro.mk.intro.mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ toList✝ : List γ
w x : List α
y z : List β
h : { toList := w }.size = { toList := y }.size
h₁ : { toList := toList✝¹ } = zipWith f { toList := w } { toList := y }
h₂ : { toList := toList✝ } = zipWith f { toList := x } { toList := z }
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.length = y_1.length ∧
      { toList := w }.toList ++ { toList := x }.toList = w_1 ++ x_1 ∧
        { toList := y }.toList ++ { toList := z }.toList = y_1 ++ z_1 ∧
          toList✝¹ = List.zipWith f w_1 y_1 ∧ toList✝ = List.zipWith f x_1 z_1