feat(CategoryTheory): products of finally small categories (#35691)

A product of two finally small categories is finally small.

Author: joelriou

Mathlib/CategoryTheory/Limits/FinallySmall.lean

@@ -29,7 +29,7 @@ converse holds if `J` is filtered.
 
 @[expose] public section
 
-universe w v v₁ u u₁
+universe w w' v v₁ u u₁
 
 open CategoryTheory Functor
 
@@ -86,6 +86,11 @@ instance [Limits.HasTerminal J] : FinallySmall.{w} J :=
   have := Functor.final_const_terminal (C := PUnit.{w + 1}) (D := J)
   .mk' ((Functor.const PUnit.{w + 1}).obj (⊤_ J))
 
+instance {J' : Type*} [Category* J'] [FinallySmall.{w} J] [FinallySmall.{w'} J'] :
+    FinallySmall.{max w w'} (J × J') :=
+  finallySmall_of_final_of_essentiallySmall
+    ((fromFinalModel.{w} J).prod (fromFinalModel.{w'} J'))
+
 end FinallySmall
 
 section InitiallySmall
@@ -146,6 +151,11 @@ instance [LocallySmall.{w} J] [InitiallySmall.{w} J] (X : J) :
   exact initiallySmall_of_initial_of_initiallySmall
     (CostructuredArrow.toOver (fromInitialModel.{w} J) X)
 
+instance {J' : Type*} [Category* J'] [InitiallySmall.{w} J] [InitiallySmall.{w'} J'] :
+    InitiallySmall.{max w w'} (J × J') :=
+  initiallySmall_of_initial_of_essentiallySmall
+    ((fromInitialModel.{w} J).prod (fromInitialModel.{w'} J'))
+
 end InitiallySmall
 
 instance {J : Type u} [Category.{v} J] [InitiallySmall.{w} J] : FinallySmall.{w} Jᵒᵖ where