bump to nightly-2023-04-05-14

mathlib commit leanprover-community/mathlib@1a4df69

Mathbin/AlgebraicTopology/SimplexCategory.lean

@@ -933,7 +933,7 @@ to the category attached to the ordered set `{0, 1, ..., n}` -/
 def toCat : SimplexCategory ⥤ Cat.{0} :=
   SimplexCategory.skeletalFunctor ⋙
     forget₂ NonemptyFinLinOrdCat LinOrd ⋙
-      forget₂ LinOrd Lat ⋙ forget₂ Lat PartOrd ⋙ forget₂ PartOrd PreordCat ⋙ preordCatToCat
+      forget₂ LinOrd Lat ⋙ forget₂ Lat PartOrdCat ⋙ forget₂ PartOrdCat PreordCat ⋙ preordCatToCat
 #align simplex_category.to_Cat SimplexCategory.toCat
 
 end SimplexCategory

Mathbin/Order/Category/BddLat.lean

@@ -113,22 +113,23 @@ theorem coe_forget_to_semilatInf (X : BddLat) : ↥((forget₂ BddLat SemilatInf
   rfl
 #align BddLat.coe_forget_to_SemilatInf BddLat.coe_forget_to_semilatInf
 
-theorem forget_lat_partOrd_eq_forget_bddOrd_partOrd :
-    forget₂ BddLat Lat ⋙ forget₂ Lat PartOrd = forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd :=
+theorem forget_lat_partOrdCat_eq_forget_bddOrd_partOrdCat :
+    forget₂ BddLat Lat ⋙ forget₂ Lat PartOrdCat =
+      forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrdCat :=
   rfl
-#align BddLat.forget_Lat_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd
+#align BddLat.forget_Lat_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_lat_partOrdCat_eq_forget_bddOrd_partOrdCat
 
-theorem forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd :
-    forget₂ BddLat SemilatSup ⋙ forget₂ SemilatSup PartOrd =
-      forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd :=
+theorem forget_semilatSup_partOrdCat_eq_forget_bddOrd_partOrdCat :
+    forget₂ BddLat SemilatSup ⋙ forget₂ SemilatSup PartOrdCat =
+      forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrdCat :=
   rfl
-#align BddLat.forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd
+#align BddLat.forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatSup_partOrdCat_eq_forget_bddOrd_partOrdCat
 
-theorem forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd :
-    forget₂ BddLat SemilatInf ⋙ forget₂ SemilatInf PartOrd =
-      forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd :=
+theorem forget_semilatInf_partOrdCat_eq_forget_bddOrd_partOrdCat :
+    forget₂ BddLat SemilatInf ⋙ forget₂ SemilatInf PartOrdCat =
+      forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrdCat :=
   rfl
-#align BddLat.forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd
+#align BddLat.forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatInf_partOrdCat_eq_forget_bddOrd_partOrdCat
 
 /-- Constructs an equivalence between bounded lattices from an order isomorphism
 between them. -/

Mathbin/Order/Category/BddOrd.lean

@@ -25,7 +25,7 @@ open CategoryTheory
 
 /-- The category of bounded orders with monotone functions. -/
 structure BddOrd where
-  toPartOrd : PartOrd
+  toPartOrd : PartOrdCat
   [isBoundedOrder : BoundedOrder to_PartOrd]
 #align BddOrd BddOrd
 
@@ -68,7 +68,7 @@ instance concreteCategory : ConcreteCategory BddOrd
   forget_faithful := ⟨fun X Y => by convert FunLike.coe_injective⟩
 #align BddOrd.concrete_category BddOrd.concreteCategory
 
-instance hasForgetToPartOrd : HasForget₂ BddOrd PartOrd
+instance hasForgetToPartOrd : HasForget₂ BddOrd PartOrdCat
     where forget₂ :=
     { obj := fun X => X.toPartOrd
       map := fun X Y => BoundedOrderHom.toOrderHom }
@@ -113,10 +113,10 @@ def dualEquiv : BddOrd ≌ BddOrd :=
 
 end BddOrd
 
-theorem bddOrd_dual_comp_forget_to_partOrd :
-    BddOrd.dual ⋙ forget₂ BddOrd PartOrd = forget₂ BddOrd PartOrd ⋙ PartOrd.dual :=
+theorem bddOrd_dual_comp_forget_to_partOrdCat :
+    BddOrd.dual ⋙ forget₂ BddOrd PartOrdCat = forget₂ BddOrd PartOrdCat ⋙ PartOrdCat.dual :=
   rfl
-#align BddOrd_dual_comp_forget_to_PartOrd bddOrd_dual_comp_forget_to_partOrd
+#align BddOrd_dual_comp_forget_to_PartOrd bddOrd_dual_comp_forget_to_partOrdCat
 
 theorem bddOrd_dual_comp_forget_to_bipointed :
     BddOrd.dual ⋙ forget₂ BddOrd Bipointed = forget₂ BddOrd Bipointed ⋙ Bipointed.swap :=

Mathbin/Order/Category/FinPartOrd.lean

@@ -31,7 +31,7 @@ open CategoryTheory
 
 /-- The category of finite partial orders with monotone functions. -/
 structure FinPartOrd where
-  toPartOrd : PartOrd
+  toPartOrd : PartOrdCat
   [isFintype : Fintype to_PartOrd]
 #align FinPartOrd FinPartOrd
 
@@ -71,7 +71,7 @@ instance concreteCategory : ConcreteCategory FinPartOrd :=
   InducedCategory.concreteCategory FinPartOrd.toPartOrd
 #align FinPartOrd.concrete_category FinPartOrd.concreteCategory
 
-instance hasForgetToPartOrd : HasForget₂ FinPartOrd PartOrd :=
+instance hasForgetToPartOrd : HasForget₂ FinPartOrd PartOrdCat :=
   InducedCategory.hasForget₂ FinPartOrd.toPartOrd
 #align FinPartOrd.has_forget_to_PartOrd FinPartOrd.hasForgetToPartOrd
 
@@ -112,8 +112,9 @@ def dualEquiv : FinPartOrd ≌ FinPartOrd :=
 
 end FinPartOrd
 
-theorem finPartOrd_dual_comp_forget_to_partOrd :
-    FinPartOrd.dual ⋙ forget₂ FinPartOrd PartOrd = forget₂ FinPartOrd PartOrd ⋙ PartOrd.dual :=
+theorem finPartOrd_dual_comp_forget_to_partOrdCat :
+    FinPartOrd.dual ⋙ forget₂ FinPartOrd PartOrdCat =
+      forget₂ FinPartOrd PartOrdCat ⋙ PartOrdCat.dual :=
   rfl
-#align FinPartOrd_dual_comp_forget_to_PartOrd finPartOrd_dual_comp_forget_to_partOrd
+#align FinPartOrd_dual_comp_forget_to_PartOrd finPartOrd_dual_comp_forget_to_partOrdCat
 

Mathbin/Order/Category/Lat.lean

@@ -68,7 +68,7 @@ instance : LargeCategory.{u} Lat :=
 instance : ConcreteCategory Lat :=
   BundledHom.concreteCategory LatticeHom
 
-instance hasForgetToPartOrd : HasForget₂ Lat PartOrd
+instance hasForgetToPartOrd : HasForget₂ Lat PartOrdCat
     where
   forget₂ :=
     { obj := fun X => ⟨X⟩
@@ -107,8 +107,8 @@ def dualEquiv : Lat ≌ Lat :=
 
 end Lat
 
-theorem lat_dual_comp_forget_to_partOrd :
-    Lat.dual ⋙ forget₂ Lat PartOrd = forget₂ Lat PartOrd ⋙ PartOrd.dual :=
+theorem lat_dual_comp_forget_to_partOrdCat :
+    Lat.dual ⋙ forget₂ Lat PartOrdCat = forget₂ Lat PartOrdCat ⋙ PartOrdCat.dual :=
   rfl
-#align Lat_dual_comp_forget_to_PartOrd lat_dual_comp_forget_to_partOrd
+#align Lat_dual_comp_forget_to_PartOrd lat_dual_comp_forget_to_partOrdCat
 

Mathbin/Order/Category/PartOrd.lean

@@ -22,44 +22,53 @@ open CategoryTheory
 
 universe u
 
+#print PartOrdCat /-
 /-- The category of partially ordered types. -/
-def PartOrd :=
+def PartOrdCat :=
   Bundled PartialOrder
-#align PartOrd PartOrd
+#align PartOrd PartOrdCat
+-/
 
-namespace PartOrd
+namespace PartOrdCat
 
 instance : BundledHom.ParentProjection @PartialOrder.toPreorder :=
   ⟨⟩
 
-deriving instance LargeCategory, ConcreteCategory for PartOrd
+deriving instance LargeCategory, ConcreteCategory for PartOrdCat
 
-instance : CoeSort PartOrd (Type _) :=
+instance : CoeSort PartOrdCat (Type _) :=
   Bundled.hasCoeToSort
 
+#print PartOrdCat.of /-
 /-- Construct a bundled PartOrd from the underlying type and typeclass. -/
-def of (α : Type _) [PartialOrder α] : PartOrd :=
+def of (α : Type _) [PartialOrder α] : PartOrdCat :=
   Bundled.of α
-#align PartOrd.of PartOrd.of
+#align PartOrd.of PartOrdCat.of
+-/
 
+#print PartOrdCat.coe_of /-
 @[simp]
 theorem coe_of (α : Type _) [PartialOrder α] : ↥(of α) = α :=
   rfl
-#align PartOrd.coe_of PartOrd.coe_of
+#align PartOrd.coe_of PartOrdCat.coe_of
+-/
 
-instance : Inhabited PartOrd :=
+instance : Inhabited PartOrdCat :=
   ⟨of PUnit⟩
 
-instance (α : PartOrd) : PartialOrder α :=
+instance (α : PartOrdCat) : PartialOrder α :=
   α.str
 
-instance hasForgetToPreord : HasForget₂ PartOrd PreordCat :=
+#print PartOrdCat.hasForgetToPreordCat /-
+instance hasForgetToPreordCat : HasForget₂ PartOrdCat PreordCat :=
   BundledHom.forget₂ _ _
-#align PartOrd.has_forget_to_Preord PartOrd.hasForgetToPreord
+#align PartOrd.has_forget_to_Preord PartOrdCat.hasForgetToPreordCat
+-/
 
+#print PartOrdCat.Iso.mk /-
 /-- Constructs an equivalence between partial orders from an order isomorphism between them. -/
 @[simps]
-def Iso.mk {α β : PartOrd.{u}} (e : α ≃o β) : α ≅ β
+def Iso.mk {α β : PartOrdCat.{u}} (e : α ≃o β) : α ≅ β
     where
   Hom := e
   inv := e.symm
@@ -69,46 +78,62 @@ def Iso.mk {α β : PartOrd.{u}} (e : α ≃o β) : α ≅ β
   inv_hom_id' := by
     ext
     exact e.apply_symm_apply x
-#align PartOrd.iso.mk PartOrd.Iso.mk
+#align PartOrd.iso.mk PartOrdCat.Iso.mk
+-/
 
+#print PartOrdCat.dual /-
 /-- `order_dual` as a functor. -/
 @[simps]
-def dual : PartOrd ⥤ PartOrd where
+def dual : PartOrdCat ⥤ PartOrdCat where
   obj X := of Xᵒᵈ
   map X Y := OrderHom.dual
-#align PartOrd.dual PartOrd.dual
+#align PartOrd.dual PartOrdCat.dual
+-/
 
+/- warning: PartOrd.dual_equiv -> PartOrdCat.dualEquiv is a dubious translation:
+lean 3 declaration is
+  CategoryTheory.Equivalence.{u1, u1, succ u1, succ u1} PartOrdCat.{u1} PartOrdCat.largeCategory.{u1} PartOrdCat.{u1} PartOrdCat.largeCategory.{u1}
+but is expected to have type
+  CategoryTheory.Equivalence.{u1, u1, succ u1, succ u1} PartOrdCat.{u1} PartOrdCat.{u1} instPartOrdCatLargeCategory.{u1} instPartOrdCatLargeCategory.{u1}
+Case conversion may be inaccurate. Consider using '#align PartOrd.dual_equiv PartOrdCat.dualEquivₓ'. -/
 /-- The equivalence between `PartOrd` and itself induced by `order_dual` both ways. -/
 @[simps Functor inverse]
-def dualEquiv : PartOrd ≌ PartOrd :=
+def dualEquiv : PartOrdCat ≌ PartOrdCat :=
   Equivalence.mk dual dual
     (NatIso.ofComponents (fun X => Iso.mk <| OrderIso.dualDual X) fun X Y f => rfl)
     (NatIso.ofComponents (fun X => Iso.mk <| OrderIso.dualDual X) fun X Y f => rfl)
-#align PartOrd.dual_equiv PartOrd.dualEquiv
+#align PartOrd.dual_equiv PartOrdCat.dualEquiv
 
-end PartOrd
+end PartOrdCat
 
-theorem partOrd_dual_comp_forget_to_preordCat :
-    PartOrd.dual ⋙ forget₂ PartOrd PreordCat = forget₂ PartOrd PreordCat ⋙ PreordCat.dual :=
+#print partOrdCat_dual_comp_forget_to_preordCat /-
+theorem partOrdCat_dual_comp_forget_to_preordCat :
+    PartOrdCat.dual ⋙ forget₂ PartOrdCat PreordCat =
+      forget₂ PartOrdCat PreordCat ⋙ PreordCat.dual :=
   rfl
-#align PartOrd_dual_comp_forget_to_Preord partOrd_dual_comp_forget_to_preordCat
+#align PartOrd_dual_comp_forget_to_Preord partOrdCat_dual_comp_forget_to_preordCat
+-/
 
+#print preordCatToPartOrdCat /-
 /-- `antisymmetrization` as a functor. It is the free functor. -/
-def preordToPartOrd : PreordCat.{u} ⥤ PartOrd
+def preordCatToPartOrdCat : PreordCat.{u} ⥤ PartOrdCat
     where
-  obj X := PartOrd.of (Antisymmetrization X (· ≤ ·))
+  obj X := PartOrdCat.of (Antisymmetrization X (· ≤ ·))
   map X Y f := f.Antisymmetrization
   map_id' X := by
     ext
     exact Quotient.inductionOn' x fun x => Quotient.map'_mk'' _ (fun a b => id) _
   map_comp' X Y Z f g := by
     ext
     exact Quotient.inductionOn' x fun x => OrderHom.antisymmetrization_apply_mk _ _
-#align Preord_to_PartOrd preordToPartOrd
+#align Preord_to_PartOrd preordCatToPartOrdCat
+-/
 
+#print preordCatToPartOrdCatForgetAdjunction /-
 /-- `Preord_to_PartOrd` is left adjoint to the forgetful functor, meaning it is the free
 functor from `Preord` to `PartOrd`. -/
-def preordToPartOrdForgetAdjunction : preordToPartOrd.{u} ⊣ forget₂ PartOrd PreordCat :=
+def preordCatToPartOrdCatForgetAdjunction :
+    preordCatToPartOrdCat.{u} ⊣ forget₂ PartOrdCat PreordCat :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun X Y =>
         { toFun := fun f =>
@@ -122,13 +147,16 @@ def preordToPartOrdForgetAdjunction : preordToPartOrd.{u} ⊣ forget₂ PartOrd
       homEquiv_naturality_left_symm := fun X Y Z f g =>
         OrderHom.ext _ _ <| funext fun x => Quotient.inductionOn' x fun x => rfl
       homEquiv_naturality_right := fun X Y Z f g => OrderHom.ext _ _ <| funext fun x => rfl }
-#align Preord_to_PartOrd_forget_adjunction preordToPartOrdForgetAdjunction
+#align Preord_to_PartOrd_forget_adjunction preordCatToPartOrdCatForgetAdjunction
+-/
 
+#print preordCatToPartOrdCatCompToDualIsoToDualCompPreordCatToPartOrdCat /-
 /-- `Preord_to_PartOrd` and `order_dual` commute. -/
 @[simps]
-def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd :
-    preordToPartOrd.{u} ⋙ PartOrd.dual ≅ PreordCat.dual ⋙ preordToPartOrd :=
-  NatIso.ofComponents (fun X => PartOrd.Iso.mk <| OrderIso.dualAntisymmetrization _) fun X Y f =>
+def preordCatToPartOrdCatCompToDualIsoToDualCompPreordCatToPartOrdCat :
+    preordCatToPartOrdCat.{u} ⋙ PartOrdCat.dual ≅ PreordCat.dual ⋙ preordCatToPartOrdCat :=
+  NatIso.ofComponents (fun X => PartOrdCat.Iso.mk <| OrderIso.dualAntisymmetrization _) fun X Y f =>
     OrderHom.ext _ _ <| funext fun x => Quotient.inductionOn' x fun x => rfl
-#align Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd
+#align Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd preordCatToPartOrdCatCompToDualIsoToDualCompPreordCatToPartOrdCat
+-/
 

Mathbin/Order/Category/Semilat.lean

@@ -79,16 +79,16 @@ instance : ConcreteCategory SemilatSup
       map := fun X Y => coeFn }
   forget_faithful := ⟨fun X Y => FunLike.coe_injective⟩
 
-instance hasForgetToPartOrd : HasForget₂ SemilatSup PartOrd
+instance hasForgetToPartOrd : HasForget₂ SemilatSup PartOrdCat
     where forget₂ :=
     { obj := fun X => ⟨X⟩
       map := fun X Y f => f }
 #align SemilatSup.has_forget_to_PartOrd SemilatSup.hasForgetToPartOrd
 
 @[simp]
-theorem coe_forget_to_partOrd (X : SemilatSup) : ↥((forget₂ SemilatSup PartOrd).obj X) = ↥X :=
+theorem coe_forget_to_partOrdCat (X : SemilatSup) : ↥((forget₂ SemilatSup PartOrdCat).obj X) = ↥X :=
   rfl
-#align SemilatSup.coe_forget_to_PartOrd SemilatSup.coe_forget_to_partOrd
+#align SemilatSup.coe_forget_to_PartOrd SemilatSup.coe_forget_to_partOrdCat
 
 end SemilatSup
 
@@ -128,16 +128,16 @@ instance : ConcreteCategory SemilatInf
       map := fun X Y => coeFn }
   forget_faithful := ⟨fun X Y => FunLike.coe_injective⟩
 
-instance hasForgetToPartOrd : HasForget₂ SemilatInf PartOrd
+instance hasForgetToPartOrd : HasForget₂ SemilatInf PartOrdCat
     where forget₂ :=
     { obj := fun X => ⟨X⟩
       map := fun X Y f => f }
 #align SemilatInf.has_forget_to_PartOrd SemilatInf.hasForgetToPartOrd
 
 @[simp]
-theorem coe_forget_to_partOrd (X : SemilatInf) : ↥((forget₂ SemilatInf PartOrd).obj X) = ↥X :=
+theorem coe_forget_to_partOrdCat (X : SemilatInf) : ↥((forget₂ SemilatInf PartOrdCat).obj X) = ↥X :=
   rfl
-#align SemilatInf.coe_forget_to_PartOrd SemilatInf.coe_forget_to_partOrd
+#align SemilatInf.coe_forget_to_PartOrd SemilatInf.coe_forget_to_partOrdCat
 
 end SemilatInf
 
@@ -205,13 +205,15 @@ def semilatSupEquivSemilatInf : SemilatSup ≌ SemilatInf :=
     (NatIso.ofComponents (fun X => SemilatInf.Iso.mk <| OrderIso.dualDual X) fun X Y f => rfl)
 #align SemilatSup_equiv_SemilatInf semilatSupEquivSemilatInf
 
-theorem semilatSup_dual_comp_forget_to_partOrd :
-    SemilatSup.dual ⋙ forget₂ SemilatInf PartOrd = forget₂ SemilatSup PartOrd ⋙ PartOrd.dual :=
+theorem semilatSup_dual_comp_forget_to_partOrdCat :
+    SemilatSup.dual ⋙ forget₂ SemilatInf PartOrdCat =
+      forget₂ SemilatSup PartOrdCat ⋙ PartOrdCat.dual :=
   rfl
-#align SemilatSup_dual_comp_forget_to_PartOrd semilatSup_dual_comp_forget_to_partOrd
+#align SemilatSup_dual_comp_forget_to_PartOrd semilatSup_dual_comp_forget_to_partOrdCat
 
-theorem semilatInf_dual_comp_forget_to_partOrd :
-    SemilatInf.dual ⋙ forget₂ SemilatSup PartOrd = forget₂ SemilatInf PartOrd ⋙ PartOrd.dual :=
+theorem semilatInf_dual_comp_forget_to_partOrdCat :
+    SemilatInf.dual ⋙ forget₂ SemilatSup PartOrdCat =
+      forget₂ SemilatInf PartOrdCat ⋙ PartOrdCat.dual :=
   rfl
-#align SemilatInf_dual_comp_forget_to_PartOrd semilatInf_dual_comp_forget_to_partOrd
+#align SemilatInf_dual_comp_forget_to_PartOrd semilatInf_dual_comp_forget_to_partOrdCat
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "145adc65407837db584b447d8e6b8570220db8bd",
+    "rev": "86d013e4a75fa2fb47b4873a02c241d1d56a4f6c",
     "name": "lean3port",
-    "inputRev?": "145adc65407837db584b447d8e6b8570220db8bd"}},
+    "inputRev?": "86d013e4a75fa2fb47b4873a02c241d1d56a4f6c"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "333d55a71146ed492842576c2ed6033ca0af5322",
+    "rev": "b57ede590c8e21e71ba026c0b434dec2631ccd28",
     "name": "mathlib",
-    "inputRev?": "333d55a71146ed492842576c2ed6033ca0af5322"}},
+    "inputRev?": "b57ede590c8e21e71ba026c0b434dec2631ccd28"}},
   {"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-04-05-12"
+def tag : String := "nightly-2023-04-05-14"
 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"@"145adc65407837db584b447d8e6b8570220db8bd"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"86d013e4a75fa2fb47b4873a02c241d1d56a4f6c"
 
 @[default_target]
 lean_lib Mathbin where