feat(CategoryTheory/Products): generalize prod to CategoryStruct's (leanprover-community#31160)

This will allow us to recycle these lemmas when defining the product of bicategories.

In doing this I have renamed the product category instance to `prod'` so that the simp lemmas (which are generated for the categorystruct version) get the names `prod_`. Fruthermore, I removed the manual specification of simp lemmas as it did not seem necessary (it generates the same list anyways).

Note that the diff does not make it clear that `prod.hom_ext` `prod_id` and `prod_comp` have been generalized.

Author: callesonne

Mathlib/CategoryTheory/Products/Basic.lean

@@ -34,12 +34,11 @@ universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
 
 section
 
-variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+variable (C : Type u₁) [CategoryStruct.{v₁} C] (D : Type u₂) [CategoryStruct.{v₂} D]
 
--- the generates simp lemmas like `id_fst` and `comp_snd`
-/-- `prod C D` gives the Cartesian product of two categories. -/
-@[simps (notRecursive := []) Hom id_fst id_snd comp_fst comp_snd, stacks 001K]
-instance prod : Category.{max v₁ v₂} (C × D) where
+/-- `CategoryStruct.prod C D` gives the Cartesian product of two `CategoryStruct`'s. -/
+@[simps (notRecursive := [])] -- notRecursive to generate simp lemmas like `id_fst` and `comp_snd`
+instance prod : CategoryStruct.{max v₁ v₂} (C × D) where
   Hom X Y := (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)
   id X := ⟨𝟙 X.1, 𝟙 X.2⟩
   comp f g := (f.1 ≫ g.1, f.2 ≫ g.2)
@@ -72,6 +71,17 @@ abbrev mkHom {X₁ X₂ : C} {Y₁ Y₂ : D} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y
 scoped infixr:70 " ×ₘ " => Prod.mkHom
 
 end Prod
+
+end
+
+section
+
+variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+
+/-- `prod C D` gives the Cartesian product of two categories. -/
+@[stacks 001K]
+instance prod' : Category.{max v₁ v₂} (C × D) where
+
 theorem isIso_prod_iff {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} :
     IsIso f ↔ IsIso f.1 ∧ IsIso f.2 := by
   constructor
@@ -113,7 +123,7 @@ variable (C : Type u₁) [Category.{v₁} C] (D : Type u₁) [Category.{v₁} D]
 universe levels. This helps typeclass resolution.
 -/
 instance uniformProd : Category (C × D) :=
-  CategoryTheory.prod C D
+  CategoryTheory.prod' C D
 
 end
 

Mathlib/CategoryTheory/Yoneda.lean

@@ -455,10 +455,10 @@ variable (C)
 
 -- We need to help typeclass inference with some awkward universe levels here.
 instance prodCategoryInstance1 : Category ((Cᵒᵖ ⥤ Type v₁) × Cᵒᵖ) :=
-  CategoryTheory.prod.{max u₁ v₁, v₁} (Cᵒᵖ ⥤ Type v₁) Cᵒᵖ
+  CategoryTheory.prod'.{max u₁ v₁, v₁} (Cᵒᵖ ⥤ Type v₁) Cᵒᵖ
 
 instance prodCategoryInstance2 : Category (Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) :=
-  CategoryTheory.prod.{v₁, max u₁ v₁} Cᵒᵖ (Cᵒᵖ ⥤ Type v₁)
+  CategoryTheory.prod'.{v₁, max u₁ v₁} Cᵒᵖ (Cᵒᵖ ⥤ Type v₁)
 
 open Yoneda