bump to nightly-2023-03-07-00

mathlib commit leanprover-community/mathlib@3b267e7

Mathbin/CategoryTheory/Category/Ulift.lean

@@ -188,7 +188,7 @@ def ULiftHom.down : ULiftHom C ⥤ C where
 lean 3 declaration is
   forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C], CategoryTheory.Equivalence.{u1, max u3 u1, u2, u2} C _inst_1 (CategoryTheory.ULiftHom.{u3, u2} C) (CategoryTheory.ULiftHom.category.{u1, u3, u2} C _inst_1)
 but is expected to have type
-  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C], CategoryTheory.Equivalence.{u1, max u1 u3, u2, u2} C (CategoryTheory.ULiftHom.{u3, u2} C) _inst_1 (CategoryTheory.instCategoryULiftHom.{u1, u3, u2} C _inst_1)
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C], CategoryTheory.Equivalence.{u1, max u1 u3, u2, u2} C (CategoryTheory.ULiftHom.{u3, u2} C) _inst_1 (CategoryTheory.ULiftHom.category.{u1, u3, u2} C _inst_1)
 Case conversion may be inaccurate. Consider using '#align category_theory.ulift_hom.equiv CategoryTheory.ULiftHom.equivₓ'. -/
 /-- The equivalence between `C` and `ulift_hom C`. -/
 def ULiftHom.equiv : C ≌ ULiftHom C
@@ -270,7 +270,7 @@ instance [Inhabited C] : Inhabited (AsSmall C) :=
 lean 3 declaration is
   forall (C : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u3, u4} C], CategoryTheory.Equivalence.{u3, max u1 u3, u4, max u4 u2} C _inst_2 (CategoryTheory.ULiftHom.{u1, max u4 u2} (ULift.{u2, u4} C)) (CategoryTheory.ULiftHom.category.{u3, u1, max u4 u2} (ULift.{u2, u4} C) (CategoryTheory.uliftCategory.{u3, u4, u2} C _inst_2))
 but is expected to have type
-  forall (C : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u3, u4} C], CategoryTheory.Equivalence.{u3, max u3 u1, u4, max u2 u4} C (CategoryTheory.ULiftHom.{u1, max u2 u4} (ULift.{u2, u4} C)) _inst_2 (CategoryTheory.instCategoryULiftHom.{u3, u1, max u4 u2} (ULift.{u2, u4} C) (CategoryTheory.uliftCategory.{u3, u4, u2} C _inst_2))
+  forall (C : Type.{u4}) [_inst_2 : CategoryTheory.Category.{u3, u4} C], CategoryTheory.Equivalence.{u3, max u3 u1, u4, max u2 u4} C (CategoryTheory.ULiftHom.{u1, max u2 u4} (ULift.{u2, u4} C)) _inst_2 (CategoryTheory.ULiftHom.category.{u3, u1, max u4 u2} (ULift.{u2, u4} C) (CategoryTheory.uliftCategory.{u3, u4, u2} C _inst_2))
 Case conversion may be inaccurate. Consider using '#align category_theory.ulift_hom_ulift_category.equiv CategoryTheory.ULiftHomULiftCategory.equivₓ'. -/
 /-- The equivalence between `C` and `ulift_hom (ulift C)`. -/
 def ULiftHomULiftCategory.equiv.{v', u', v, u} (C : Type u) [Category.{v} C] :

Mathbin/CategoryTheory/Limits/Preserves/Finite.lean

@@ -42,36 +42,45 @@ variable {E : Type u₃} [Category.{v₃} E]
 
 variable {J : Type w} [SmallCategory J] {K : J ⥤ C}
 
+#print CategoryTheory.Limits.PreservesFiniteLimits /-
 /-- A functor is said to preserve finite limits, if it preserves all limits of shape `J`,
 where `J : Type` is a finite category.
 -/
 class PreservesFiniteLimits (F : C ⥤ D) where
   PreservesFiniteLimits :
     ∀ (J : Type) [SmallCategory J] [FinCategory J], PreservesLimitsOfShape J F := by infer_instance
 #align category_theory.limits.preserves_finite_limits CategoryTheory.Limits.PreservesFiniteLimits
