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

Tactic:
rw [ih₁] at h

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

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

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

Tactic:
rw [cons_eq_append_iff]

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 β
⊢ (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

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

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

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

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

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

Tactic:
exact ⟨[], x₁ :: l₁, [], by simp⟩

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
exact ⟨[], x₁ :: l₁, [], x₂ :: l₂, by simp⟩

Result:
no goals