bump to nightly-2023-08-25-23

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/CategoryTheory/Functor/FullyFaithful.lean

@@ -390,7 +390,7 @@ theorem Faithful.div_comp (F : C ⥤ E) [Faithful F] (G : D ⥤ E) [Faithful G]
   by
   cases' F with F_obj _ _ _; cases' G with G_obj _ _ _
   unfold faithful.div Functor.Comp
-  unfold_projs at h_obj 
+  unfold_projs  at h_obj 
   have : F_obj = G_obj ∘ obj := (funext h_obj).symm
   subst this
   congr

Mathbin/Geometry/Manifold/ChartedSpace.lean

@@ -658,10 +658,10 @@ theorem ChartedSpace.secondCountable_of_sigma_compact [SecondCountableTopology H
 #align charted_space.second_countable_of_sigma_compact ChartedSpace.secondCountable_of_sigma_compact
 -/
 
-#print ChartedSpace.locallyCompact /-
+#print ChartedSpace.locallyCompactSpace /-
 /-- If a topological space admits an atlas with locally compact charts, then the space itself
 is locally compact. -/
-theorem ChartedSpace.locallyCompact [LocallyCompactSpace H] : LocallyCompactSpace M :=
+theorem ChartedSpace.locallyCompactSpace [LocallyCompactSpace H] : LocallyCompactSpace M :=
   by
   have :
     ∀ x : M,
@@ -675,7 +675,7 @@ theorem ChartedSpace.locallyCompact [LocallyCompactSpace H] : LocallyCompactSpac
   refine' locallyCompactSpace_of_hasBasis this _
   rintro x s ⟨h₁, h₂, h₃⟩
   exact h₂.image_of_continuous_on ((chart_at H x).continuousOn_symm.mono h₃)
-#align charted_space.locally_compact ChartedSpace.locallyCompact
+#align charted_space.locally_compact ChartedSpace.locallyCompactSpace
 -/
 
 #print ChartedSpace.locallyConnectedSpace /-

Mathbin/Geometry/Manifold/Metrizable.lean

@@ -29,7 +29,7 @@ theorem ManifoldWithCorners.metrizableSpace {E : Type _} [NormedAddCommGroup E]
     [FiniteDimensional ℝ E] {H : Type _} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
     (M : Type _) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] :
     MetrizableSpace M := by
-  haveI := I.locally_compact; haveI := ChartedSpace.locallyCompact H M
+  haveI := I.locally_compact; haveI := ChartedSpace.locallyCompactSpace H M
   haveI : NormalSpace M := normal_of_paracompact_t2
   haveI := I.second_countable_topology
   haveI := ChartedSpace.secondCountable_of_sigma_compact H M

Mathbin/Geometry/Manifold/PartitionOfUnity.lean

@@ -382,7 +382,7 @@ theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s)
   by
   -- First we deduce some missing instances
   haveI : LocallyCompactSpace H := I.locally_compact
-  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
+  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
   haveI : NormalSpace M := normal_of_paracompact_t2
   -- Next we choose a covering by supports of smooth bump functions
   have hB := fun x hx => SmoothBumpFunction.nhds_basis_support I (hU x hx)
@@ -613,7 +613,7 @@ theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (h
     (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U :=
   by
   haveI : LocallyCompactSpace H := I.locally_compact
-  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
+  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
   haveI : NormalSpace M := normal_of_paracompact_t2
   rcases BumpCovering.exists_isSubordinate_of_prop (Smooth I 𝓘(ℝ)) _ hs U ho hU with ⟨f, hf, hfU⟩
   · exact ⟨f.to_smooth_partition_of_unity hf, hfU.to_smooth_partition_of_unity hf⟩

Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -418,8 +418,8 @@ theorem symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {f : H 
 #align model_with_corners.symm_continuous_within_at_comp_right_iff ModelWithCorners.symm_continuousWithinAt_comp_right_iff
 -/
 
-#print ModelWithCorners.locally_compact /-
-protected theorem locally_compact [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) :
+#print ModelWithCorners.locallyCompactSpace /-
+protected theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) :
     LocallyCompactSpace H :=
   by
   have :
@@ -432,7 +432,7 @@ protected theorem locally_compact [LocallyCompactSpace E] (I : ModelWithCorners
   refine' locallyCompactSpace_of_hasBasis this _
   rintro x s ⟨-, hsc⟩
   exact (hsc.inter_right I.closed_range).image I.continuous_symm
-#align model_with_corners.locally_compact ModelWithCorners.locally_compact
+#align model_with_corners.locally_compact ModelWithCorners.locallyCompactSpace
 -/
 
 open TopologicalSpace

lake-manifest.json

@@ -12,10 +12,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "d567cce18f1645c764ad94cea3f35a9d7311d5d2",
+    "rev": "837831b077d6760539f542797a786bb89d531b59",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "d567cce18f1645c764ad94cea3f35a9d7311d5d2",
+    "inputRev?": "837831b077d6760539f542797a786bb89d531b59",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -28,10 +28,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "891adb329938ca3cd49a1d1208f691a98fb0896f",
+    "rev": "7f2ee0917b6e7b4d2a2fbd505eb56448b0cce911",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "891adb329938ca3cd49a1d1208f691a98fb0896f",
+    "inputRev?": "7f2ee0917b6e7b4d2a2fbd505eb56448b0cce911",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",

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-25-21"
+def tag : String := "nightly-2023-08-25-23"
 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"@"d567cce18f1645c764ad94cea3f35a9d7311d5d2"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"837831b077d6760539f542797a786bb89d531b59"
 
 @[default_target]
 lean_lib Mathbin where