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

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

case cons.cons.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 γ
x₂ : β
l₂ : List β
⊢ (∃ 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) →
    l₁' = [] ∧ l₂' = f x₁ x₂ :: zipWith f l₁ l₂ ∨ ∃ a', l₁' = f x₁ x₂ :: a' ∧ zipWith f l₁ l₂ = a' ++ l₂'

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

Tactic:
rintro ⟨rfl, rfl⟩

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

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

Tactic:
simp

Result:
no goals

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₃ : x₂ :: l₂ = 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 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:
rw [cons_eq_append_iff] at h₃

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

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

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃

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

case cons.cons.mpr.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x₁ : α
x₂ : β
x : List α
z : List β
w' : List α
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
y' : List β
h₁ : (x₁ :: w').length = (x₂ :: y').length
⊢ zipWith f (x₁ :: w') (x₂ :: y') = [] ∧ zipWith f x z = f x₁ x₂ :: zipWith f (w' ++ x) (y' ++ z) ∨
    ∃ a', zipWith f (x₁ :: w') (x₂ :: y') = f x₁ x₂ :: a' ∧ zipWith f (w' ++ x) (y' ++ z) = a' ++ zipWith f x z

Proof state:
case nil.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w✝¹ w✝ : List β
⊢ zipWith f [] w✝¹ = [] ∧ zipWith f [] w✝ = []

Tactic:
simp

Result:
no goals

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

Tactic:
refine ⟨x₁ :: w, x, x₂ :: y, z, by simp [h, h']⟩

Result:
no goals

Proof state:
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₂' = []

Tactic:
rintro ⟨_, _, _, -, ⟨rfl, rfl⟩, _, rfl, rfl, rfl⟩

Result:
case nil.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w✝¹ w✝ : List β
⊢ zipWith f [] w✝¹ = [] ∧ zipWith f [] w✝ = []