case head
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
l₁ : List α
l₂ : List β
⊢ a ∈ a :: l₁ ∧ b ∈ b :: l₂

case tail
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : (a, b) ∈ zip (head✝¹ :: l₁) (head✝ :: l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
cases' h with _ _ _ h
no goals
case head
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
l₁ : List α
l₂ : List β
⊢ a ∈ a :: l₁ ∧ b ∈ b :: l₂
simp
case tail
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
this : a ∈ l₁ ∧ b ∈ l₂
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
case tail
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
have := mem_zip h
no goals
case tail
α : Type u
β : Type u_1
γ : Type ?u.74738
δ : Type ?u.74741
ε : Type ?u.74744
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
this : a ∈ l₁ ∧ b ∈ l₂
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂
exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