chore: fix simps projections in CategoryTheory.Monad.Basic (#3269)

This fixes a regression of `@[simps]` to `@[simp]` from #2969, per [zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.232969.20simps.20bug.3F.20.28Monad.2EBasic.29).

There are a few incidental changes to `@[simps]` arguments in this PR, just removing arguments that had no effect on behaviour.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

@@ -71,7 +71,7 @@ variable (C : Type u) [Category.{v} C]
 /-- We call a category `NonPreadditiveAbelian` if it has a zero object, kernels, cokernels, binary
     products and coproducts, and every monomorphism and every epimorphism is normal. -/
 class NonPreadditiveAbelian extends HasZeroMorphisms C, NormalMonoCategory C,
-  NormalEpiCategory C where
+    NormalEpiCategory C where
   [has_zero_object : HasZeroObject C]
   [has_kernels : HasKernels C]
   [has_cokernels : HasCokernels C]

Mathlib/CategoryTheory/Bicategory/Functor.lean

@@ -85,13 +85,12 @@ variable {D : Type u₃} [Quiver.{v₃ + 1} D] [∀ a b : D, Quiver.{w₃ + 1} (
 structure PrelaxFunctor (B : Type u₁) [Quiver.{v₁ + 1} B] [∀ a b : B, Quiver.{w₁ + 1} (a ⟶ b)]
   (C : Type u₂) [Quiver.{v₂ + 1} C] [∀ a b : C, Quiver.{w₂ + 1} (a ⟶ b)] extends
   Prefunctor B C where
+  /-- The action of a prelax functor on 2-morphisms. -/
   map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (map f ⟶ map g)
 #align category_theory.prelax_functor CategoryTheory.PrelaxFunctor
 
 initialize_simps_projections PrelaxFunctor (+toPrefunctor, -obj, -map)
 
-attribute [nolint docBlame] CategoryTheory.PrelaxFunctor.map₂
-
 /-- The prefunctor between the underlying quivers. -/
 add_decl_doc PrelaxFunctor.toPrefunctor
 
@@ -371,7 +370,7 @@ associator, the left unitor, and the right unitor modulo some adjustments of dom
 of 2-morphisms.
 -/
 structure Pseudofunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u₂)
-  [Bicategory.{w₂, v₂} C] extends PrelaxFunctor B C where
+    [Bicategory.{w₂, v₂} C] extends PrelaxFunctor B C where
   mapId (a : B) : map (𝟙 a) ≅ 𝟙 (obj a)
   mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : map (f ≫ g) ≅ map f ≫ map g
   map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f) := by aesop_cat

Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

@@ -489,7 +489,7 @@ theorem Cofork.IsColimit.existsUnique {s : Cofork f g} (hs : IsColimit s) {W : C
 
 /-- This is a slightly more convenient method to verify that a fork is a limit cone. It
     only asks for a proof of facts that carry any mathematical content -/
-@[simps lift]
+@[simps]
 def Fork.IsLimit.mk (t : Fork f g) (lift : ∀ s : Fork f g, s.pt ⟶ t.pt)
     (fac : ∀ s : Fork f g, lift s ≫ Fork.ι t = Fork.ι s)
     (uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt) (_ : m ≫ t.ι = s.ι), m = lift s) : IsLimit t :=

Mathlib/CategoryTheory/Monad/Basic.lean

@@ -183,16 +183,21 @@ structure MonadHom (T₁ T₂ : Monad C) extends NatTrans (T₁ : C ⥤ C) T₂
     aesop_cat
 #align category_theory.monad_hom CategoryTheory.MonadHom
 
+initialize_simps_projections MonadHom (+toNatTrans, -app)
+
 /-- A morphism of comonads is a natural transformation compatible with ε and δ. -/
 @[ext]
 structure ComonadHom (M N : Comonad C) extends NatTrans (M : C ⥤ C) N where
   app_ε : ∀ X, app X ≫ N.ε.app X = M.ε.app X := by aesop_cat
   app_δ : ∀ X, app X ≫ N.δ.app X = M.δ.app X ≫ app _ ≫ (N : C ⥤ C).map (app X) := by aesop_cat
 #align category_theory.comonad_hom CategoryTheory.ComonadHom
 
+initialize_simps_projections ComonadHom (+toNatTrans, -app)
+
 attribute [reassoc (attr := simp)] MonadHom.app_η MonadHom.app_μ
 attribute [reassoc (attr := simp)] ComonadHom.app_ε ComonadHom.app_δ
 
+
 instance : Category (Monad C) where
   Hom := MonadHom
   id M := { toNatTrans := 𝟙 (M : C ⥤ C) }
@@ -253,10 +258,9 @@ theorem comp_toNatTrans {T₁ T₂ T₃ : Comonad C} (f : T₁ ⟶ T₂) (g : T
   rfl
 #align category_theory.comp_to_nat_trans CategoryTheory.comp_toNatTrans
 
--- porting note: was @[simps]
 /-- Construct a monad isomorphism from a natural isomorphism of functors where the forward
 direction is a monad morphism. -/
-@[simp]
+@[simps]
 def MonadIso.mk {M N : Monad C} (f : (M : C ⥤ C) ≅ N)
     (f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X)
     (f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X =
@@ -275,10 +279,9 @@ def MonadIso.mk {M N : Monad C} (f : (M : C ⥤ C) ≅ N)
         simp }
 #align category_theory.monad_iso.mk CategoryTheory.MonadIso.mk
 
--- porting note: was @[simps]
 /-- Construct a comonad isomorphism from a natural isomorphism of functors where the forward
 direction is a comonad morphism. -/
-@[simp]
+@[simps]
 def ComonadIso.mk {M N : Comonad C} (f : (M : C ⥤ C) ≅ N)
     (f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X)
     (f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X =

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -95,6 +95,8 @@ structure LaxMonoidalFunctor extends C ⥤ D where
 
 -- Porting note: todo: remove this configuration and use the default configuration.
 -- We keep this to be consistent with Lean 3.
+-- See also `initialize_simps_projections MonoidalFunctor` below.
+-- This may require waiting on https://github.com/leanprover-community/mathlib4/pull/2936
 initialize_simps_projections LaxMonoidalFunctor (+toFunctor, -obj, -map)
 
 --Porting note: was `[simp, reassoc.1]`
@@ -151,6 +153,7 @@ structure MonoidalFunctor extends LaxMonoidalFunctor.{v₁, v₂} C D where
   μ_isIso : ∀ X Y : C, IsIso (μ X Y) := by infer_instance
 #align category_theory.monoidal_functor CategoryTheory.MonoidalFunctor
 
+-- See porting note on `initialize_simps_projections LaxMonoidalFunctor`
 initialize_simps_projections MonoidalFunctor (+toLaxMonoidalFunctor, -obj, -map, -ε, -μ)
 
 attribute [instance] MonoidalFunctor.ε_isIso MonoidalFunctor.μ_isIso

Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

@@ -57,6 +57,8 @@ structure MonoidalNatTrans (F G : LaxMonoidalFunctor C D) extends
 attribute [reassoc (attr := simp)] MonoidalNatTrans.tensor
 attribute [reassoc (attr := simp)] MonoidalNatTrans.unit
 
+initialize_simps_projections MonoidalNatTrans (+toNatTrans, -app)
+
 #align category_theory.monoidal_nat_trans.unit CategoryTheory.MonoidalNatTrans.unit
 #align category_theory.monoidal_nat_trans.unit_assoc CategoryTheory.MonoidalNatTrans.unit_assoc
 #align category_theory.monoidal_nat_trans.tensor CategoryTheory.MonoidalNatTrans.tensor