chore: rename private mk to of for some bundled categories (#31622)

In a few places we can replace `private mk` by `of` and save some lines. Whilst searching for this I also replaced a few non-private `mk` with `of` where possible.

Author: callesonne

Mathlib/Algebra/Category/BoolRing.lean

@@ -24,7 +24,8 @@ open CategoryTheory Order
 
 /-- The category of Boolean rings. -/
 structure BoolRing where
-  private mk ::
+  /-- Construct a bundled `BoolRing` from a `BooleanRing`. -/
+  of ::
   /-- The underlying type. -/
   carrier : Type u
   [booleanRing : BooleanRing carrier]
@@ -40,10 +41,6 @@ attribute [coe] carrier
 
 attribute [instance] booleanRing
 
-/-- Construct a bundled `BoolRing` from a `BooleanRing`. -/
-abbrev of (α : Type*) [BooleanRing α] : BoolRing :=
-  ⟨α⟩
-
 theorem coe_of (α : Type*) [BooleanRing α] : ↥(of α) = α :=
   rfl
 

Mathlib/Algebra/Category/GrpWithZero.lean

@@ -21,6 +21,8 @@ open CategoryTheory
 
 /-- The category of groups with zero. -/
 structure GrpWithZero where
+  /-- Construct a bundled `GrpWithZero` from a `GroupWithZero`. -/
+  of ::
   /-- The underlying group with zero. -/
   carrier : Type*
   [str : GroupWithZero carrier]
@@ -32,10 +34,6 @@ namespace GrpWithZero
 instance : CoeSort GrpWithZero Type* :=
   ⟨carrier⟩
 
-/-- Construct a bundled `GrpWithZero` from a `GroupWithZero`. -/
-abbrev of (α : Type*) [GroupWithZero α] : GrpWithZero where
-  carrier := α
-
 instance : Inhabited GrpWithZero :=
   ⟨of (WithZero PUnit)⟩
 

Mathlib/Algebra/Category/HopfAlgCat/Basic.lean

@@ -24,6 +24,7 @@ variable (R : Type u) [CommRing R]
 
 /-- The category of `R`-Hopf algebras. -/
 structure HopfAlgCat where
+  private mk ::
   /-- The underlying type. -/
   carrier : Type v
   [instRing : Ring carrier]

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -26,7 +26,9 @@ open CategoryTheory
 
 /-- The category of semirings. -/
 structure SemiRingCat where
-  private mk ::
+  /-- The object in the category of semirings associated to a type equipped with the appropriate
+  typeclasses. -/
+  of ::
   /-- The underlying type. -/
   carrier : Type u
   [semiring : Semiring carrier]
@@ -42,11 +44,6 @@ instance : CoeSort (SemiRingCat) (Type u) :=
 
 attribute [coe] SemiRingCat.carrier
 
-/-- The object in the category of R-algebras associated to a type equipped with the appropriate
-typeclasses. This is the preferred way to construct a term of `SemiRingCat`. -/
-abbrev of (R : Type u) [Semiring R] : SemiRingCat :=
-  ⟨R⟩
-
 lemma coe_of (R : Type u) [Semiring R] : (of R : Type u) = R :=
   rfl
 
@@ -176,7 +173,9 @@ end SemiRingCat
 
 /-- The category of rings. -/
 structure RingCat where
-  private mk ::
+  /-- The object in the category of rings associated to a type equipped with the appropriate
+  typeclasses. -/
+  of ::
   /-- The underlying type. -/
   carrier : Type u
   [ring : Ring carrier]
@@ -192,11 +191,6 @@ instance : CoeSort (RingCat) (Type u) :=
 
 attribute [coe] RingCat.carrier
 
-/-- The object in the category of R-algebras associated to a type equipped with the appropriate
-typeclasses. This is the preferred way to construct a term of `RingCat`. -/
-abbrev of (R : Type u) [Ring R] : RingCat :=
-  ⟨R⟩
-
 lemma coe_of (R : Type u) [Ring R] : (of R : Type u) = R :=
   rfl
 
@@ -338,7 +332,9 @@ end RingCat
 
 /-- The category of commutative semirings. -/
 structure CommSemiRingCat where
-  private mk ::
+  /-- The object in the category of commutative semirings associated to a type equipped with the
+  appropriate typeclasses. -/
+  of ::
   /-- The underlying type. -/
   carrier : Type u
   [commSemiring : CommSemiring carrier]
@@ -354,11 +350,6 @@ instance : CoeSort (CommSemiRingCat) (Type u) :=
 
 attribute [coe] CommSemiRingCat.carrier
 
-/-- The object in the category of R-algebras associated to a type equipped with the appropriate
-typeclasses. This is the preferred way to construct a term of `CommSemiRingCat`. -/
-abbrev of (R : Type u) [CommSemiring R] : CommSemiRingCat :=
-  ⟨R⟩
-
 lemma coe_of (R : Type u) [CommSemiring R] : (of R : Type u) = R :=
   rfl
 
@@ -499,7 +490,9 @@ end CommSemiRingCat
 
 /-- The category of commutative rings. -/
 structure CommRingCat where
-  private mk ::
+  /-- The object in the category of commutative rings associated to a type equipped with the
+  appropriate typeclasses. -/
+  of ::
   /-- The underlying type. -/
   carrier : Type u
   [commRing : CommRing carrier]
@@ -515,11 +508,6 @@ instance : CoeSort (CommRingCat) (Type u) :=
 
 attribute [coe] CommRingCat.carrier
 
-/-- The object in the category of R-algebras associated to a type equipped with the appropriate
-typeclasses. This is the preferred way to construct a term of `CommRingCat`. -/
-abbrev of (R : Type u) [CommRing R] : CommRingCat :=
-  ⟨R⟩
-
 lemma coe_of (R : Type u) [CommRing R] : (of R : Type u) = R :=
   rfl
 

Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean

@@ -24,6 +24,8 @@ open CategoryTheory
 
 /-- The category of seminormed abelian groups and bounded group homomorphisms. -/
 structure SemiNormedGrp : Type (u + 1) where
+  /-- Construct a bundled `SemiNormedGrp` from the underlying type and typeclass. -/
+  of ::
   /-- The underlying seminormed abelian group. -/
   carrier : Type u
   [str : SeminormedAddCommGroup carrier]
@@ -35,10 +37,6 @@ namespace SemiNormedGrp
 instance : CoeSort SemiNormedGrp Type* where
   coe X := X.carrier
 
-/-- Construct a bundled `SemiNormedGrp` from the underlying type and typeclass. -/
-abbrev of (M : Type u) [SeminormedAddCommGroup M] : SemiNormedGrp where
-  carrier := M
-
 /-- The type of morphisms in `SemiNormedGrp` -/
 @[ext]
 structure Hom (M N : SemiNormedGrp.{u}) where
@@ -209,6 +207,8 @@ end SemiNormedGrp
 which we shall equip with the category structure consisting only of the norm non-increasing maps.
 -/
 structure SemiNormedGrp₁ : Type (u + 1) where
+  /-- Construct a bundled `SemiNormedGrp₁` from the underlying type and typeclass. -/
+  of ::
   /-- The underlying seminormed abelian group. -/
   carrier : Type u
   [str : SeminormedAddCommGroup carrier]
@@ -220,10 +220,6 @@ namespace SemiNormedGrp₁
 instance : CoeSort SemiNormedGrp₁ Type* where
   coe X := X.carrier
 
-/-- Construct a bundled `SemiNormedGrp₁` from the underlying type and typeclass. -/
-abbrev of (M : Type u) [SeminormedAddCommGroup M] : SemiNormedGrp₁ where
-  carrier := M
-
 /-- The type of morphisms in `SemiNormedGrp₁` -/
 @[ext]
 structure Hom (M N : SemiNormedGrp₁.{u}) where

Mathlib/CategoryTheory/FintypeCat.lean

@@ -25,6 +25,8 @@ open CategoryTheory
 
 /-- The category of finite types. -/
 structure FintypeCat where
+  /-- Construct a bundled `FintypeCat` from the underlying type and typeclass. -/
+  of ::
   /-- The underlying type. -/
   carrier : Type*
   [str : Fintype carrier]
@@ -36,10 +38,6 @@ namespace FintypeCat
 instance instCoeSort : CoeSort FintypeCat Type* :=
   ⟨carrier⟩
 
-/-- Construct a bundled `FintypeCat` from the underlying type and typeclass. -/
-abbrev of (X : Type*) [Fintype X] : FintypeCat where
-  carrier := X
-
 instance : Inhabited FintypeCat :=
   ⟨of PEmpty⟩
 

Mathlib/MeasureTheory/Category/MeasCat.lean

@@ -37,6 +37,8 @@ universe u v
 
 /-- The category of measurable spaces and measurable functions. -/
 structure MeasCat : Type (u + 1) where
+  /-- Construct a bundled `MeasCat` from the underlying type and the typeclass. -/
+  of ::
   /-- The underlying measurable space. -/
   carrier : Type u
   [str : MeasurableSpace carrier]
@@ -48,10 +50,6 @@ namespace MeasCat
 instance : CoeSort MeasCat Type* :=
   ⟨carrier⟩
 
-/-- Construct a bundled `MeasCat` from the underlying type and the typeclass. -/
-abbrev of (α : Type u) [ms : MeasurableSpace α] : MeasCat where
-  carrier := α
-
 theorem coe_of (X : Type u) [MeasurableSpace X] : (of X : Type u) = X :=
   rfl
 

Mathlib/Order/Category/BoolAlg.lean

@@ -21,6 +21,8 @@ open CategoryTheory
 
 /-- The category of Boolean algebras. -/
 structure BoolAlg where
+  /-- Construct a bundled `BoolAlg` from the underlying type and typeclass. -/
+  of ::
   /-- The underlying Boolean algebra. -/
   carrier : Type*
   [str : BooleanAlgebra carrier]
@@ -36,9 +38,6 @@ instance : CoeSort BoolAlg (Type _) :=
 
 attribute [coe] BoolAlg.carrier
 
-/-- Construct a bundled `BoolAlg` from the underlying type and typeclass. -/
-abbrev of (X : Type*) [BooleanAlgebra X] : BoolAlg := ⟨X⟩
-
 /-- The type of morphisms in `BoolAlg R`. -/
 @[ext]
 structure Hom (X Y : BoolAlg.{u}) where

Mathlib/Order/Category/CompleteLat.lean

@@ -19,6 +19,8 @@ open CategoryTheory
 
 /-- The category of complete lattices. -/
 structure CompleteLat where
+  /-- Construct a bundled `CompleteLat` from the underlying type and typeclass. -/
+  of ::
   /-- The underlying lattice. -/
   (carrier : Type*)
   [str : CompleteLattice carrier]
@@ -34,9 +36,6 @@ instance : CoeSort CompleteLat (Type _) :=
 
 attribute [coe] CompleteLat.carrier
 
-/-- Construct a bundled `CompleteLat` from the underlying type and typeclass. -/
-abbrev of (X : Type*) [CompleteLattice X] : CompleteLat := ⟨X⟩
-
 theorem coe_of (α : Type*) [CompleteLattice α] : ↥(of α) = α :=
   rfl
 

Mathlib/Order/Category/Frm.lean

@@ -24,6 +24,8 @@ open CategoryTheory Order
 
 /-- The category of frames. -/
 structure Frm where
+  /-- Construct a bundled `Frm` from the underlying type and typeclass. -/
+  of ::
   /-- The underlying frame. -/
   (carrier : Type*)
   [str : Frame carrier]
@@ -39,9 +41,6 @@ instance : CoeSort Frm (Type _) :=
 
 attribute [coe] Frm.carrier
 
-/-- Construct a bundled `Frm` from the underlying type and typeclass. -/
-abbrev of (X : Type*) [Frame X] : Frm := ⟨X⟩
-
 /-- The type of morphisms in `Frm R`. -/
 @[ext]
 structure Hom (X Y : Frm.{u}) where