bump to nightly-2023-03-31-12

mathlib commit leanprover-community/mathlib@ce11c3c

Mathbin/CategoryTheory/Action.lean

@@ -57,7 +57,7 @@ namespace ActionCategory
 /-- The projection from the action category to the monoid, mapping a morphism to its
   label. -/
 def π : ActionCategory M X ⥤ SingleObj M :=
-  categoryOfElements.π _
+  CategoryOfElements.π _
 #align category_theory.action_category.π CategoryTheory.ActionCategory.π
 
 @[simp]

Mathbin/CategoryTheory/Limits/Presheaf.lean

@@ -92,7 +92,7 @@ def restrictedYonedaYoneda : restrictedYoneda (yoneda : C ⥤ Cᵒᵖ ⥤ Type u
 It is shown in `restrict_yoneda_hom_equiv_natural` that this is a natural bijection.
 -/
 def restrictYonedaHomEquiv (P : Cᵒᵖ ⥤ Type u₁) (E : ℰ)
-    {c : Cocone ((categoryOfElements.π P).leftOp ⋙ A)} (t : IsColimit c) :
+    {c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)} (t : IsColimit c) :
     (c.pt ⟶ E) ≃ (P ⟶ (restrictedYoneda A).obj E) :=
   ((uliftTrivial _).symm ≪≫ t.homIso' E).toEquiv.trans
     { toFun := fun k =>
@@ -144,13 +144,13 @@ def extendAlongYoneda : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ :=
 
 @[simp]
 theorem extendAlongYoneda_obj (P : Cᵒᵖ ⥤ Type u₁) :
-    (extendAlongYoneda A).obj P = colimit ((categoryOfElements.π P).leftOp ⋙ A) :=
+    (extendAlongYoneda A).obj P = colimit ((CategoryOfElements.π P).leftOp ⋙ A) :=
   rfl
 #align category_theory.colimit_adj.extend_along_yoneda_obj CategoryTheory.ColimitAdj.extendAlongYoneda_obj
 
 theorem extendAlongYoneda_map {X Y : Cᵒᵖ ⥤ Type u₁} (f : X ⟶ Y) :
     (extendAlongYoneda A).map f =
-      colimit.pre ((categoryOfElements.π Y).leftOp ⋙ A) (categoryOfElements.map f).op :=
+      colimit.pre ((CategoryOfElements.π Y).leftOp ⋙ A) (CategoryOfElements.map f).op :=
   by
   ext J
   erw [colimit.ι_pre ((category_of_elements.π Y).leftOp ⋙ A) (category_of_elements.map f).op]
@@ -223,9 +223,9 @@ This follows from `category_theory.category_of_elements.costructured_arrow_yoned
 @[simps]
 def extendAlongYonedaIsoKanApp (X) :
     (extendAlongYoneda A).obj X ≅ ((lan yoneda : (_ ⥤ ℰ) ⥤ _).obj A).obj X :=
-  let eq := categoryOfElements.costructuredArrowYonedaEquivalence X
+  let eq := CategoryOfElements.costructuredArrowYonedaEquivalence X
   { Hom := colimit.pre (Lan.diagram (yoneda : C ⥤ _ ⥤ Type u₁) A X) Eq.Functor
-    inv := colimit.pre ((categoryOfElements.π X).leftOp ⋙ A) Eq.inverse
+    inv := colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) Eq.inverse
     hom_inv_id' :=
       by
       erw [colimit.pre_pre ((category_of_elements.π X).leftOp ⋙ A) eq.inverse]
@@ -296,7 +296,7 @@ by the fact that it factors through the yoneda embedding).
 `cocone_of_representable` gives a cocone for this functor which is a colimit and has point `P`.
 -/
 def functorToRepresentables (P : Cᵒᵖ ⥤ Type u₁) : P.Elementsᵒᵖ ⥤ Cᵒᵖ ⥤ Type u₁ :=
-  (categoryOfElements.π P).leftOp ⋙ yoneda
+  (CategoryOfElements.π P).leftOp ⋙ yoneda
 #align category_theory.functor_to_representables CategoryTheory.functorToRepresentables
 
 /-- This is a cocone with point `P` for the functor `functor_to_representables P`. It is shown in
@@ -324,7 +324,7 @@ theorem coconeOfRepresentable_ι_app (P : Cᵒᵖ ⥤ Type u₁) (j : P.Elements
 /-- The legs of the cocone `cocone_of_representable` are natural in the choice of presheaf. -/
 theorem coconeOfRepresentable_naturality {P₁ P₂ : Cᵒᵖ ⥤ Type u₁} (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ) :
     (coconeOfRepresentable P₁).ι.app j ≫ α =
-      (coconeOfRepresentable P₂).ι.app ((categoryOfElements.map α).op.obj j) :=
+      (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j) :=
   by
   ext (T f)
   simpa [cocone_of_representable_ι_app] using functor_to_types.naturality _ _ α f.op _

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "347b5e9405bc2b488fe32bfcef13148fa6b8f896",
+    "rev": "f71bfd03e7897d688c27196a4727c9af0680ee22",
     "name": "lean3port",
-    "inputRev?": "347b5e9405bc2b488fe32bfcef13148fa6b8f896"}},
+    "inputRev?": "f71bfd03e7897d688c27196a4727c9af0680ee22"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ac1e75f550b4f6486f1aa7c4799216f4f43ed2fc",
+    "rev": "c04b29dd6b022753894b2fc21d2d4951e76e339e",
     "name": "mathlib",
-    "inputRev?": "ac1e75f550b4f6486f1aa7c4799216f4f43ed2fc"}},
+    "inputRev?": "c04b29dd6b022753894b2fc21d2d4951e76e339e"}},
   {"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-31-10"
+def tag : String := "nightly-2023-03-31-12"
 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"@"347b5e9405bc2b488fe32bfcef13148fa6b8f896"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f71bfd03e7897d688c27196a4727c9af0680ee22"
 
 @[default_target]
 lean_lib Mathbin where