no goals
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f x) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
cases x <;> simp! [Sum.traverse, functor_norm, ApplicativeTransformation.preserves_map,
  ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure]