map_eq_bind_pure_comp

theorem map_eq_bind_pure_comp : ∀ {α β : Type u} (m : Type u → Type v) [inst : Monad m] [inst_1 : LawfulMonad m] (f : α → β) (x : m α), f <$> x = x >>= pure ∘ f

This theorem, `map_eq_bind_pure_comp`, states that for any monad `m`, any types `α` and `β`, and any function `f` from `α` to `β`, the operation of mapping `f` over a monadic value `x` (`f <$> x`) is equivalent to first applying `f` to `x` using the monadic bind operator (`>>=`), and then lifting the result into the monadic context with `pure`. In mathematical terms, this is an expression of the interchange law for monads, which dictates how the operations of bind and map interact.

More concisely: For any monad `m`, type `α`, function `f : α → β`, and value `x : m α`, `f <$> x` is equivalent to `lift (f x)` where `lift = pure . f`.