no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type ?u.21794
f : α → γ
g : β → δ
l₁ : List α
⊢ zip (map f l₁) (map g []) = map (Prod.map f g) (zip l₁ [])
simp only [map, zip_nil_right]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type ?u.21794
f : α → γ
g : β → δ
a : α
l₁ : List α
b : β
l₂ : List β
⊢ (f a, g b) :: map (fun x => (f x.fst, g x.snd)) (zip l₁ l₂) =
    (f a, g b) :: map (fun x => (f x.fst, g x.snd)) (zipWith Prod.mk l₁ l₂)
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type ?u.21794
f : α → γ
g : β → δ
a : α
l₁ : List α
b : β
l₂ : List β
⊢ zip (map f (a :: l₁)) (map g (b :: l₂)) = map (Prod.map f g) (zip (a :: l₁) (b :: l₂))
simp only [map, zip_cons_cons, zip_map, Prod.map]
no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type ?u.21794
f : α → γ
g : β → δ
a : α
l₁ : List α
b : β
l₂ : List β
⊢ (f a, g b) :: map (fun x => (f x.fst, g x.snd)) (zip l₁ l₂) =
    (f a, g b) :: map (fun x => (f x.fst, g x.snd)) (zipWith Prod.mk l₁ l₂)
constructor