α : Type u
β : Type u_1
γ : Type ?u.86201
δ : Type ?u.86204
ε : Type ?u.86207
l₁ : List α
h : length l₁ ≤ length []
⊢ (unzip (zip [] [])).fst = []
α : Type u
β : Type u_1
γ : Type ?u.86201
δ : Type ?u.86204
ε : Type ?u.86207
l₁ : List α
h : length l₁ ≤ length []
⊢ (unzip (zip l₁ [])).fst = l₁
rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]
no goals
α : Type u
β : Type u_1
γ : Type ?u.86201
δ : Type ?u.86204
ε : Type ?u.86207
l₁ : List α
h : length l₁ ≤ length []
⊢ (unzip (zip [] [])).fst = []
rfl
no goals
α : Type u
β : Type u_1
γ : Type ?u.86201
δ : Type ?u.86204
ε : Type ?u.86207
a : α
l₁ : List α
b : β
l₂ : List β
h : length (a :: l₁) ≤ length (b :: l₂)
⊢ (unzip (zip (a :: l₁) (b :: l₂))).fst = a :: l₁
simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]