no goals
ι : Type ?u.466133
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as : List α
x✝ : length [] ≤ length []
⊢ map₂Left f [] [] = zipWith (fun a b => f a (some b)) [] []
simp
no goals
ι : Type ?u.466133
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as : List α
head✝ : β
tail✝ : List β
x✝ : length [] ≤ length (head✝ :: tail✝)
⊢ map₂Left f [] (head✝ :: tail✝) = zipWith (fun a b => f a (some b)) [] (head✝ :: tail✝)
simp
no goals
ι : Type ?u.466133
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as✝ : List α
a : α
as : List α
h : length (a :: as) ≤ length []
⊢ map₂Left f (a :: as) [] = zipWith (fun a b => f a (some b)) (a :: as) []
simp at h
ι : Type ?u.466133
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as✝ : List α
a : α
as : List α
b : β
bs : List β
h : length as ≤ length bs
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)
ι : Type ?u.466133
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as✝ : List α
a : α
as : List α
b : β
bs : List β
h : length (a :: as) ≤ length (b :: bs)
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)
simp [Nat.succ_le_succ_iff] at h
no goals
ι : Type ?u.466133
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as✝ : List α
a : α
as : List α
b : β
bs : List β
h : length as ≤ length bs
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)
simp [h, map₂Left_eq_zipWith]