bump to nightly-2023-10-23-06

mathlib commit leanprover-community/mathlib@b1abe23

Mathbin/Topology/Sheaves/Forget.lean

@@ -62,7 +62,6 @@ variable {ι : Type v} (U : ι → Opens X)
 
 attribute [local reducible] diagram left_res right_res
 
-#print TopCat.Presheaf.SheafCondition.diagramCompPreservesLimits /-
 /-- When `G` preserves limits, the sheaf condition diagram for `F` composed with `G` is
 naturally isomorphic to the sheaf condition diagram for `F ⋙ G`.
 -/
@@ -85,11 +84,9 @@ def diagramCompPreservesLimits : diagram F U ⋙ G ≅ diagram.{v} (F ⋙ G) U :
     dsimp; simp
   · ext; simp; dsimp; simp
 #align Top.presheaf.sheaf_condition.diagram_comp_preserves_limits TopCat.Presheaf.SheafCondition.diagramCompPreservesLimits
--/
 
 attribute [local reducible] res
 
-#print TopCat.Presheaf.SheafCondition.mapConeFork /-
 /-- When `G` preserves limits, the image under `G` of the sheaf condition fork for `F`
 is the sheaf condition fork for `F ⋙ G`,
 postcomposed with the inverse of the natural isomorphism `diagram_comp_preserves_limits`.
@@ -109,7 +106,6 @@ def mapConeFork :
       dsimp
       simp only [limit.lift_π, fan.mk_π_app, ← G.map_comp, limit.lift_π_assoc, fan.mk_π_app]
 #align Top.presheaf.sheaf_condition.map_cone_fork TopCat.Presheaf.SheafCondition.mapConeFork
--/
 
 end SheafCondition
 

Mathbin/Topology/Sheaves/Functors.lean

@@ -42,17 +42,14 @@ namespace TopCat
 
 namespace Presheaf.SheafConditionPairwiseIntersections
 
-#print TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram /-
 theorem map_diagram : Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).obj ∘ U) :=
   by
   apply functor.hext
   abstract obj_eq intro i; cases i <;> rfl
   intro i j g; apply Subsingleton.helim
   iterate 2 rw [map_diagram.obj_eq]
 #align Top.presheaf.sheaf_condition_pairwise_intersections.map_diagram TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram
--/
 
-#print TopCat.Presheaf.SheafConditionPairwiseIntersections.mapCocone /-
 theorem mapCocone :
     HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).obj ∘ U)) :=
   by
@@ -61,9 +58,7 @@ theorem mapCocone :
   apply Subsingleton.helim; rw [map_diagram, opens.map_supr]
   apply proof_irrel_heq
 #align Top.presheaf.sheaf_condition_pairwise_intersections.map_cocone TopCat.Presheaf.SheafConditionPairwiseIntersections.mapCocone
--/
 
-#print TopCat.Presheaf.SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf /-
 theorem pushforward_sheaf_of_sheaf {F : Presheaf C X} (h : F.IsSheafPairwiseIntersections) :
     (f _* F).IsSheafPairwiseIntersections := fun ι U =>
   by
