-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_eq_cons_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
    zipWith f l₁ l₂ = g :: l ↔
      ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = g :: l ↔
    ∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ g = f a b ∧ l = zipWith f l₁' l₂'

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = g :: l →
    ∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ g = f a b ∧ l = zipWith f l₁' l₂'

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ (∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ g = f a b ∧ l = zipWith f l₁' l₂') →
    zipWith f (a' :: l₁) (b' :: l₂) = g :: l

Proof state:
case mp.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ ∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ f a' b' = f a b ∧ zipWith f l₁ l₂ = zipWith f l₁' l₂'

Tactic:
refine ⟨a', l₁, b', l₂, by simp⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = g :: l →
    ∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ g = f a b ∧ l = zipWith f l₁' l₂'

Tactic:
rintro ⟨⟨rfl, rfl⟩, rfl⟩

Result:
case mp.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ ∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ f a' b' = f a b ∧ zipWith f l₁ l₂ = zipWith f l₁' l₂'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁ : List α
l₂✝ : List β
b : β
l₂ : List β
⊢ zipWith f [] (b :: l₂) = g :: l ↔
    ∃ a l₁' b_1 l₂', [] = a :: l₁' ∧ b :: l₂ = b_1 :: l₂' ∧ g = f a b_1 ∧ l = zipWith f l₁' l₂'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁ : List α
l₂ : List β
⊢ zipWith f [] [] = g :: l ↔ ∃ a l₁' b l₂', [] = a :: l₁' ∧ [] = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂'

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = f a' b' :: zipWith f l₁ l₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂ : List β
a : α
l₁ : List α
⊢ zipWith f (a :: l₁) [] = g :: l ↔
    ∃ a_1 l₁' b l₂', a :: l₁ = a_1 :: l₁' ∧ [] = b :: l₂' ∧ g = f a_1 b ∧ l = zipWith f l₁' l₂'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ (a' = a' ∧ l₁ = l₁) ∧ (b' = b' ∧ l₂ = l₂) ∧ f a' b' = f a' b' ∧ zipWith f l₁ l₂ = zipWith f l₁ l₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = g :: l ↔
    ∃ a l₁' b l₂', a' :: l₁ = a :: l₁' ∧ b' :: l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂'

Tactic:
simp only [zip_cons_cons, cons.injEq, Prod.mk.injEq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = g :: l ↔
    ∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ g = f a b ∧ l = zipWith f l₁' l₂'

Proof state:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ
l : List γ
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ (∃ a l₁' b l₂', (a' = a ∧ l₁ = l₁') ∧ (b' = b ∧ l₂ = l₂') ∧ g = f a b ∧ l = zipWith f l₁' l₂') →
    zipWith f (a' :: l₁) (b' :: l₂) = g :: l

Tactic:
rintro ⟨a, l₁, b, l₂, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl, rfl⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁✝ : List α
l₂✝ : List β
a' : α
l₁ : List α
b' : β
l₂ : List β
⊢ zipWith f (a' :: l₁) (b' :: l₂) = f a' b' :: zipWith f l₁ l₂