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