no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a✝ : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = map₂ (fun a b => f b a) b a
cases a <;> cases b <;> rfl