@@ -72,7 +67,6 @@ theorem pushforward_sheaf_of_sheaf {F : Presheaf C X} (h : F.IsSheafPairwiseInte
   change HEq (F.map_cone ((opens.map f).mapCocone _).op) _
   congr; iterate 2 rw [map_diagram]; apply map_cocone
 #align Top.presheaf.sheaf_condition_pairwise_intersections.pushforward_sheaf_of_sheaf TopCat.Presheaf.SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf
--/
 
 end Presheaf.SheafConditionPairwiseIntersections
 

Mathbin/Topology/Sheaves/SheafCondition/UniqueGluing.lean

@@ -111,17 +111,14 @@ section TypeValued
 
 variable {X : TopCat.{v}} (F : Presheaf (Type v) X) {ι : Type v} (U : ι → Opens X)
 
-#print TopCat.Presheaf.piOpensIsoSectionsFamily /-
 /-- For presheaves of types, terms of `pi_opens F U` are just families of sections.
 -/
 def piOpensIsoSectionsFamily : piOpens F U ≅ ∀ i : ι, F.obj (op (U i)) :=
   Limits.IsLimit.conePointUniqueUpToIso
     (limit.isLimit (Discrete.functor fun i : ι => F.obj (op (U i))))
     (Types.productLimitCone.{v, v} fun i : ι => F.obj (op (U i))).IsLimit
 #align Top.presheaf.pi_opens_iso_sections_family TopCat.Presheaf.piOpensIsoSectionsFamily
--/
 
-#print TopCat.Presheaf.compatible_iff_leftRes_eq_rightRes /-
 /-- Under the isomorphism `pi_opens_iso_sections_family`, compatibility of sections is the same
 as being equalized by the arrows `left_res` and `right_res` of the equalizer diagram.
 -/
@@ -138,9 +135,7 @@ theorem compatible_iff_leftRes_eq_rightRes (sf : piOpens F U) :
     · rw [left_res, types.pi_lift_π_apply]; rfl
     · rw [right_res, types.pi_lift_π_apply]; rfl
 #align Top.presheaf.compatible_iff_left_res_eq_right_res TopCat.Presheaf.compatible_iff_leftRes_eq_rightRes
--/
 
-#print TopCat.Presheaf.isGluing_iff_eq_res /-
 /-- Under the isomorphism `pi_opens_iso_sections_family`, being a gluing of a family of
 sections `sf` is the same as lying in the preimage of `res` (the leftmost arrow of the
 equalizer diagram).
@@ -158,7 +153,6 @@ theorem isGluing_iff_eq_res (sf : piOpens F U) (s : F.obj (op (iSup U))) :
     rw [res, types.pi_lift_π_apply]
     rfl
 #align Top.presheaf.is_gluing_iff_eq_res TopCat.Presheaf.isGluing_iff_eq_res
--/
 
 #print TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types /-
 /-- The "equalizer" sheaf condition can be obtained from the sheaf condition
@@ -190,11 +184,10 @@ theorem isSheaf_of_isSheafUniqueGluing_types (Fsh : F.IsSheafUniqueGluing) : F.I
 #align Top.presheaf.is_sheaf_of_is_sheaf_unique_gluing_types TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types
 -/
 
-#print TopCat.Presheaf.isSheafUniqueGluing_of_isSheaf_types /-
 /-- The sheaf condition in terms of unique gluings can be obtained from the usual
 "equalizer" sheaf condition.
 -/
-theorem isSheafUniqueGluing_of_isSheaf_types (Fsh : F.IsSheaf) : F.IsSheafUniqueGluing :=
+theorem isSheafUniqueGluingOfIsSheafTypes (Fsh : F.IsSheaf) : F.IsSheafUniqueGluing :=
   by
   rw [is_sheaf_iff_is_sheaf_equalizer_products] at Fsh 
   intro ι U sf hsf
@@ -212,15 +205,14 @@ theorem isSheafUniqueGluing_of_isSheaf_types (Fsh : F.IsSheaf) : F.IsSheafUnique
     rw [← is_gluing_iff_eq_res F U]
     convert hy
     rw [inv_hom_id_apply]
-#align Top.presheaf.is_sheaf_unique_gluing_of_is_sheaf_types TopCat.Presheaf.isSheafUniqueGluing_of_isSheaf_types
--/
+#align Top.presheaf.is_sheaf_unique_gluing_of_is_sheaf_types TopCat.Presheaf.isSheafUniqueGluingOfIsSheafTypes
 
 #print TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types /-
 /-- For type-valued presheaves, the sheaf condition in terms of unique gluings is equivalent to the
 usual sheaf condition in terms of equalizer diagrams.
 -/
 theorem isSheaf_iff_isSheafUniqueGluing_types : F.IsSheaf ↔ F.IsSheafUniqueGluing :=
-  Iff.intro (isSheafUniqueGluing_of_isSheaf_types F) (isSheaf_of_isSheafUniqueGluing_types F)
+  Iff.intro (isSheafUniqueGluingOfIsSheafTypes F) (isSheaf_of_isSheafUniqueGluing_types F)
 #align Top.presheaf.is_sheaf_iff_is_sheaf_unique_gluing_types TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types
 -/
 

lake-manifest.json

@@ -4,23 +4,23 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "d4266f4f116fbc5c7248ee5ca0d0d51254d9b200",
+    "rev": "6b7a334462e82aae3c98ea238490410e0fd7940e",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "d4266f4f116fbc5c7248ee5ca0d0d51254d9b200",
+    "inputRev?": "6b7a334462e82aae3c98ea238490410e0fd7940e",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "08a8af0bc86b066933f76221f69539978a3c9893",
+    "rev": "3ce43c18f614b76e161f911b75a3e1ef641620ff",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "08a8af0bc86b066933f76221f69539978a3c9893",
+    "inputRev?": "3ce43c18f614b76e161f911b75a3e1ef641620ff",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dd2549f76ff763c897fe997061e2625a7d628eaf",
+    "rev": "727fa6aa1113c376ea1873812d1ab5c17a24f1d2",
     "opts": {},
     "name": "std",
     "inputRev?": "main",

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-10-21-06"
+def tag : String := "nightly-2023-10-23-06"
 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"@"d4266f4f116fbc5c7248ee5ca0d0d51254d9b200"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6b7a334462e82aae3c98ea238490410e0fd7940e"
 
 @[default_target]
 lean_lib Mathbin where