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