no goals
ι : Type ?u.465338
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as : List α
x✝ : List β
⊢ map₂Left f [] x✝ = (map₂Left' f [] x✝).fst
simp
no goals
ι : Type ?u.465338
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as✝ : List α
a : α
as : List α
⊢ map₂Left f (a :: as) [] = (map₂Left' f (a :: as) []).fst
simp
no goals
ι : Type ?u.465338
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option β → γ
as✝ : List α
a : α
as : List α
b : β
bs : List β
⊢ map₂Left f (a :: as) (b :: bs) = (map₂Left' f (a :: as) (b :: bs)).fst
simp [map₂Left_eq_map₂Left']