α : Type u
β : Type u_1
γ : Type ?u.88166
δ : Type ?u.88169
ε : Type ?u.88172
l : List α
f : α → β
⊢ zip (map (fun x => f x) l) (map (fun x => x) l) = zip (map f l) l
α : Type u
β : Type u_1
γ : Type ?u.88166
δ : Type ?u.88169
ε : Type ?u.88172
l : List α
f : α → β
⊢ map (fun x => (f x, x)) l = zip (map f l) l
rw [← zip_map']
case e_a
α : Type u
β : Type u_1
γ : Type ?u.88166
δ : Type ?u.88169
ε : Type ?u.88172
l : List α
f : α → β
⊢ map (fun x => x) l = l
α : Type u
β : Type u_1
γ : Type ?u.88166
δ : Type ?u.88169
ε : Type ?u.88172
l : List α
f : α → β
⊢ zip (map (fun x => f x) l) (map (fun x => x) l) = zip (map f l) l
congr
no goals
case e_a
α : Type u
β : Type u_1
γ : Type ?u.88166
δ : Type ?u.88169
ε : Type ?u.88172
l : List α
f : α → β
⊢ map (fun x => x) l = l
exact map_id _