+-/
 
 attribute [instance] preserves_finite_limits.preserves_finite_limits
 
+#print CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits /-
 /-- Preserving finite limits also implies preserving limits over finite shapes in higher universes,
 though through a noncomputable instance. -/
 noncomputable instance (priority := 100) preservesLimitsOfShapeOfPreservesFiniteLimits (F : C ⥤ D)
     [PreservesFiniteLimits F] (J : Type w) [SmallCategory J] [FinCategory J] :
     PreservesLimitsOfShape J F := by
   apply preserves_limits_of_shape_of_equiv (fin_category.equiv_as_type J)
 #align category_theory.limits.preserves_limits_of_shape_of_preserves_finite_limits CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits
+-/
 
+#print CategoryTheory.Limits.PreservesLimits.preservesFiniteLimitsOfSize /-
 noncomputable instance (priority := 100) PreservesLimits.preservesFiniteLimitsOfSize (F : C ⥤ D)
     [PreservesLimitsOfSize.{w, w₂} F] : PreservesFiniteLimits F :=
   ⟨fun J sJ fJ =>
     haveI := preserves_smallest_limits_of_preserves_limits F
     preserves_limits_of_shape_of_equiv (fin_category.equiv_as_type J) F⟩
 #align category_theory.limits.preserves_limits.preserves_finite_limits_of_size CategoryTheory.Limits.PreservesLimits.preservesFiniteLimitsOfSize
+-/
 
+#print CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits /-
 noncomputable instance (priority := 120) PreservesLimits.preservesFiniteLimits (F : C ⥤ D)
     [PreservesLimits F] : PreservesFiniteLimits F :=
   PreservesLimits.preservesFiniteLimitsOfSize F
 #align category_theory.limits.preserves_limits.preserves_finite_limits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits
+-/
 
+#print CategoryTheory.Limits.preservesFiniteLimitsOfPreservesFiniteLimitsOfSize /-
 /-- We can always derive `preserves_finite_limits C` by showing that we are preserving limits at an
 arbitrary universe. -/
 def preservesFiniteLimitsOfPreservesFiniteLimitsOfSize (F : C ⥤ D)
@@ -90,18 +99,24 @@ def preservesFiniteLimitsOfPreservesFiniteLimitsOfSize (F : C ⥤ D)
     haveI := h (ULiftHom.{w} (ULift.{w} J)) CategoryTheory.finCategoryUlift
     exact preserves_limits_of_shape_of_equiv (ULiftHomULiftCategory.equiv.{w, w} J).symm F⟩
 #align category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size CategoryTheory.Limits.preservesFiniteLimitsOfPreservesFiniteLimitsOfSize
+-/
 
+#print CategoryTheory.Limits.idPreservesFiniteLimits /-
 instance idPreservesFiniteLimits : PreservesFiniteLimits (𝟭 C) where
 #align category_theory.limits.id_preserves_finite_limits CategoryTheory.Limits.idPreservesFiniteLimits
+-/
 
+#print CategoryTheory.Limits.compPreservesFiniteLimits /-
 /-- The composition of two left exact functors is left exact. -/
 def compPreservesFiniteLimits (F : C ⥤ D) (G : D ⥤ E) [PreservesFiniteLimits F]
     [PreservesFiniteLimits G] : PreservesFiniteLimits (F ⋙ G) :=
   ⟨fun _ _ _ => by
     skip
     infer_instance⟩
 #align category_theory.limits.comp_preserves_finite_limits CategoryTheory.Limits.compPreservesFiniteLimits
+-/
 
+#print CategoryTheory.Limits.PreservesFiniteColimits /-
 /-- A functor is said to preserve finite colimits, if it preserves all colimits of
 shape `J`, where `J : Type` is a finite category.
 -/
