Commit 2025-06-15 16:47 b3d15f63

chore/refactor(CategoryTheory/Monoidal/Functor): deprime LaxMonoidal and OplaxMonoidal fields (#25766) Discussed in #25628. We use the new language feature that allows to change expliciteness of binders in the definition of classes. Hence, the "primed" versions of Functor.LaxMonoidal.μ, Functor.LaxMonoidal.ε, Functor.OplaxMonoidal.δ and Functor.OplaxMonoidal.η are not needed anymore, as well as the primed version of attached lemmas. This refactor introduces a bunch of deprecations, as simps now become a viable attribute for LaxMonoidal and OplaxMonoidal classes. These attribute are not systematically applied though, as in some cases the name of the lemmas might be bad.