bump to nightly-2023-02-28-08

mathlib commit leanprover-community/mathlib@9da1b35

Mathbin/Topology/MetricSpace/Gluing.lean

@@ -643,7 +643,7 @@ theorem to_glue_commute (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :
   letI := i.to_uniform_space
   funext
   simp only [comp, to_glue_l, to_glue_r]
-  refine' UniformSpace.SeparationQuotient.mk'_eq_mk'.2 (Metric.inseparable_iff.2 _)
+  refine' UniformSpace.SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 _)
   exact glue_dist_glued_points Φ Ψ 0 x
 #align metric.to_glue_commute Metric.to_glue_commute
 
@@ -766,7 +766,7 @@ theorem toInductiveLimit_commute (I : ∀ n, Isometry (f n)) (n : ℕ) :
   letI := inductive_premetric I
   funext
   simp only [comp, to_inductive_limit]
-  refine' UniformSpace.SeparationQuotient.mk'_eq_mk'.2 (Metric.inseparable_iff.2 _)
+  refine' UniformSpace.SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 _)
   show inductive_limit_dist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
   · rw [inductive_limit_dist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, le_rec_on_self,
       le_rec_on_succ, le_rec_on_self, dist_self]

Mathbin/Topology/UniformSpace/Separation.lean

@@ -531,9 +531,11 @@ instance : SeparatedSpace (SeparationQuotient α) :=
 instance [Inhabited α] : Inhabited (SeparationQuotient α) :=
   Quotient.inhabited (separationSetoid α)
 
-theorem mk'_eq_mk' {x y : α} : (⟦x⟧ : SeparationQuotient α) = ⟦y⟧ ↔ Inseparable x y :=
+#print UniformSpace.SeparationQuotient.mk_eq_mk /-
+theorem mk_eq_mk {x y : α} : (⟦x⟧ : SeparationQuotient α) = ⟦y⟧ ↔ Inseparable x y :=
   Quotient.eq''.trans separationRel_iff_inseparable
-#align uniform_space.separation_quotient.mk_eq_mk UniformSpace.SeparationQuotient.mk'_eq_mk'
+#align uniform_space.separation_quotient.mk_eq_mk UniformSpace.SeparationQuotient.mk_eq_mk
+-/
 
 #print UniformSpace.SeparationQuotient.lift /-
 /-- Factoring functions to a separated space through the separation quotient. -/

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "4b6c790ac8453b9b52fb42b88b50945885119dfc",
+    "rev": "e26af3a875b2e4ec95a9327f476edaafbe82cc71",
     "name": "lean3port",
-    "inputRev?": "4b6c790ac8453b9b52fb42b88b50945885119dfc"}},
+    "inputRev?": "e26af3a875b2e4ec95a9327f476edaafbe82cc71"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "917b7089d132cb110f67f6b286dffe15eb05f9b8",
+    "rev": "0ed2027858bb128c9a6cad1700ed045c2ab59139",
     "name": "mathlib",
-    "inputRev?": "917b7089d132cb110f67f6b286dffe15eb05f9b8"}},
+    "inputRev?": "0ed2027858bb128c9a6cad1700ed045c2ab59139"}},
   {"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-02-28-06"
+def tag : String := "nightly-2023-02-28-08"
 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"@"4b6c790ac8453b9b52fb42b88b50945885119dfc"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e26af3a875b2e4ec95a9327f476edaafbe82cc71"
 
 @[default_target]
 lean_lib Mathbin where