no goals
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)
cases a <;> cases b <;> cases c <;> simp [h_left_comm]