@@ -110,24 +125,30 @@ class PreservesFiniteColimits (F : C ⥤ D) where
     ∀ (J : Type) [SmallCategory J] [FinCategory J], PreservesColimitsOfShape J F := by
     infer_instance
 #align category_theory.limits.preserves_finite_colimits CategoryTheory.Limits.PreservesFiniteColimits
+-/
 
 attribute [instance] preserves_finite_colimits.preserves_finite_colimits
 
+#print CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits /-
 /-- Preserving finite limits also implies preserving limits over finite shapes in higher universes,
 though through a noncomputable instance. -/
 noncomputable instance (priority := 100) preservesColimitsOfShapeOfPreservesFiniteColimits
     (F : C ⥤ D) [PreservesFiniteColimits F] (J : Type w) [SmallCategory J] [FinCategory J] :
     PreservesColimitsOfShape J F := by
   apply preserves_colimits_of_shape_of_equiv (fin_category.equiv_as_type J)
 #align category_theory.limits.preserves_colimits_of_shape_of_preserves_finite_colimits CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits
+-/
 
+#print CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits /-
 noncomputable instance (priority := 100) PreservesColimits.preservesFiniteColimits (F : C ⥤ D)
     [PreservesColimitsOfSize.{w, w₂} F] : PreservesFiniteColimits F :=
   ⟨fun J sJ fJ =>
     haveI := preserves_smallest_colimits_of_preserves_colimits F
     preserves_colimits_of_shape_of_equiv (fin_category.equiv_as_type J) F⟩
 #align category_theory.limits.preserves_colimits.preserves_finite_colimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits
+-/
 
+#print CategoryTheory.Limits.preservesFiniteColimitsOfPreservesFiniteColimitsOfSize /-
 /-- We can always derive `preserves_finite_limits C` by showing that we are preserving limits at an
 arbitrary universe. -/
 def preservesFiniteColimitsOfPreservesFiniteColimitsOfSize (F : C ⥤ D)
@@ -146,17 +167,22 @@ def preservesFiniteColimitsOfPreservesFiniteColimitsOfSize (F : C ⥤ D)
     haveI := h (ULiftHom.{w} (ULift.{w} J)) CategoryTheory.finCategoryUlift
     exact preserves_colimits_of_shape_of_equiv (ULiftHomULiftCategory.equiv.{w, w} J).symm F⟩
 #align category_theory.limits.preserves_finite_colimits_of_preserves_finite_colimits_of_size CategoryTheory.Limits.preservesFiniteColimitsOfPreservesFiniteColimitsOfSize
+-/
 
+#print CategoryTheory.Limits.idPreservesFiniteColimits /-
 instance idPreservesFiniteColimits : PreservesFiniteColimits (𝟭 C) where
 #align category_theory.limits.id_preserves_finite_colimits CategoryTheory.Limits.idPreservesFiniteColimits
+-/
 
+#print CategoryTheory.Limits.compPreservesFiniteColimits /-
 /-- The composition of two right exact functors is right exact. -/
 def compPreservesFiniteColimits (F : C ⥤ D) (G : D ⥤ E) [PreservesFiniteColimits F]
     [PreservesFiniteColimits G] : PreservesFiniteColimits (F ⋙ G) :=
   ⟨fun _ _ _ => by
     skip
     infer_instance⟩
 #align category_theory.limits.comp_preserves_finite_colimits CategoryTheory.Limits.compPreservesFiniteColimits
+-/
 
 end CategoryTheory.Limits
 

Mathbin/CategoryTheory/Limits/Shapes/WidePullbacks.lean

