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

Tactic:
simp_all [zipWith_append, Nat.succ_inj']

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
rintro rfl  rfl

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

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

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

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₂ : x₁ :: l₁ = w ++ 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

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

Tactic:
simp only [zipWith_nil_right, nil_eq, append_eq_nil_iff, exists_and_left, and_imp]

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 γ
⊢ l₁' = [] →
    l₂' = [] →
      ∃ w x y,
        w.length = y.length ∧
          x₁ :: l₁ = w ++ x ∧ ∃ x_1, (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.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

Tactic:
simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
or_false]

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 (x₁ :: l₁) z = f x₁ x₂ :: zipWith f l₁ l₂