Traversable.traverse_map

theorem Traversable.traverse_map : ∀ {t : Type u → Type u} [inst : Traversable t] [inst_1 : LawfulTraversable t] {F : Type u → Type u} [inst_2 : Applicative F] [inst_3 : LawfulApplicative F] {α β γ : Type u} (f : β → F γ) (g : α → β) (x : t α), traverse f (g <$> x) = traverse (f ∘ g) x

The theorem `Traversable.traverse_map` states that for any type `t` that is `Traversable` and obeys the laws of a `LawfulTraversable`, for any `Applicative` functor `F` that obeys the laws of a `LawfulApplicative`, and for any three types `α`, `β`, and `γ`, if you have a function `f` from `β` to `F γ` and a function `g` from `α` to `β`, then traversing over the result of mapping `g` over `x` (where `x` is of type `t α`) with function `f` is equivalent to traversing over `x` with the composite function `f ∘ g`. This is a property of traversable functors in functional programming and is closely related to the "map" operation of functors and the "traverse" operation of traversable functors.

More concisely: For any `Traversable t` and `LawfulTraversable t`, `LawfulApplicative F`, functions `f : β -> F γ` and `g : α -> β`, the traversal of `f . map g` over `t x` equals the traversal of `x` with `f . (.) g`.