chore: use TypeMax in CategoryTheory.Limits.Types (#3653)

Per discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233463.20universe.20constraint.20issues



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>

Mathlib.lean

@@ -1206,6 +1206,7 @@ import Mathlib.Data.Sym.Sym2
 import Mathlib.Data.Sym.Sym2.Init
 import Mathlib.Data.Tree
 import Mathlib.Data.TwoPointing
+import Mathlib.Data.TypeMax
 import Mathlib.Data.TypeVec
 import Mathlib.Data.TypeVec.Attr
 import Mathlib.Data.UInt

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -330,24 +330,20 @@ def productLimitCone {J : Type u} (F : J → Type max u v) :
 #align category_theory.limits.types.product_limit_cone CategoryTheory.Limits.Types.productLimitCone
 
 /-- The categorical product in `Type u` is the type theoretic product `Π j, F j`. -/
-noncomputable def productIso {J : Type u} (F : J → Type max u v) :
-  haveI : HasProduct F := hasLimit.{u,v} _; ∏ F ≅ ∀ j, F j :=
-  haveI : HasProduct F := hasLimit.{u,v} _; limit.isoLimitCone (productLimitCone.{u, v} F)
+noncomputable def productIso {J : Type u} (F : J → TypeMax.{u, v}) : ∏ F ≅ ∀ j, F j :=
+  limit.isoLimitCone (productLimitCone.{u, v} F)
 #align category_theory.limits.types.product_iso CategoryTheory.Limits.Types.productIso
 
 -- porting note: was `@[elementwise (attr := simp)]`, but it produces a trivial lemma.
 @[simp]
-theorem productIso_hom_comp_eval {J : Type u} (F : J → Type max u v) (j : J) :
-     haveI : HasProduct F := hasLimit.{u,v} _;
+theorem productIso_hom_comp_eval {J : Type u} (F : J → TypeMax.{u, v}) (j : J) :
     ((productIso.{u, v} F).hom ≫ fun f => f j) = Pi.π F j :=
   rfl
 #align category_theory.limits.types.product_iso_hom_comp_eval CategoryTheory.Limits.Types.productIso_hom_comp_eval
 
 @[elementwise (attr := simp)]
-theorem productIso_inv_comp_π {J : Type u} (F : J → Type max u v) (j : J) :
-    haveI : HasProduct F := hasLimit.{u,v} _;
+theorem productIso_inv_comp_π {J : Type u} (F : J → TypeMax.{u, v}) (j : J) :
     (productIso.{u, v} F).inv ≫ Pi.π F j = fun f => f j :=
-  haveI : HasProduct F := hasLimit.{u,v} _;
   limit.isoLimitCone_inv_π (productLimitCone.{u, v} F) ⟨j⟩
 #align category_theory.limits.types.product_iso_inv_comp_π CategoryTheory.Limits.Types.productIso_inv_comp_π