chore: unprime the Prop-valued fields of Mon_Class (#26102)

Now that we have syntax to make `X` explicit in them, there's really no point having the primed fields.

From Toric

Author: YaelDillies

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -44,9 +44,9 @@ variable {R : Type u} [CommRing R]
 noncomputable instance (X : CoalgCat R) : Comon_Class (ModuleCat.of R X) where
   counit := ModuleCat.ofHom Coalgebra.counit
   comul := ModuleCat.ofHom Coalgebra.comul
-  counit_comul' := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
-  comul_counit' := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
-  comul_assoc' := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
+  counit_comul := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
+  comul_counit := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
+  comul_assoc := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
 
 /-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
 @[simps X]

Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

@@ -77,16 +77,16 @@ def ofOplaxFromUnit (F : OplaxFunctor (LocallyDiscrete (Discrete Unit)) B) :
     Comonad (F.map (𝟙 ⟨⟨Unit.unit⟩⟩)) where
   comul := F.map₂ (ρ_ _).inv ≫ F.mapComp _ _
   counit := F.mapId _
-  comul_assoc' := by
+  comul_assoc := by
     simp only [tensorObj_def, MonoidalCategory.whiskerLeft_comp, whiskerLeft_def, Category.assoc,
       MonoidalCategory.comp_whiskerRight, whiskerRight_def, associator_def]
     rw [← F.mapComp_naturality_left_assoc, ← F.mapComp_naturality_right_assoc]
     simp only [whiskerLeft_rightUnitor_inv, PrelaxFunctor.map₂_comp, Category.assoc,
       OplaxFunctor.map₂_associator, whiskerRight_id, Iso.hom_inv_id_assoc]
-  counit_comul' := by
+  counit_comul := by
     simp only [tensorUnit_def, tensorObj_def, whiskerRight_def, Category.assoc, leftUnitor_def]
     rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]
-  comul_counit' := by
+  comul_counit := by
     simp only [tensorUnit_def, tensorObj_def, whiskerLeft_def, rightUnitor_def]
     rw [Category.assoc, F.mapComp_id_right, F.map₂_inv_hom_assoc]
 

Mathlib/CategoryTheory/Monad/EquivMon.lean

@@ -39,7 +39,7 @@ attribute [local instance] endofunctorMonoidalCategory
 instance (M : Monad C) : Mon_Class (M : C ⥤ C) where
   one := M.η
   mul := M.μ
-  mul_assoc' := by ext; simp [M.assoc]
+  mul_assoc := by ext; simp [M.assoc]
 
 /-- To every `Monad C` we associated a monoid object in `C ⥤ C`. -/
 @[simps]

Mathlib/CategoryTheory/Monoidal/Bimon_.lean

@@ -38,33 +38,14 @@ A bimonoid object in a braided category `C` is a object that is simultaneously m
 objects, and structure morphisms of them satisfy appropriate consistency conditions.
 -/
 class Bimon_Class (M : C) extends Mon_Class M, Comon_Class M where
-  /- For the names of the conditions below, the unprimed names are reserved for the version where
-  the argument `M` is explicit. -/
-  mul_comul' : μ[M] ≫ Δ[M] = (Δ[M] ⊗ₘ Δ[M]) ≫ tensorμ M M M M ≫ (μ[M] ⊗ₘ μ[M]) := by aesop_cat
-  one_comul' : η[M] ≫ Δ[M] = η[M ⊗ M] := by aesop_cat
-  mul_counit' : μ[M] ≫ ε[M] = ε[M ⊗ M] := by aesop_cat
-  one_counit' : η[M] ≫ ε[M] = 𝟙 (𝟙_ C) := by aesop_cat
+  mul_comul (M) : μ[M] ≫ Δ[M] = (Δ[M] ⊗ₘ Δ[M]) ≫ tensorμ M M M M ≫ (μ[M] ⊗ₘ μ[M]) := by aesop_cat
+  one_comul (M) : η[M] ≫ Δ[M] = η[M ⊗ M] := by aesop_cat
+  mul_counit (M) : μ[M] ≫ ε[M] = ε[M ⊗ M] := by aesop_cat
+  one_counit (M) : η[M] ≫ ε[M] = 𝟙 (𝟙_ C) := by aesop_cat
 
 namespace Bimon_Class
 
