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