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