case h.e'_2.h.e'_5
α : Type u
β : Type u_3
γ : Type u_2
δ : Type u_1
ε : Type ?u.50129
f : α → β → γ
l : List α
g : δ → β
l' : List δ
⊢ l = map id l
α : Type u
β : Type u_3
γ : Type u_2
δ : Type u_1
ε : Type ?u.50129
f : α → β → γ
l : List α
g : δ → β
l' : List δ
⊢ zipWith f l (map g l') = zipWith (fun x => f x ∘ g) l l'
convert List.zipWith_map f id g l l'
no goals
case h.e'_2.h.e'_5
α : Type u
β : Type u_3
γ : Type u_2
δ : Type u_1
ε : Type ?u.50129
f : α → β → γ
l : List α
g : δ → β
l' : List δ
⊢ l = map id l
exact Eq.symm (List.map_id _)