no goals
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
a : Option α
b : Option β
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f a b = map₂ g b a
cases a <;> cases b <;> simp [h_comm]