bump to nightly-2023-06-24-07

mathlib commit leanprover-community/mathlib@93f8809

Mathbin/Algebra/Algebra/Unitization.lean

@@ -699,10 +699,10 @@ theorem algebraMap_eq_inl : ⇑(algebraMap R (Unitization R A)) = inl :=
 #align unitization.algebra_map_eq_inl Unitization.algebraMap_eq_inl
 -/
 
-#print Unitization.algebraMap_eq_inl_hom /-
-theorem algebraMap_eq_inl_hom : algebraMap R (Unitization R A) = inlRingHom R A :=
+#print Unitization.algebraMap_eq_inlRingHom /-
+theorem algebraMap_eq_inlRingHom : algebraMap R (Unitization R A) = inlRingHom R A :=
   rfl
-#align unitization.algebra_map_eq_inl_hom Unitization.algebraMap_eq_inl_hom
+#align unitization.algebra_map_eq_inl_hom Unitization.algebraMap_eq_inlRingHom
 -/
 
 #print Unitization.fstHom /-

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "ebb4637a472639c8d1a6e2b8bbda3134d9335104",
+    "rev": "86ed8344a9a6b93630b069311a67c0481dbd7edc",
     "name": "lean3port",
-    "inputRev?": "ebb4637a472639c8d1a6e2b8bbda3134d9335104"}},
+    "inputRev?": "86ed8344a9a6b93630b069311a67c0481dbd7edc"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "750b7536599c7b0924e12fe79d0522b8554125c9",
+    "rev": "ab70224ae9d908070fdbd34f87a628ef3658640a",
     "name": "mathlib",
-    "inputRev?": "750b7536599c7b0924e12fe79d0522b8554125c9"}},
+    "inputRev?": "ab70224ae9d908070fdbd34f87a628ef3658640a"}},
   {"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-24-05"
+def tag : String := "nightly-2023-06-24-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"@"ebb4637a472639c8d1a6e2b8bbda3134d9335104"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"86ed8344a9a6b93630b069311a67c0481dbd7edc"
 
 @[default_target]
 lean_lib Mathbin where