@@ -186,7 +186,7 @@ def equivalenceOfEquiv (J' : Type w') (h : J ≃ J') : WidePullbackShape J ≌ W
 lean 3 declaration is
   forall {J : Type.{u1}}, CategoryTheory.Equivalence.{max u2 u1, max u1 u2, max u1 u2, max u1 u2} (CategoryTheory.ULiftHom.{u2, max u1 u2} (ULift.{u2, u1} (CategoryTheory.Limits.WidePullbackShape.{u1} J))) (CategoryTheory.ULiftHom.category.{u1, u2, max u1 u2} (ULift.{u2, u1} (CategoryTheory.Limits.WidePullbackShape.{u1} J)) (CategoryTheory.uliftCategory.{u1, u1, u2} (CategoryTheory.Limits.WidePullbackShape.{u1} J) (CategoryTheory.Limits.WidePullbackShape.category.{u1} J))) (CategoryTheory.Limits.WidePullbackShape.{max u1 u2} (ULift.{u2, u1} J)) (CategoryTheory.Limits.WidePullbackShape.category.{max u1 u2} (ULift.{u2, u1} J))
 but is expected to have type
-  forall {J : Type.{u1}}, CategoryTheory.Equivalence.{max u1 u2, max u1 u2, max u2 u1, max u1 u2} (CategoryTheory.ULiftHom.{u2, max u2 u1} (ULift.{u2, u1} (CategoryTheory.Limits.WidePullbackShape.{u1} J))) (CategoryTheory.Limits.WidePullbackShape.{max u1 u2} (ULift.{u2, u1} J)) (CategoryTheory.instCategoryULiftHom.{u1, u2, max u1 u2} (ULift.{u2, u1} (CategoryTheory.Limits.WidePullbackShape.{u1} J)) (CategoryTheory.uliftCategory.{u1, u1, u2} (CategoryTheory.Limits.WidePullbackShape.{u1} J) (CategoryTheory.Limits.WidePullbackShape.category.{u1} J))) (CategoryTheory.Limits.WidePullbackShape.category.{max u1 u2} (ULift.{u2, u1} J))
+  forall {J : Type.{u1}}, CategoryTheory.Equivalence.{max u1 u2, max u1 u2, max u2 u1, max u1 u2} (CategoryTheory.ULiftHom.{u2, max u2 u1} (ULift.{u2, u1} (CategoryTheory.Limits.WidePullbackShape.{u1} J))) (CategoryTheory.Limits.WidePullbackShape.{max u1 u2} (ULift.{u2, u1} J)) (CategoryTheory.ULiftHom.category.{u1, u2, max u1 u2} (ULift.{u2, u1} (CategoryTheory.Limits.WidePullbackShape.{u1} J)) (CategoryTheory.uliftCategory.{u1, u1, u2} (CategoryTheory.Limits.WidePullbackShape.{u1} J) (CategoryTheory.Limits.WidePullbackShape.category.{u1} J))) (CategoryTheory.Limits.WidePullbackShape.category.{max u1 u2} (ULift.{u2, u1} J))
 Case conversion may be inaccurate. Consider using '#align category_theory.limits.wide_pullback_shape.ulift_equivalence CategoryTheory.Limits.WidePullbackShape.uliftEquivalenceₓ'. -/
 /-- Lifting universe and morphism levels preserves wide pullback diagrams. -/
 def uliftEquivalence :

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "62fbb5208f22bc33dc6e206d02583c130bbfd077",
+    "rev": "5716e8852fccd143396aa09a0dc77915d29946b4",
     "name": "lean3port",
-    "inputRev?": "62fbb5208f22bc33dc6e206d02583c130bbfd077"}},
+    "inputRev?": "5716e8852fccd143396aa09a0dc77915d29946b4"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "b55832c639041a4c60d92ea92a86268307140792",
+    "rev": "d1ee6c39408c269106b3e3f498b50b2e69832968",
     "name": "mathlib",
-    "inputRev?": "b55832c639041a4c60d92ea92a86268307140792"}},
+    "inputRev?": "d1ee6c39408c269106b3e3f498b50b2e69832968"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-06-12"
+def tag : String := "nightly-2023-03-07-00"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"62fbb5208f22bc33dc6e206d02583c130bbfd077"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5716e8852fccd143396aa09a0dc77915d29946b4"
 
 @[default_target]
 lean_lib Mathbin where