bump to nightly-2023-08-16-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/CategoryTheory/Functor/Flat.lean

@@ -65,7 +65,6 @@ variable {J : Type w} [SmallCategory J]
 
 variable {K : J ⥤ C} (F : C ⥤ D) (c : Cone K)
 
-#print CategoryTheory.StructuredArrowCone.toDiagram /-
 /-- Given a cone `c : cone K` and a map `f : X ⟶ c.X`, we can construct a cone of structured
 arrows over `X` with `f` as the cone point. This is the underlying diagram.
 -/
@@ -75,29 +74,30 @@ def toDiagram : J ⥤ StructuredArrow c.pt K
   obj j := StructuredArrow.mk (c.π.app j)
   map j k g := StructuredArrow.homMk g (by simpa)
 #align category_theory.structured_arrow_cone.to_diagram CategoryTheory.StructuredArrowCone.toDiagram
--/
 
-#print CategoryTheory.StructuredArrowCone.diagramToCone /-
+#print CategoryTheory.Limits.Cone.fromStructuredArrow /-
 /-- Given a diagram of `structured_arrow X F`s, we may obtain a cone with cone point `X`. -/
 @[simps]
-def diagramToCone {X : D} (G : J ⥤ StructuredArrow X F) : Cone (G ⋙ proj X F ⋙ F) :=
+def CategoryTheory.Limits.Cone.fromStructuredArrow {X : D} (G : J ⥤ StructuredArrow X F) :
+    Cone (G ⋙ proj X F ⋙ F) :=
   { pt
     π := { app := fun j => (G.obj j).Hom } }
-#align category_theory.structured_arrow_cone.diagram_to_cone CategoryTheory.StructuredArrowCone.diagramToCone
+#align category_theory.structured_arrow_cone.diagram_to_cone CategoryTheory.Limits.Cone.fromStructuredArrow
 -/
 
-#print CategoryTheory.StructuredArrowCone.toCone /-
+#print CategoryTheory.Limits.Cone.toStructuredArrowCone /-
 /-- Given a cone `c : cone K` and a map `f : X ⟶ F.obj c.X`, we can construct a cone of structured
 arrows over `X` with `f` as the cone point.
 -/
 @[simps]
