no goals
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : α → F β
x : t' α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Equiv.traverse eqv f x) =
    Equiv.traverse eqv ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
simp only [Equiv.traverse, functor_norm]