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