-- 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:
α : 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
⊢ (x₁ :: w).length = (x₂ :: y).length ∧
    x₁ :: (w ++ x) = x₁ :: w ++ x ∧
      x₂ :: (y ++ z) = x₂ :: y ++ z ∧ f x₁ x₂ :: l₁'' = zipWith f (x₁ :: w) (x₂ :: y) ∧ zipWith f x z = zipWith f x z

Tactic:
simp [h, h']

Result:
no goals

Proof state:
case cons.nil
α : 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 γ
⊢ zipWith f (x₁ :: l₁) [] = l₁' ++ l₂' ↔
    ∃ w x y z, w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ [] = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
constructor

Result:
case cons.nil.mp
α : 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 γ
⊢ zipWith f (x₁ :: l₁) [] = l₁' ++ l₂' →
    ∃ w x y z, w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ [] = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

case cons.nil.mpr
α : 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 γ
⊢ (∃ w x y z, w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ [] = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z) →
    zipWith f (x₁ :: l₁) [] = l₁' ++ l₂'

Proof state:
case cons.nil.mpr
α : 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 γ
⊢ (∃ w x y z, w.length = y.length ∧ x₁ :: l₁ = w ++ x ∧ [] = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z) →
    zipWith f (x₁ :: l₁) [] = l₁' ++ l₂'

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

Result:
case cons.nil.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ w x : List α
y z : List β
h₁ : w.length = y.length
left✝ : x₁ :: l₁ = w ++ x
h₃ : [] = y ++ 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 (x₁ :: l₁) [] = zipWith f w y ++ zipWith f x z

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

Tactic:
exact ⟨[], [], [], by simp⟩

Result:
no goals

Proof state:
case cons.nil.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ w x : List α
y z : List β
h₁ : w.length = y.length
left✝ : x₁ :: l₁ = w ++ x
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
h₃ : y = [] ∧ z = []
⊢ zipWith f (x₁ :: l₁) [] = zipWith f w y ++ zipWith f x z

Tactic:
obtain ⟨rfl, rfl⟩ := h₃

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

Proof state:
case cons.cons.mp
α : 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 β
⊢ (l₁' = [] ∧ l₂' = f x₁ x₂ :: zipWith f l₁ l₂ ∨ ∃ a', l₁' = f x₁ x₂ :: a' ∧ zipWith f l₁ l₂ = a' ++ 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:
rintro (⟨rfl, rfl⟩ | ⟨l₁'', rfl, h⟩)

Result:
case cons.cons.mp.inl.intro
α : 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
⊢ ∃ w x y z,
    w.length = y.length ∧
      x₁ :: l₁ = w ++ x ∧ x₂ :: l₂ = y ++ z ∧ [] = zipWith f w y ∧ f x₁ x₂ :: zipWith f l₁ l₂ = zipWith f x z

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 : zipWith f l₁ l₂ = l₁'' ++ l₂'
⊢ ∃ 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

Proof state:
case cons.nil.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ w x : List α
y z : List β
h₁ : w.length = y.length
left✝ : x₁ :: l₁ = w ++ x
h₃ : [] = y ++ 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 (x₁ :: l₁) [] = zipWith f w y ++ zipWith f x z

Tactic:
simp only [nil_eq, append_eq_nil_iff] at h₃

Result:
case cons.nil.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
l₁ w x : List α
y z : List β
h₁ : w.length = y.length
left✝ : x₁ :: l₁ = w ++ x
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
h₃ : y = [] ∧ z = []
⊢ zipWith f (x₁ :: l₁) [] = zipWith f w y ++ zipWith f x z