no goals
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)
cases x <;> simp! [functor_norm] <;> rfl