-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Proof state:
case cons.cons.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
x₁ : α
l₁ : List α
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z
x₂ : β
l₂ : List β
l₁'' : List γ
h : ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁'' = zipWith f w y ∧ l₂' = zipWith f x z
⊢ ∃ w x y z,
    w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ x₂ :: l₂ = y ++ z ∧ f x₁ x₂ :: l₁'' = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
obtain ⟨w, x, y, z, h, rfl, rfl, h', rfl⟩ := h

Result:
case cons.cons.mp.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
x₂ : β
l₁'' : List γ
w x : List α
y z : List β
h : w.length = y.length
h' : l₁'' = zipWith f w y
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f (w ++ x) l₂ = l₁' ++ zipWith f x z ↔
      ∃ w_1 x_1 y z_1,
        w_1.length = y.length ∧
          w ++ x = w_1 ++ x_1 ∧ l₂ = y ++ z_1 ∧ l₁' = zipWith f w_1 y ∧ zipWith f x z = zipWith f x_1 z_1
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.length = y_1.length ∧
      x₁ :: (w ++ x) = w_1 ++ x_1 ∧
        x₂ :: (y ++ z) = y_1 ++ z_1 ∧ f x₁ x₂ :: l₁'' = zipWith f w_1 y_1 ∧ zipWith f x z = zipWith f x_1 z_1

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
l₁' : List γ
l₂ : List β
⊢ zipWith f [] l₂ = l₁' ++ l₂' ↔
    ∃ w x y z, w.length = y.length ∧ [] = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
simp

Result:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
l₁' : List γ
l₂ : List β
⊢ l₁' = [] ∧ l₂' = [] ↔
    ∃ w x y,
      w.length = y.length ∧ (w = [] ∧ x = []) ∧ ∃ x_1, l₂ = y ++ x_1 ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x x_1

Proof state:
case cons.cons.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ : List α
x₂ : β
l₂ : List β
w x : List α
y z : List β
h₁ : w.length = y.length
h₂ : w = [] ∧ x = x₁ :: l₁ ∨ ∃ a', w = x₁ :: a' ∧ l₁ = a' ++ x
h₃ : y = [] ∧ z = x₂ :: l₂ ∨ ∃ a', y = x₂ :: a' ∧ l₂ = a' ++ z
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f l₁ l₂ = l₁' ++ zipWith f x z ↔
      ∃ w x_1 y z_1,
        w.length = y.length ∧ l₁ = w ++ x_1 ∧ l₂ = y ++ z_1 ∧ l₁' = zipWith f w y ∧ zipWith f x z = zipWith f x_1 z_1
⊢ zipWith f w y = [] ∧ zipWith f x z = f x₁ x₂ :: zipWith f l₁ l₂ ∨
    ∃ a', zipWith f w y = f x₁ x₂ :: a' ∧ zipWith f l₁ l₂ = a' ++ zipWith f x z

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨w', rfl, rfl⟩) := h₂

Result:
case cons.cons.mpr.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ : List α
x₂ : β
l₂ y z : List β
h₃ : y = [] ∧ z = x₂ :: l₂ ∨ ∃ a', y = x₂ :: a' ∧ l₂ = a' ++ z
h₁ : [].length = y.length
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f l₁ l₂ = l₁' ++ zipWith f (x₁ :: l₁) z ↔
      ∃ w x y z_1,
        w.length = y.length ∧
          l₁ = w ++ x ∧ l₂ = y ++ z_1 ∧ l₁' = zipWith f w y ∧ zipWith f (x₁ :: l₁) z = zipWith f x z_1
⊢ zipWith f [] y = [] ∧ zipWith f (x₁ :: l₁) z = f x₁ x₂ :: zipWith f l₁ l₂ ∨
    ∃ a', zipWith f [] y = f x₁ x₂ :: a' ∧ zipWith f l₁ l₂ = a' ++ zipWith f (x₁ :: l₁) z

case cons.cons.mpr.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
x₂ : β
l₂ : List β
x : List α
y z : List β
h₃ : y = [] ∧ z = x₂ :: l₂ ∨ ∃ a', y = x₂ :: a' ∧ l₂ = a' ++ z
w' : List α
h₁ : (x₁ :: w').length = y.length
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f (w' ++ x) l₂ = l₁' ++ zipWith f x z ↔
      ∃ w x_1 y z_1,
        w.length = y.length ∧
          w' ++ x = w ++ x_1 ∧ l₂ = y ++ z_1 ∧ l₁' = zipWith f w y ∧ zipWith f x z = zipWith f x_1 z_1
⊢ zipWith f (x₁ :: w') y = [] ∧ zipWith f x z = f x₁ x₂ :: zipWith f (w' ++ x) l₂ ∨
    ∃ a', zipWith f (x₁ :: w') y = f x₁ x₂ :: a' ∧ zipWith f (w' ++ x) l₂ = a' ++ zipWith f x z

