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