diff --git a/Mathbin/Data/Polynomial/Degree/Definitions.lean b/Mathbin/Data/Polynomial/Degree/Definitions.lean
index 3393f58fff..1a4751b876 100644
--- a/Mathbin/Data/Polynomial/Degree/Definitions.lean
+++ b/Mathbin/Data/Polynomial/Degree/Definitions.lean
@@ -270,7 +270,7 @@ theorem degree_ne_of_natDegree_ne {n : ℕ} : p.natDegree ≠ n → degree p ≠
 
 #print Polynomial.natDegree_le_iff_degree_le /-
 theorem natDegree_le_iff_degree_le {n : ℕ} : natDegree p ≤ n ↔ degree p ≤ n :=
-  WithBot.unbot'_bot_le_iff
+  WithBot.unbot'_le_iff
 #align polynomial.nat_degree_le_iff_degree_le Polynomial.natDegree_le_iff_degree_le
 -/
 
diff --git a/Mathbin/Order/GaloisConnection.lean b/Mathbin/Order/GaloisConnection.lean
index d04ea7c174..3a28f35ed2 100644
--- a/Mathbin/Order/GaloisConnection.lean
+++ b/Mathbin/Order/GaloisConnection.lean
@@ -1176,7 +1176,7 @@ coercion form a Galois insertion. -/
 def WithBot.giUnbot'Bot [Preorder α] [OrderBot α] :
     GaloisInsertion (WithBot.unbot' ⊥) (coe : α → WithBot α)
     where
-  gc a b := WithBot.unbot'_bot_le_iff
+  gc a b := WithBot.unbot'_le_iff
   le_l_u a := le_rfl
   choice o ho := o.unbot' ⊥
   choice_eq _ _ := rfl
diff --git a/Mathbin/Order/WithBot.lean b/Mathbin/Order/WithBot.lean
index 5cf496109c..7be9089146 100644
--- a/Mathbin/Order/WithBot.lean
+++ b/Mathbin/Order/WithBot.lean
@@ -480,10 +480,10 @@ theorem le_coe_unbot' [Preorder α] : ∀ (a : WithBot α) (b : α), a ≤ a.unb
 #align with_bot.le_coe_unbot' WithBot.le_coe_unbot'
 -/
 
-#print WithBot.unbot'_bot_le_iff /-
-theorem unbot'_bot_le_iff [LE α] [OrderBot α] {a : WithBot α} {b : α} : a.unbot' ⊥ ≤ b ↔ a ≤ b := by
+#print WithBot.unbot'_le_iff /-
+theorem unbot'_le_iff [LE α] [OrderBot α] {a : WithBot α} {b : α} : a.unbot' ⊥ ≤ b ↔ a ≤ b := by
   cases a <;> simp [none_eq_bot, some_eq_coe]
-#align with_bot.unbot'_bot_le_iff WithBot.unbot'_bot_le_iff
+#align with_bot.unbot'_bot_le_iff WithBot.unbot'_le_iff
 -/
 
 #print WithBot.unbot'_lt_iff /-
diff --git a/lake-manifest.json b/lake-manifest.json
index 9ad0fe8e8f..5629865953 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "1ce0a5a3986b4c41d2282f72802fc3776d8b8381",
+    "rev": "758cb0e8c273df825524e578128e3e94e0c639d3",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "1ce0a5a3986b4c41d2282f72802fc3776d8b8381",
+    "inputRev?": "758cb0e8c273df825524e578128e3e94e0c639d3",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "6f7f5f38aeade5fd16b2d96674a055b3a850e736",
+    "rev": "0fd376a2a6771146b41dfd81b6726431ebc5f2c4",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "6f7f5f38aeade5fd16b2d96674a055b3a850e736",
+    "inputRev?": "0fd376a2a6771146b41dfd81b6726431ebc5f2c4",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
diff --git a/lakefile.lean b/lakefile.lean
index 4fdf26530c..1f3cdea72e 100644
--- a/lakefile.lean
+++ b/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-09-26-06"
+def tag : String := "nightly-2023-09-27-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"@"1ce0a5a3986b4c41d2282f72802fc3776d8b8381"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"758cb0e8c273df825524e578128e3e94e0c639d3"
 
 @[default_target]
 lean_lib Mathbin where