Proof state:
case cons.cons.mpr.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
x₂ : β
l₂ : List β
x w' : List α
h₁ : (x₁ :: w').length = [].length
ih₁ :
  ∀ {l₁' : List γ} {l₂_1 : List β},
    zipWith f (w' ++ x) l₂_1 = l₁' ++ zipWith f x (x₂ :: l₂) ↔
      ∃ w x_1 y z,
        w.length = y.length ∧
          w' ++ x = w ++ x_1 ∧ l₂_1 = y ++ z ∧ l₁' = zipWith f w y ∧ zipWith f x (x₂ :: l₂) = zipWith f x_1 z
⊢ zipWith f (x₁ :: w') [] = [] ∧ zipWith f x (x₂ :: l₂) = f x₁ x₂ :: zipWith f (w' ++ x) l₂ ∨
    ∃ a', zipWith f (x₁ :: w') [] = f x₁ x₂ :: a' ∧ zipWith f (w' ++ x) l₂ = a' ++ zipWith f x (x₂ :: l₂)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
x₁ : α
l₁ : List α
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z
l₁' : List γ
x₂ : β
l₂ : List β
⊢ zipWith f (x₁ :: l₁) (x₂ :: l₂) = l₁' ++ l₂' ↔
    ∃ w x y z, w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ x₂ :: l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
simp only [zipWith_cons_cons]

Result:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
x₁ : α
l₁ : List α
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z
l₁' : List γ
x₂ : β
l₂ : List β
⊢ f x₁ x₂ :: zipWith f l₁ l₂ = l₁' ++ l₂' ↔
    ∃ w x y z, w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ 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 : α → β → γ
x₁ : α
l₁ : List α
ih₁ :
  ∀ {l₁' : List γ} {l₂ : List β},
    zipWith f l₁ l₂ = l₁' ++ [] ↔
      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ [] = zipWith f x z
⊢ [].length = [].length ∧
    x₁ :: l₁ = [] ++ x₁ :: l₁ ∧ ∃ x, ([] = [] ∧ x = []) ∧ [] = zipWith f [] [] ∧ [] = zipWith f (x₁ :: l₁) x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ : List α
x₂ : β
l₂ : List β
ih₁ :
  ∀ {l₁' : List γ} {l₂_1 : List β},
    zipWith f l₁ l₂_1 = l₁' ++ f x₁ x₂ :: zipWith f l₁ l₂ ↔
      ∃ w x y z,
        w.length = y.length ∧
          l₁ = w ++ x ∧ l₂_1 = y ++ z ∧ l₁' = zipWith f w y ∧ f x₁ x₂ :: zipWith f l₁ l₂ = zipWith f x z
⊢ [].length = [].length ∧
    x₁ :: l₁ = [] ++ x₁ :: l₁ ∧
      x₂ :: l₂ = [] ++ x₂ :: l₂ ∧ [] = zipWith f [] [] ∧ f x₁ x₂ :: zipWith f l₁ l₂ = zipWith f (x₁ :: l₁) (x₂ :: l₂)

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
l₁' : List γ
l₂ : List β
⊢ l₁' = [] ∧ l₂' = [] ↔
    ∃ w x y,
      w.length = y.length ∧ (w = [] ∧ x = []) ∧ ∃ x_1, l₂ = y ++ x_1 ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x x_1

Tactic:
constructor

Result:
case nil.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
l₁' : List γ
l₂ : List β
⊢ l₁' = [] ∧ l₂' = [] →
    ∃ w x y,
      w.length = y.length ∧ (w = [] ∧ x = []) ∧ ∃ x_1, l₂ = y ++ x_1 ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x x_1

case nil.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : List γ
f : α → β → γ
l₁' : List γ
l₂ : List β
⊢ (∃ w x y,
      w.length = y.length ∧ (w = [] ∧ x = []) ∧ ∃ x_1, l₂ = y ++ x_1 ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x x_1) →
    l₁' = [] ∧ l₂' = []