α : Type u
β : Type u_1
γ : Type ?u.85279
δ : Type ?u.85282
ε : Type ?u.85285
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = Prod.swap (map Prod.fst l, map Prod.snd l)
α : Type u
β : Type u_1
γ : Type ?u.85279
δ : Type ?u.85282
ε : Type ?u.85285
l : List (α × β)
⊢ unzip (map Prod.swap l) = Prod.swap (unzip l)
simp only [unzip_eq_map, map_map]
no goals
α : Type u
β : Type u_1
γ : Type ?u.85279
δ : Type ?u.85282
ε : Type ?u.85285
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = Prod.swap (map Prod.fst l, map Prod.snd l)
rfl