lean4#7356 monadic theorems about mapM, foldM, etc

Stream: PR reviews

[Eric Wieser]

Posting here since some batteries contributors may also be interested in lean4#7356, which provides theorems like l.foldrM (pure <| f · ·) b = pure (l.foldr f b) for lawful monads.

This is against core rather than batteries because I plan to use it to clean up the simp set around the Id monad.