α : Type u
β : Type u_1
γ : Type ?u.89441
δ : Type ?u.89444
ε : Type ?u.89447
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l
α : Type u
β : Type u_1
γ : Type ?u.89441
δ : Type ?u.89444
ε : Type ?u.89447
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith f l l' = zipWith f l' l
rw [zipWith_comm]
no goals
α : Type u
β : Type u_1
γ : Type ?u.89441
δ : Type ?u.89444
ε : Type ?u.89447
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : List α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l
simp only [comm]