-/- The simp attribute is reserved for the unprimed versions. -/
-attribute [reassoc] mul_comul' one_comul' mul_counit' one_counit'
-
-variable (M : C) [Bimon_Class M]
-
-@[reassoc (attr := simp)]
-theorem mul_comul (M : C) [Bimon_Class M] :
-    μ[M] ≫ Δ[M] = (Δ[M] ⊗ₘ Δ[M]) ≫ tensorμ M M M M ≫ (μ[M] ⊗ₘ μ[M]) :=
-  mul_comul'
-
-@[reassoc (attr := simp)]
-theorem one_comul (M : C) [Bimon_Class M] : η[M] ≫ Δ[M] = η[M ⊗ M] := one_comul'
-
-@[reassoc (attr := simp)]
-theorem mul_counit (M : C) [Bimon_Class M] : μ[M] ≫ ε[M] = ε[M ⊗ M] := mul_counit'
-
-@[reassoc (attr := simp)]
-theorem one_counit (M : C) [Bimon_Class M] : η[M] ≫ ε[M] = 𝟙 (𝟙_ C) := one_counit'
+attribute [reassoc (attr := simp)] mul_comul one_comul mul_counit one_counit
 
 end Bimon_Class
 
@@ -266,11 +247,11 @@ theorem Bimon_ClassAux_comul (M : Bimon_ C) :
 instance (M : Bimon_ C) : Bimon_Class M.X.X where
   counit := ε[M.X].hom
   comul := Δ[M.X].hom
-  counit_comul' := by
+  counit_comul := by
     rw [← Bimon_ClassAux_counit, ← Bimon_ClassAux_comul, Comon_Class.counit_comul]
-  comul_counit' := by
+  comul_counit := by
     rw [← Bimon_ClassAux_counit, ← Bimon_ClassAux_comul, Comon_Class.comul_counit]
-  comul_assoc' := by
+  comul_assoc := by
     simp_rw [← Bimon_ClassAux_comul, Comon_Class.comul_assoc]
 
 attribute [local simp] Mon_Class.tensorObj.one_def in

Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

@@ -49,23 +49,23 @@ def Mon_Class.ofRepresentableBy (F : Cᵒᵖ ⥤ MonCat.{w}) (α : (F ⋙ forget
     Mon_Class X where
   one := α.homEquiv.symm 1
   mul := α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X))
-  one_mul' := by
+  one_mul := by
     apply α.homEquiv.injective
     simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
     simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]
     simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
     simp only [whiskerRight_fst, whiskerRight_snd]
     simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
     simp [leftUnitor_hom]
-  mul_one' := by
+  mul_one := by
     apply α.homEquiv.injective
     simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
     simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]
     simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
     simp only [whiskerLeft_fst, whiskerLeft_snd]
     simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
     simp [rightUnitor_hom]
-  mul_assoc' := by
+  mul_assoc := by
     apply α.homEquiv.injective
     simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
     simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]

Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

@@ -180,7 +180,7 @@ noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
   obj A :=
     { F.mapGrp.obj A.toGrp_ with
       comm :=
-        { mul_comm' := by
+        { mul_comm := by
             dsimp
             rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMon.mul_comm] } }
   map f := F.mapMon.map f

Mathlib/CategoryTheory/Monoidal/CommMon_.lean

@@ -157,7 +157,7 @@ def mapCommMon : CommMon_ C ⥤ CommMon_ D where
   obj A :=
     { F.mapMon.obj A.toMon_ with
       comm :=
-        { mul_comm' := by
+        { mul_comm := by
             dsimp
             rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMon.mul_comm] } }
   map f := F.mapMon.map f

Mathlib/CategoryTheory/Monoidal/Comon_.lean

@@ -40,11 +40,9 @@ class Comon_Class (X : C) where
   counit : X ⟶ 𝟙_ C
   /-- The comultiplication morphism of a comonoid object. -/
   comul : X ⟶ X ⊗ X
-  /- For the names of the conditions below, the unprimed names are reserved for the version where
-  the argument `X` is explicit. -/
-  counit_comul' : comul ≫ counit ▷ X = (λ_ X).inv := by aesop_cat
-  comul_counit' : comul ≫ X ◁ counit = (ρ_ X).inv := by aesop_cat
-  comul_assoc' : comul ≫ X ◁ comul = comul ≫ (comul ▷ X) ≫ (α_ X X X).hom := by aesop_cat
+  counit_comul (X) : comul ≫ counit ▷ X = (λ_ X).inv := by aesop_cat
+  comul_counit (X) : comul ≫ X ◁ counit = (ρ_ X).inv := by aesop_cat
+  comul_assoc (X) : comul ≫ X ◁ comul = comul ≫ (comul ▷ X) ≫ (α_ X X X).hom := by aesop_cat
 
 namespace Comon_Class
 
