bump to nightly-2023-06-28-07

mathlib commit leanprover-community/mathlib@8b98191

Mathbin/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -34,25 +34,35 @@ namespace UpperHalfPlane
 instance : TopologicalSpace ℍ :=
   Subtype.topologicalSpace
 
+#print UpperHalfPlane.openEmbedding_coe /-
 theorem openEmbedding_coe : OpenEmbedding (coe : ℍ → ℂ) :=
   IsOpen.openEmbedding_subtype_val <| isOpen_lt continuous_const Complex.continuous_im
 #align upper_half_plane.open_embedding_coe UpperHalfPlane.openEmbedding_coe
+-/
 
+#print UpperHalfPlane.embedding_coe /-
 theorem embedding_coe : Embedding (coe : ℍ → ℂ) :=
   embedding_subtype_val
 #align upper_half_plane.embedding_coe UpperHalfPlane.embedding_coe
+-/
 
+#print UpperHalfPlane.continuous_coe /-
 theorem continuous_coe : Continuous (coe : ℍ → ℂ) :=
   embedding_coe.Continuous
 #align upper_half_plane.continuous_coe UpperHalfPlane.continuous_coe
+-/
 
+#print UpperHalfPlane.continuous_re /-
 theorem continuous_re : Continuous re :=
   Complex.continuous_re.comp continuous_coe
 #align upper_half_plane.continuous_re UpperHalfPlane.continuous_re
+-/
 
+#print UpperHalfPlane.continuous_im /-
 theorem continuous_im : Continuous im :=
   Complex.continuous_im.comp continuous_coe
 #align upper_half_plane.continuous_im UpperHalfPlane.continuous_im
+-/
 
 instance : TopologicalSpace.SecondCountableTopology ℍ :=
   TopologicalSpace.Subtype.secondCountableTopology _ _

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "8018d64c9d10f3c750fdee1adbc9598cbcf9d4bf",
+    "rev": "93cc194e9d64c8172a104268589ea8cd85c4f88e",
     "name": "lean3port",
-    "inputRev?": "8018d64c9d10f3c750fdee1adbc9598cbcf9d4bf"}},
+    "inputRev?": "93cc194e9d64c8172a104268589ea8cd85c4f88e"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "1ecea4a93f11da2405de479730f0da6085caa160",
+    "rev": "580093d41630ad3e98758eca8ec9561f46772a8d",
     "name": "mathlib",
-    "inputRev?": "1ecea4a93f11da2405de479730f0da6085caa160"}},
+    "inputRev?": "580093d41630ad3e98758eca8ec9561f46772a8d"}},
   {"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-06-28-05"
+def tag : String := "nightly-2023-06-28-07"
 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"@"8018d64c9d10f3c750fdee1adbc9598cbcf9d4bf"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"93cc194e9d64c8172a104268589ea8cd85c4f88e"
 
 @[default_target]
 lean_lib Mathbin where