α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
x✝¹ : List α
x✝ : length [] ≤ length x✝¹
⊢ map Prod.snd [] = []
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
x✝¹ : List α
x✝ : length [] ≤ length x✝¹
⊢ map Prod.snd (zip x✝¹ []) = []
rw [zip_nil_right]
no goals
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
x✝¹ : List α
x✝ : length [] ≤ length x✝¹
⊢ map Prod.snd [] = []
rfl
no goals
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
b : β
bs : List β
h : length (b :: bs) ≤ length []
⊢ map Prod.snd (zip [] (b :: bs)) = b :: bs
simp at h
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ map Prod.snd (zip (a :: as) (b :: bs)) = b :: bs
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
a : α
as : List α
b : β
bs : List β
h : length (b :: bs) ≤ length (a :: as)
⊢ map Prod.snd (zip (a :: as) (b :: bs)) = b :: bs
simp [succ_le_succ_iff] at h
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ (a, b).snd :: map Prod.snd (zip as bs) = b :: bs
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ map Prod.snd (zip (a :: as) (b :: bs)) = b :: bs
change _ :: map Prod.snd (zip as bs) = _ :: bs
no goals
α : Type u
β : Type u_1
γ : Type ?u.83109
δ : Type ?u.83112
ε : Type ?u.83115
a : α
as : List α
b : β
bs : List β
h : length bs ≤ length as
⊢ (a, b).snd :: map Prod.snd (zip as bs) = b :: bs
rw [map_snd_zip as bs h]