mathlib3

7c77279e - feat(category_theory/monad): use bundled monads everywhere (#5889)

feat(category_theory/monad): use bundled monads everywhere (#5889) This PR makes bundled monads the default (adapting definitions by @adamtopaz). The main motivation for this is that the category of algebras for a monad is currently not "hygienic" in that isomorphic monads don't have equivalent Eilenberg-Moore categories, but further that the notion of monad isomorphism is tricky to express, in particular this makes the definition of a monadic functor not preserved by isos either despite not explicitly having monads or algebras in the type. We can now say: ``` @[simps] def algebra_equiv_of_iso_monads {T₁ T₂ : monad C} (h : T₁ ≅ T₂) : algebra T₁ ≌ algebra T₂ := ``` Other than this new data, virtually everything in this PR is just refactoring - in particular there's quite a bit of golfing and generalisation possible, but to keep the diff here minimal I'll do those in later PRs