no goals
α : Type u
β : Type u_1
γ : Type ?u.87252
δ : Type ?u.87255
ε : Type ?u.87258
l₁ : List α
l₂ : List β
h : length l₁ = length l₂
⊢ unzip (zip l₁ l₂) = (l₁, l₂)
rw [← Prod.mk.eta (p := unzip (zip l₁ l₂)),
  unzip_zip_left (le_of_eq h), unzip_zip_right (ge_of_eq h)]