α : Type u
β : Type u_1
γ : Type ?u.5392
δ : Type ?u.5395
ε : Type ?u.5398
l₁ : List α
⊢ map Prod.swap [] = zip [] l₁
α : Type u
β : Type u_1
γ : Type ?u.5392
δ : Type ?u.5395
ε : Type ?u.5398
l₁ : List α
⊢ map Prod.swap (zip l₁ []) = zip [] l₁
rw [zip_nil_right]
no goals
α : Type u
β : Type u_1
γ : Type ?u.5392
δ : Type ?u.5395
ε : Type ?u.5398
l₁ : List α
⊢ map Prod.swap [] = zip [] l₁
rfl
no goals
α : Type u
β : Type u_1
γ : Type ?u.5392
δ : Type ?u.5395
ε : Type ?u.5398
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap (zip (a :: l₁) (b :: l₂)) = zip (b :: l₂) (a :: l₁)
simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]