mathlib3

6b59725c - chore(control/traversable/{basic,equiv,instances,lemmas}): linting (#4444)

chore(control/traversable/{basic,equiv,instances,lemmas}): linting (#4444) The `nolint`s in `instances.lean` are there because all the arguments need to be there for `is_lawful_traversable`. In the same file, I moved `traverse_map` because it does not need the `is_lawful_applicative` instances.