α : Type u
β : Type u_1
γ : Type ?u.82177
δ : Type ?u.82180
ε : Type ?u.82183
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length as ≤ length bs
⊢ map Prod.fst (zip (head✝¹ :: as) (head✝ :: bs)) = head✝¹ :: as
α : Type u
β : Type u_1
γ : Type ?u.82177
δ : Type ?u.82180
ε : Type ?u.82183
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length (head✝¹ :: as) ≤ length (head✝ :: bs)
⊢ map Prod.fst (zip (head✝¹ :: as) (head✝ :: bs)) = head✝¹ :: as
simp [succ_le_succ_iff] at h
α : Type u
β : Type u_1
γ : Type ?u.82177
δ : Type ?u.82180
ε : Type ?u.82183
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length as ≤ length bs
⊢ (head✝¹, head✝).fst :: map Prod.fst (zip as bs) = head✝¹ :: as
α : Type u
β : Type u_1
γ : Type ?u.82177
δ : Type ?u.82180
ε : Type ?u.82183
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length as ≤ length bs
⊢ map Prod.fst (zip (head✝¹ :: as) (head✝ :: bs)) = head✝¹ :: as
change _ :: map Prod.fst (zip as bs) = _ :: as
no goals
α : Type u
β : Type u_1
γ : Type ?u.82177
δ : Type ?u.82180
ε : Type ?u.82183
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : length as ≤ length bs
⊢ (head✝¹, head✝).fst :: map Prod.fst (zip as bs) = head✝¹ :: as
rw [map_fst_zip as bs h]
no goals
α : Type u
β : Type u_1
γ : Type ?u.82177
δ : Type ?u.82180
ε : Type ?u.82183
a : α
as : List α
h : length (a :: as) ≤ length []
⊢ map Prod.fst (zip (a :: as) []) = a :: as
simp at h