-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_eq_cons_iff {l₁ : List α} {l₂ : List β} :
    zip l₁ l₂ = (a, b) :: l ↔
      ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zip l₁' l₂'

Proof state:
case mpr
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ (∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zipWith Prod.mk l₁' l₂') →
    ∃ a_2 l₁' b_1 l₂', l₁ = a_2 :: l₁' ∧ l₂ = b_1 :: l₂' ∧ (a, b) = (a_2, b_1) ∧ l = zipWith Prod.mk l₁' l₂'

Tactic:
rintro ⟨l₁', l₂', rfl, rfl, rfl⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
a : α
b : β
l₁' : List α
l₂' : List β
⊢ ∃ a_1 l₁'_1 b_1 l₂'_1,
    a :: l₁' = a_1 :: l₁'_1 ∧
      b :: l₂' = b_1 :: l₂'_1 ∧ (a, b) = (a_1, b_1) ∧ zipWith Prod.mk l₁' l₂' = zipWith Prod.mk l₁'_1 l₂'_1

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l₁' : List α
l₂' : List β
⊢ a :: l₁' = a :: l₁' ∧ b :: l₂' = b :: l₂' ∧ (a, b) = (a, b) ∧ zipWith Prod.mk l₁' l₂' = zipWith Prod.mk l₁' l₂'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ l₁.zip l₂ = (a, b) :: l ↔ ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = l₁'.zip l₂'

Tactic:
simp only [zip_eq_zipWith, zipWith_eq_cons_iff]

Result:
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ (∃ a_1 l₁' b_1 l₂', l₁ = a_1 :: l₁' ∧ l₂ = b_1 :: l₂' ∧ (a, b) = (a_1, b_1) ∧ l = zipWith Prod.mk l₁' l₂') ↔
    ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zipWith Prod.mk l₁' l₂'

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.refl.intro
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : List α
l₂ : List β
⊢ ∃ l₁' l₂', a :: l₁ = a :: l₁' ∧ b :: l₂ = b :: l₂' ∧ zipWith Prod.mk l₁ l₂ = zipWith Prod.mk l₁' l₂'

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
a : α
b : β
l₁' : List α
l₂' : List β
⊢ ∃ a_1 l₁'_1 b_1 l₂'_1,
    a :: l₁' = a_1 :: l₁'_1 ∧
      b :: l₂' = b_1 :: l₂'_1 ∧ (a, b) = (a_1, b_1) ∧ zipWith Prod.mk l₁' l₂' = zipWith Prod.mk l₁'_1 l₂'_1

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

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ (∃ a_1 l₁' b_1 l₂', l₁ = a_1 :: l₁' ∧ l₂ = b_1 :: l₂' ∧ (a, b) = (a_1, b_1) ∧ l = zipWith Prod.mk l₁' l₂') →
    ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zipWith Prod.mk l₁' l₂'

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

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
β : Type u_2
a✝ : α
b✝ : β
a : α
l₁ : List α
b : β
l₂ : List β
h : (a✝, b✝) = (a, b)
⊢ ∃ l₁' l₂', a :: l₁ = a✝ :: l₁' ∧ b :: l₂ = b✝ :: l₂' ∧ zipWith Prod.mk l₁ l₂ = zipWith Prod.mk l₁' l₂'

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
β : Type u_2
a✝ : α
b✝ : β
a : α
l₁ : List α
b : β
l₂ : List β
h : a✝ = a ∧ b✝ = b
⊢ ∃ l₁' l₂', a :: l₁ = a✝ :: l₁' ∧ b :: l₂ = b✝ :: l₂' ∧ zipWith Prod.mk l₁ l₂ = zipWith Prod.mk l₁' l₂'

Tactic:
obtain ⟨rfl, rfl⟩ := h

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.refl.intro
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : List α
l₂ : List β
⊢ ∃ l₁' l₂', a :: l₁ = a :: l₁' ∧ b :: l₂ = b :: l₂' ∧ zipWith Prod.mk l₁ l₂ = zipWith Prod.mk l₁' l₂'

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
β : Type u_2
a✝ : α
b✝ : β
a : α
l₁ : List α
b : β
l₂ : List β
h : (a✝, b✝) = (a, b)
⊢ ∃ l₁' l₂', a :: l₁ = a✝ :: l₁' ∧ b :: l₂ = b✝ :: l₂' ∧ zipWith Prod.mk l₁ l₂ = zipWith Prod.mk l₁' l₂'

Tactic:
simp only [Prod.mk.injEq] at h

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
β : Type u_2
a✝ : α
b✝ : β
a : α
l₁ : List α
b : β
l₂ : List β
h : a✝ = a ∧ b✝ = b
⊢ ∃ l₁' l₂', a :: l₁ = a✝ :: l₁' ∧ b :: l₂ = b✝ :: l₂' ∧ zipWith Prod.mk l₁ l₂ = zipWith Prod.mk l₁' l₂'

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ (∃ a_1 l₁' b_1 l₂', l₁ = a_1 :: l₁' ∧ l₂ = b_1 :: l₂' ∧ (a, b) = (a_1, b_1) ∧ l = zipWith Prod.mk l₁' l₂') ↔
    ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zipWith Prod.mk l₁' l₂'

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ (∃ a_1 l₁' b_1 l₂', l₁ = a_1 :: l₁' ∧ l₂ = b_1 :: l₂' ∧ (a, b) = (a_1, b_1) ∧ l = zipWith Prod.mk l₁' l₂') →
    ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zipWith Prod.mk l₁' l₂'

case mpr
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
l₁ : List α
l₂ : List β
⊢ (∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zipWith Prod.mk l₁' l₂') →
    ∃ a_2 l₁' b_1 l₂', l₁ = a_2 :: l₁' ∧ l₂ = b_1 :: l₂' ∧ (a, b) = (a_2, b_1) ∧ l = zipWith Prod.mk l₁' l₂'