@@ -53,27 +51,15 @@ namespace Comon_Class
 @[inherit_doc] scoped notation "ε" => Comon_Class.counit
 @[inherit_doc] scoped notation "ε["M"]" => Comon_Class.counit (X := M)
 
-/- The simp attribute is reserved for the unprimed versions. -/
-attribute [reassoc] counit_comul' comul_counit' comul_assoc'
-
-@[reassoc (attr := simp)]
-theorem counit_comul (X : C) [Comon_Class X] : Δ ≫ ε ▷ X = (λ_ X).inv := counit_comul'
-
-@[reassoc (attr := simp)]
-theorem comul_counit (X : C) [Comon_Class X] : Δ ≫ X ◁ ε = (ρ_ X).inv := comul_counit'
-
-@[reassoc (attr := simp)]
-theorem comul_assoc (X : C) [Comon_Class X] :
-    Δ ≫ X ◁ Δ = Δ ≫ Δ ▷ X ≫ (α_ X X X).hom :=
-  comul_assoc'
+attribute [reassoc (attr := simp)] counit_comul comul_counit comul_assoc
 
 @[simps]
 instance (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] : Comon_Class (𝟙_ C) where
   counit := 𝟙 _
   comul := (λ_ _).inv
-  counit_comul' := by monoidal_coherence
-  comul_counit' := by monoidal_coherence
-  comul_assoc' := by monoidal_coherence
+  counit_comul := by monoidal_coherence
+  comul_counit := by monoidal_coherence
+  comul_assoc := by monoidal_coherence
 
 end Comon_Class
 
@@ -256,13 +242,13 @@ open Opposite
 abbrev Comon_ToMon_OpOpObjMon (A : Comon_ C) : Mon_Class (op A.X) where
   one := ε[A.X].op
   mul := Δ[A.X].op
-  one_mul' := by
+  one_mul := by
     rw [← op_whiskerRight, ← op_comp, counit_comul]
     rfl
-  mul_one' := by
+  mul_one := by
     rw [← op_whiskerLeft, ← op_comp, comul_counit]
     rfl
-  mul_assoc' := by
+  mul_assoc := by
     rw [← op_inv_associator, ← op_whiskerRight, ← op_comp, ← op_whiskerLeft, ← op_comp,
       comul_assoc_flip, op_comp, op_comp_assoc]
     rfl
@@ -290,9 +276,9 @@ The contravariant functor turning comonoid objects into monoid objects in the op
 abbrev Mon_OpOpToComonObjComon (A : Mon_ (Cᵒᵖ)) : Comon_Class (unop A.X) where
   counit := η[A.X].unop
   comul := μ[A.X].unop
-  counit_comul' := by rw [← unop_whiskerRight, ← unop_comp, Mon_Class.one_mul]; rfl
-  comul_counit' := by rw [← unop_whiskerLeft, ← unop_comp, Mon_Class.mul_one]; rfl
-  comul_assoc' := by
+  counit_comul := by rw [← unop_whiskerRight, ← unop_comp, Mon_Class.one_mul]; rfl
+  comul_counit := by rw [← unop_whiskerLeft, ← unop_comp, Mon_Class.mul_one]; rfl
+  comul_assoc := by
     rw [← unop_whiskerRight, ← unop_whiskerLeft, ← unop_comp_assoc, ← unop_comp,
       Mon_Class.mul_assoc_flip]
     rfl
@@ -401,13 +387,13 @@ abbrev obj.instComon_Class (A : C) [Comon_Class A] (F : C ⥤ D) [F.OplaxMonoida
     Comon_Class (F.obj A) where
   counit := F.map ε[A] ≫ η F
   comul := F.map Δ[A] ≫ δ F _ _
-  counit_comul' := by
+  counit_comul := by
     simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
       ← F.map_comp_assoc, counit_comul]
-  comul_counit' := by
+  comul_counit := by
     simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc,
       right_unitality, ← F.map_comp_assoc, comul_counit]
-  comul_assoc' := by
+  comul_assoc := by
     simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc,
       MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc,
       ← F.map_comp_assoc, comul_assoc, F.map_comp, Category.assoc, associativity]

Mathlib/CategoryTheory/Monoidal/Hopf_.lean

