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