-def toCone {X : D} (f : X ⟶ F.obj c.pt) : Cone (toDiagram (F.mapCone c) ⋙ map f ⋙ pre _ K F)
+def CategoryTheory.Limits.Cone.toStructuredArrowCone {X : D} (f : X ⟶ F.obj c.pt) :
+    Cone (toDiagram (F.mapCone c) ⋙ map f ⋙ pre _ K F)
     where
   pt := mk f
   π :=
     { app := fun j => homMk (c.π.app j) rfl
       naturality' := fun j k g => by ext; dsimp; simp }
-#align category_theory.structured_arrow_cone.to_cone CategoryTheory.StructuredArrowCone.toCone
+#align category_theory.structured_arrow_cone.to_cone CategoryTheory.Limits.Cone.toStructuredArrowCone
 -/
 
 end StructuredArrowCone

Mathbin/Topology/Instances/Real.lean

@@ -200,7 +200,7 @@ section
 #print closure_of_rat_image_lt /-
 theorem closure_of_rat_image_lt {q : ℚ} : closure ((coe : ℚ → ℝ) '' {x | q < x}) = {r | ↑q ≤ r} :=
   Subset.antisymm
-    ((isClosed_ge' _).closure_subset_iff.2
+    ((ClosedIciTopology.isClosed_ge' _).closure_subset_iff.2
       (image_subset_iff.2 fun p h => le_of_lt <| (@Rat.cast_lt ℝ _ _ _).2 h))
     fun x hx =>
     mem_closure_iff_nhds.2 fun t ht =>

Mathbin/Topology/MetricSpace/Basic.lean

@@ -3261,7 +3261,8 @@ theorem Bounded.subset_ball_lt (h : Bounded s) (a : ℝ) (c : α) : ∃ r, a < r
 #print Metric.bounded_closure_of_bounded /-
 theorem bounded_closure_of_bounded (h : Bounded s) : Bounded (closure s) :=
   let ⟨C, h⟩ := h
-  ⟨C, fun a ha b hb => (isClosed_le' C).closure_subset <| map_mem_closure₂ continuous_dist ha hb h⟩
+  ⟨C, fun a ha b hb =>
+    (ClosedIicTopology.isClosed_le' C).closure_subset <| map_mem_closure₂ continuous_dist ha hb h⟩
 #align metric.bounded_closure_of_bounded Metric.bounded_closure_of_bounded
 -/
 

Mathbin/Topology/Order/Basic.lean

@@ -144,27 +144,27 @@ theorem isClosed_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f)
 #align is_closed_le isClosed_le
 -/
 
-#print isClosed_le' /-
-theorem isClosed_le' (a : α) : IsClosed {b | b ≤ a} :=
+#print ClosedIicTopology.isClosed_le' /-
+theorem ClosedIicTopology.isClosed_le' (a : α) : IsClosed {b | b ≤ a} :=
   isClosed_le continuous_id continuous_const
-#align is_closed_le' isClosed_le'
+#align is_closed_le' ClosedIicTopology.isClosed_le'
 -/
 
 #print isClosed_Iic /-
 theorem isClosed_Iic {a : α} : IsClosed (Iic a) :=
-  isClosed_le' a
+  ClosedIicTopology.isClosed_le' a
 #align is_closed_Iic isClosed_Iic
 -/
 
-#print isClosed_ge' /-
-theorem isClosed_ge' (a : α) : IsClosed {b | a ≤ b} :=
+#print ClosedIciTopology.isClosed_ge' /-
+theorem ClosedIciTopology.isClosed_ge' (a : α) : IsClosed {b | a ≤ b} :=
   isClosed_le continuous_const continuous_id
-#align is_closed_ge' isClosed_ge'
+#align is_closed_ge' ClosedIciTopology.isClosed_ge'
 -/
 
 #print isClosed_Ici /-
 theorem isClosed_Ici {a : α} : IsClosed (Ici a) :=
-  isClosed_ge' a
+  ClosedIciTopology.isClosed_ge' a
 #align is_closed_Ici isClosed_Ici
 -/
 

Mathbin/Topology/Order/LowerTopology.lean

@@ -208,11 +208,13 @@ theorem isOpen_iff_generate_Ici_compl : IsOpen s ↔ GenerateOpen {t | ∃ a, Ic
 #align lower_topology.is_open_iff_generate_Ici_compl LowerTopology.isOpen_iff_generate_Ici_compl
 -/
 
-#print LowerTopology.isClosed_Ici /-
+/- warning: lower_topology.is_closed_Ici clashes with is_closed_Ici -> isClosed_Ici
+Case conversion may be inaccurate. Consider using '#align lower_topology.is_closed_Ici isClosed_Iciₓ'. -/
+#print isClosed_Ici /-
 /-- Left-closed right-infinite intervals [a, ∞) are closed in the lower topology. -/
 theorem isClosed_Ici (a : α) : IsClosed (Ici a) :=
   isOpen_compl_iff.1 <| isOpen_iff_generate_Ici_compl.2 <| GenerateOpen.basic _ ⟨a, rfl⟩
-#align lower_topology.is_closed_Ici LowerTopology.isClosed_Ici
+#align lower_topology.is_closed_Ici isClosed_Ici
 -/
 
 #print LowerTopology.isClosed_upperClosure /-
@@ -296,7 +298,7 @@ instance [Preorder α] [TopologicalSpace α] [LowerTopology α] [OrderBot α] [P
     by
     refine' le_antisymm (le_generateFrom _) _
     · rintro _ ⟨x, rfl⟩
-      exact ((LowerTopology.isClosed_Ici _).Prod <| LowerTopology.isClosed_Ici _).isOpen_compl
+      exact ((isClosed_Ici _).Prod <| isClosed_Ici _).isOpen_compl
     rw [(lower_topology.is_topological_basis.prod LowerTopology.isTopologicalBasis).eq_generateFrom,
       le_generate_from_iff_subset_is_open, image2_subset_iff]
     rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
@@ -320,7 +322,7 @@ theorem sInfHom.continuous (f : sInfHom α β) : Continuous f :=
   · exact LowerTopology.topology_eq_lowerTopology β
   rintro _ ⟨b, rfl⟩
   rw [preimage_compl, isOpen_compl_iff]
-  convert LowerTopology.isClosed_Ici (Inf <| f ⁻¹' Ici b)
+  convert isClosed_Ici (Inf <| f ⁻¹' Ici b)
   refine' subset_antisymm (fun a => sInf_le) fun a ha => le_trans _ <| OrderHomClass.mono f ha
   simp [map_Inf]
 #align Inf_hom.continuous sInfHom.continuous

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "844b7ac1e7f888457f10458b595cad2bccda2fe3",
+    "rev": "23cac21ba60ea1d623bb5739e6395deea9657825",
     "name": "lean3port",
-    "inputRev?": "844b7ac1e7f888457f10458b595cad2bccda2fe3"}},
+    "inputRev?": "23cac21ba60ea1d623bb5739e6395deea9657825"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "72b6e767aa1c478f6b5d9c51912b0e8a4f415b2e",
+    "rev": "d66f29ee65bcbe2b6211b4a3ef4b0e31664d9515",
     "name": "mathlib",
-    "inputRev?": "72b6e767aa1c478f6b5d9c51912b0e8a4f415b2e"}},
+    "inputRev?": "d66f29ee65bcbe2b6211b4a3ef4b0e31664d9515"}},
   {"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-08-16-07"
+def tag : String := "nightly-2023-08-16-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"844b7ac1e7f888457f10458b595cad2bccda2fe3"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"23cac21ba60ea1d623bb5739e6395deea9657825"
 
 @[default_target]
 lean_lib Mathbin where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-08-05
+leanprover/lean4:nightly-2023-08-15