@@ -32,26 +32,16 @@ A Hopf monoid in a braided category `C` is a bimonoid object in `C` equipped wit
 class Hopf_Class (X : C) extends Bimon_Class X where
   /-- The antipode is an endomorphism of the underlying object of the Hopf monoid. -/
   antipode : X ⟶ X
-  /- For the names of the conditions below, the unprimed names are reserved for the version where
-  the argument `X` is explicit. -/
-  antipode_left' : Δ ≫ antipode ▷ X ≫ μ = ε ≫ η := by aesop_cat
-  antipode_right' : Δ ≫ X ◁ antipode ≫ μ = ε ≫ η := by aesop_cat
+  antipode_left (X) : Δ ≫ antipode ▷ X ≫ μ = ε ≫ η := by aesop_cat
+  antipode_right (X) : Δ ≫ X ◁ antipode ≫ μ = ε ≫ η := by aesop_cat
 
 namespace Hopf_Class
 
 @[inherit_doc] scoped notation "𝒮" => Hopf_Class.antipode
 @[inherit_doc] scoped notation "𝒮["M"]" => Hopf_Class.antipode (X := M)
 
-/- The simp attribute is reserved for the unprimed versions. -/
-attribute [reassoc] antipode_left' antipode_right'
+attribute [reassoc (attr := simp)] antipode_left antipode_right
 
-/-- The object is provided as an explicit argument. -/
-@[reassoc (attr := simp)]
-theorem antipode_left (X : C) [Hopf_Class X] : Δ ≫ 𝒮 ▷ X ≫ μ = ε ≫ η := antipode_left'
-
-/-- The object is provided as an explicit argument. -/
-@[reassoc (attr := simp)]
-theorem antipode_right (X : C) [Hopf_Class X] : Δ ≫ X ◁ 𝒮 ≫ μ = ε ≫ η := antipode_right'
 
 end Hopf_Class
 

Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean

@@ -47,9 +47,9 @@ def functorObjObj (A : C ⥤ D) [Mon_Class A] (X : C) : Mon_ D where
   mon :=
   { one := η[A].app X
     mul := μ[A].app X
-    one_mul' := congr_app (one_mul A) X
-    mul_one' := congr_app (mul_one A) X
-    mul_assoc' := congr_app (mul_assoc A) X }
+    one_mul := congr_app (one_mul A) X
+    mul_one := congr_app (mul_one A) X
+    mul_assoc := congr_app (mul_assoc A) X }
 
 /-- A monoid object in a functor category induces a functor to the category of monoid objects. -/
 @[simps]
@@ -136,9 +136,9 @@ def functorObjObj (A : C ⥤ D) [Comon_Class A] (X : C) : Comon_ D where
   comon :=
   { counit := ε[A].app X
     comul := Δ[A].app X
-    counit_comul' := congr_app (counit_comul A) X
-    comul_counit' := congr_app (comul_counit A) X
-    comul_assoc' := congr_app (comul_assoc A) X }
+    counit_comul := congr_app (counit_comul A) X
+    comul_counit := congr_app (comul_counit A) X
+    comul_assoc := congr_app (comul_assoc A) X }
 
 /--
 A comonoid object in a functor category induces a functor to the category of comonoid objects.
@@ -235,7 +235,7 @@ def functor : CommMon_ (C ⥤ D) ⥤ C ⥤ CommMon_ D where
     { (monFunctorCategoryEquivalence C D).functor.obj A.toMon_ with
       obj := fun X =>
         { ((monFunctorCategoryEquivalence C D).functor.obj A.toMon_).obj X with
-          comm := { mul_comm' := congr_app (IsCommMon.mul_comm A.X) X } } }
+          comm := { mul_comm := congr_app (IsCommMon.mul_comm A.X) X } } }
   map f := { app := fun X => ((monFunctorCategoryEquivalence C D).functor.map f).app X }
 
 /-- Functor translating a functor into the category of commutative monoid objects
@@ -245,7 +245,7 @@ to a commutative monoid object in the functor category
 def inverse : (C ⥤ CommMon_ D) ⥤ CommMon_ (C ⥤ D) where
   obj F :=
     { (monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon_.forget₂Mon_ D) with
-      comm := { mul_comm' := by ext X; exact IsCommMon.mul_comm (F.obj X).X } }
+      comm := { mul_comm := by ext X; exact IsCommMon.mul_comm (F.obj X).X } }
   map α := (monFunctorCategoryEquivalence C D).inverse.map (whiskerRight α _)
 
 /-- The unit for the equivalence `CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D`.