chore: reorder universes in ConcreteCategory (#5605)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jun 30, 2023 · e9eb901 · e9eb901
1 parent 4d4f0f2
commit e9eb901
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -630,7 +630,7 @@ theorem IsAffineOpen.isLocalization_stalk_aux {X : Scheme} (U : Opens X)
   rw [eqToHom_trans]
 #align algebraic_geometry.is_affine_open.is_localization_stalk_aux AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux
 
-set_option maxHeartbeats 1643256 in
+set_option maxHeartbeats 3200000 in
 theorem IsAffineOpen.isLocalization_stalk_aux' {X : Scheme} {U : Opens X} (hU : IsAffineOpen U)
     (y : PrimeSpectrum (X.presheaf.obj <| op U)) (hy : hU.fromSpec.1.base y ∈ U) :
     hU.fromSpec.val.c.app (op U) ≫ (Scheme.Spec.obj <| op (X.presheaf.obj <| op U)).presheaf.germ
@@ -661,7 +661,7 @@ theorem IsAffineOpen.isLocalization_stalk_aux' {X : Scheme} {U : Opens X} (hU :
   rw [Category.id_comp]
   rfl
 
-set_option maxHeartbeats 420000 in
+set_option maxHeartbeats 800000 in
 theorem IsAffineOpen.isLocalization_stalk' {X : Scheme} {U : Opens X} (hU : IsAffineOpen U)
     (y : PrimeSpectrum (X.presheaf.obj <| op U)) (hy : hU.fromSpec.1.base y ∈ U) :
   haveI : IsAffine _ := hU

diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module category_theory.concrete_category.basic
-! leanprover-community/mathlib commit 05b820ec79b3c98a7dbf1cb32e181584166da2ca
+! leanprover-community/mathlib commit 311ef8c4b4ae2804ea76b8a611bc5ea1d9c16872
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -41,7 +41,7 @@ related work.
 -/
 
 
-universe w w' v v' u
+universe w w' v v' u u'
 
 namespace CategoryTheory
 
@@ -68,13 +68,13 @@ attribute [instance] ConcreteCategory.forget_faithful
 
 /-- The forgetful functor from a concrete category to `Type u`. -/
 @[reducible]
-def forget (C : Type v) [Category C] [ConcreteCategory.{u} C] : C ⥤ Type u :=
+def forget (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] : C ⥤ Type w :=
   ConcreteCategory.forget
 #align category_theory.forget CategoryTheory.forget
 
 -- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _`
 @[reducible]
-instance ConcreteCategory.types : ConcreteCategory (Type u) where
+instance ConcreteCategory.types : ConcreteCategory.{u, u, u+1} (Type u) where
   forget := 𝟭 _
 #align category_theory.concrete_category.types CategoryTheory.ConcreteCategory.types
 
@@ -86,16 +86,16 @@ You can use it on particular examples as:
 instance : HasCoeToSort X := ConcreteCategory.hasCoeToSort X
 ```
 -/
-def ConcreteCategory.hasCoeToSort (C : Type v) [Category C] [ConcreteCategory C] :
-    CoeSort C (Type u) where
+def ConcreteCategory.hasCoeToSort (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] :
+    CoeSort C (Type w) where
   coe := fun X => (forget C).obj X
 #align category_theory.concrete_category.has_coe_to_sort CategoryTheory.ConcreteCategory.hasCoeToSort
 
 section
 
 attribute [local instance] ConcreteCategory.hasCoeToSort
 
-variable {C : Type v} [Category C] [ConcreteCategory.{w} C]
+variable {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C]
 
 -- Porting note: forget_obj_eq_coe has become a syntactic tautology.
 #noalign category_theory.forget_obj_eq_coe