no goals
α : Type u_2
β : Type u_1
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
x : Option (α × β)
⊢ Option.map (uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)
cases x <;> rfl