diff --git a/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean b/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean
index 088126af3d..89d4a0b319 100644
--- a/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean
+++ b/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean
@@ -874,11 +874,11 @@ variable [Ring R] [AddCommGroup M] [Module R M]
 
 variable {B : BilinForm R M}
 
-#print BilinForm.polar_to_quadratic_form /-
-theorem polar_to_quadratic_form (x y : M) : polar (fun x => B x x) x y = B x y + B y x := by
+#print BilinForm.polar_toQuadraticForm /-
+theorem polar_toQuadraticForm (x y : M) : polar (fun x => B x x) x y = B x y + B y x := by
   simp only [add_assoc, add_sub_cancel', add_right, polar, add_left_inj, add_neg_cancel_left,
     add_left, sub_eq_add_neg _ (B y y), add_comm (B y x) _]
-#align bilin_form.polar_to_quadratic_form BilinForm.polar_to_quadratic_form
+#align bilin_form.polar_to_quadratic_form BilinForm.polar_toQuadraticForm
 -/
 
 #print BilinForm.toQuadraticForm_neg /-
diff --git a/Mathbin/SetTheory/Game/Basic.lean b/Mathbin/SetTheory/Game/Basic.lean
index b4e19cbe81..fa559e11db 100644
--- a/Mathbin/SetTheory/Game/Basic.lean
+++ b/Mathbin/SetTheory/Game/Basic.lean
@@ -82,17 +82,17 @@ instance : PartialOrder SetTheory.Game
   lt := Quotient.lift₂ (· < ·) fun x₁ y₁ x₂ y₂ hx hy => propext (SetTheory.PGame.lt_congr hx hy)
   lt_iff_le_not_le := by rintro ⟨x⟩ ⟨y⟩; exact @lt_iff_le_not_le _ _ x y
 
-#print SetTheory.Game.Lf /-
+#print SetTheory.Game.LF /-
 /-- The less or fuzzy relation on games.
 
 If `0 ⧏ x` (less or fuzzy with), then Left can win `x` as the first player. -/
-def SetTheory.Game.Lf : SetTheory.Game → SetTheory.Game → Prop :=
-  Quotient.lift₂ SetTheory.PGame.Lf fun x₁ y₁ x₂ y₂ hx hy =>
+def SetTheory.Game.LF : SetTheory.Game → SetTheory.Game → Prop :=
+  Quotient.lift₂ SetTheory.PGame.LF fun x₁ y₁ x₂ y₂ hx hy =>
     propext (SetTheory.PGame.lf_congr hx hy)
-#align game.lf SetTheory.Game.Lf
+#align game.lf SetTheory.Game.LF
 -/
 
-local infixl:50 " ⧏ " => SetTheory.Game.Lf
+local infixl:50 " ⧏ " => SetTheory.Game.LF
 
 #print SetTheory.Game.not_le /-
 /-- On `game`, simp-normal inequalities should use as few negations as possible. -/
@@ -121,10 +121,10 @@ theorem SetTheory.PGame.le_iff_game_le {x y : SetTheory.PGame} : x ≤ y ↔ ⟦
   Iff.rfl
 #align pgame.le_iff_game_le SetTheory.PGame.le_iff_game_le
 
-theorem SetTheory.PGame.lf_iff_game_lf {x y : SetTheory.PGame} :
-    SetTheory.PGame.Lf x y ↔ ⟦x⟧ ⧏ ⟦y⟧ :=
+theorem SetTheory.PGame.lF_iff_game_lF {x y : SetTheory.PGame} :
+    SetTheory.PGame.LF x y ↔ ⟦x⟧ ⧏ ⟦y⟧ :=
   Iff.rfl
-#align pgame.lf_iff_game_lf SetTheory.PGame.lf_iff_game_lf
+#align pgame.lf_iff_game_lf SetTheory.PGame.lF_iff_game_lF
 
 theorem SetTheory.PGame.lt_iff_game_lt {x y : SetTheory.PGame} : x < y ↔ ⟦x⟧ < ⟦y⟧ :=
   Iff.rfl
diff --git a/Mathbin/SetTheory/Game/Pgame.lean b/Mathbin/SetTheory/Game/Pgame.lean
index 8a45d580e6..9983c6a0d4 100644
--- a/Mathbin/SetTheory/Game/Pgame.lean
+++ b/Mathbin/SetTheory/Game/Pgame.lean
@@ -455,16 +455,16 @@ instance : LE SetTheory.PGame :=
       (∀ i, ¬le y (x.moveLeft i) (Sym2.GameAdd.snd_fst <| SetTheory.PGame.IsOption.moveLeft i)) ∧
         ∀ j, ¬le (y.moveRight j) x (Sym2.GameAdd.fst_snd <| SetTheory.PGame.IsOption.moveRight j)⟩
 
-#print SetTheory.PGame.Lf /-
+#print SetTheory.PGame.LF /-
 /-- The less or fuzzy relation on pre-games.
 
 If `0 ⧏ x`, then Left can win `x` as the first player. -/
-def SetTheory.PGame.Lf (x y : SetTheory.PGame) : Prop :=
+def SetTheory.PGame.LF (x y : SetTheory.PGame) : Prop :=
   ¬y ≤ x
-#align pgame.lf SetTheory.PGame.Lf
+#align pgame.lf SetTheory.PGame.LF
 -/
 
-scoped infixl:50 " ⧏ " => SetTheory.PGame.Lf
+scoped infixl:50 " ⧏ " => SetTheory.PGame.LF
 
 #print SetTheory.PGame.not_le /-
 @[simp]
@@ -486,10 +486,10 @@ theorem LE.le.not_gf {x y : SetTheory.PGame} : x ≤ y → ¬y ⧏ x :=
 #align has_le.le.not_gf LE.le.not_gf
 -/
 
-#print SetTheory.PGame.Lf.not_ge /-
-theorem SetTheory.PGame.Lf.not_ge {x y : SetTheory.PGame} : x ⧏ y → ¬y ≤ x :=
+#print SetTheory.PGame.LF.not_ge /-
+theorem SetTheory.PGame.LF.not_ge {x y : SetTheory.PGame} : x ⧏ y → ¬y ≤ x :=
   id
-#align pgame.lf.not_ge SetTheory.PGame.Lf.not_ge
+#align pgame.lf.not_ge SetTheory.PGame.LF.not_ge
 -/
 
 #print SetTheory.PGame.le_iff_forall_lf /-
@@ -690,7 +690,7 @@ alias _root_.has_le.le.trans_lf := lf_of_le_of_lf
 #align has_le.le.trans_lf LE.le.trans_lf
 
 alias lf.trans_le := lf_of_lf_of_le
-#align pgame.lf.trans_le SetTheory.PGame.Lf.trans_le
+#align pgame.lf.trans_le SetTheory.PGame.LF.trans_le
 
 #print SetTheory.PGame.lf_of_lt_of_lf /-
 @[trans]
@@ -712,7 +712,7 @@ alias _root_.has_lt.lt.trans_lf := lf_of_lt_of_lf
 #align has_lt.lt.trans_lf LT.lt.trans_lf
 
 alias lf.trans_lt := lf_of_lf_of_lt
-#align pgame.lf.trans_lt SetTheory.PGame.Lf.trans_lt
+#align pgame.lf.trans_lt SetTheory.PGame.LF.trans_lt
 
 #print SetTheory.PGame.moveLeft_lf /-
 theorem SetTheory.PGame.moveLeft_lf {x : SetTheory.PGame} : ∀ i, x.moveLeft i ⧏ x :=
@@ -745,7 +745,7 @@ theorem SetTheory.PGame.mk_lf {xl xr} (xL : xl → SetTheory.PGame) (xR : xr →
 preferred over `⧏`. -/
 theorem SetTheory.PGame.le_of_forall_lt {x y : SetTheory.PGame} (h₁ : ∀ i, x.moveLeft i < y)
     (h₂ : ∀ j, x < y.moveRight j) : x ≤ y :=
-  SetTheory.PGame.le_of_forall_lf (fun i => (h₁ i).Lf) fun i => (h₂ i).Lf
+  SetTheory.PGame.le_of_forall_lf (fun i => (h₁ i).LF) fun i => (h₂ i).LF
 #align pgame.le_of_forall_lt SetTheory.PGame.le_of_forall_lt
 -/
 
@@ -1026,19 +1026,19 @@ theorem SetTheory.PGame.le_of_equiv_of_le {x y z} (h₁ : x ≈ y) : y ≤ z →
 #align pgame.le_of_equiv_of_le SetTheory.PGame.le_of_equiv_of_le
 -/
 
-#print SetTheory.PGame.Lf.not_equiv /-
-theorem SetTheory.PGame.Lf.not_equiv {x y} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
-#align pgame.lf.not_equiv SetTheory.PGame.Lf.not_equiv
+#print SetTheory.PGame.LF.not_equiv /-
+theorem SetTheory.PGame.LF.not_equiv {x y} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
+#align pgame.lf.not_equiv SetTheory.PGame.LF.not_equiv
 -/
 
-#print SetTheory.PGame.Lf.not_equiv' /-
-theorem SetTheory.PGame.Lf.not_equiv' {x y} (h : x ⧏ y) : ¬(y ≈ x) := fun h' => h.not_ge h'.1
-#align pgame.lf.not_equiv' SetTheory.PGame.Lf.not_equiv'
+#print SetTheory.PGame.LF.not_equiv' /-
+theorem SetTheory.PGame.LF.not_equiv' {x y} (h : x ⧏ y) : ¬(y ≈ x) := fun h' => h.not_ge h'.1
+#align pgame.lf.not_equiv' SetTheory.PGame.LF.not_equiv'
 -/
 
-#print SetTheory.PGame.Lf.not_gt /-
-theorem SetTheory.PGame.Lf.not_gt {x y} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le
-#align pgame.lf.not_gt SetTheory.PGame.Lf.not_gt
+#print SetTheory.PGame.LF.not_gt /-
+theorem SetTheory.PGame.LF.not_gt {x y} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le
+#align pgame.lf.not_gt SetTheory.PGame.LF.not_gt
 -/
 
 #print SetTheory.PGame.le_congr_imp /-
@@ -1749,14 +1749,14 @@ decreasing_by pgame_wf_tac
 #print SetTheory.PGame.neg_le_neg_iff /-
 @[simp]
 theorem SetTheory.PGame.neg_le_neg_iff {x y : SetTheory.PGame} : -y ≤ -x ↔ x ≤ y :=
-  neg_le_lf_neg_iff.1
+  neg_le_lF_neg_iff.1
 #align pgame.neg_le_neg_iff SetTheory.PGame.neg_le_neg_iff
 -/
 
 #print SetTheory.PGame.neg_lf_neg_iff /-
 @[simp]
 theorem SetTheory.PGame.neg_lf_neg_iff {x y : SetTheory.PGame} : -y ⧏ -x ↔ x ⧏ y :=
-  neg_le_lf_neg_iff.2
+  neg_le_lF_neg_iff.2
 #align pgame.neg_lf_neg_iff SetTheory.PGame.neg_lf_neg_iff
 -/
 
@@ -2513,7 +2513,7 @@ instance : ZeroLEOneClass SetTheory.PGame :=
 #print SetTheory.PGame.zero_lf_one /-
 @[simp]
 theorem SetTheory.PGame.zero_lf_one : (0 : SetTheory.PGame) ⧏ 1 :=
-  SetTheory.PGame.zero_lt_one.Lf
+  SetTheory.PGame.zero_lt_one.LF
 #align pgame.zero_lf_one SetTheory.PGame.zero_lf_one
 -/
 
diff --git a/Mathbin/SetTheory/Game/Short.lean b/Mathbin/SetTheory/Game/Short.lean
index db3245c85c..ed155eef5d 100644
--- a/Mathbin/SetTheory/Game/Short.lean
+++ b/Mathbin/SetTheory/Game/Short.lean
@@ -282,12 +282,12 @@ instance SetTheory.PGame.shortBit1 (x : SetTheory.PGame.{u}) [SetTheory.PGame.Sh
 #align pgame.short_bit1 SetTheory.PGame.shortBit1
 -/
 
-#print SetTheory.PGame.leLfDecidable /-
+#print SetTheory.PGame.leLFDecidable /-
 /-- Auxiliary construction of decidability instances.
 We build `decidable (x ≤ y)` and `decidable (x ⧏ y)` in a simultaneous induction.
 Instances for the two projections separately are provided below.
 -/
-def SetTheory.PGame.leLfDecidable :
+def SetTheory.PGame.leLFDecidable :
     ∀ (x y : SetTheory.PGame.{u}) [SetTheory.PGame.Short x] [SetTheory.PGame.Short y],
       Decidable (x ≤ y) × Decidable (x ⧏ y)
   | mk xl xr xL xR, mk yl yr yL yR, shortx, shorty =>
@@ -311,20 +311,20 @@ def SetTheory.PGame.leLfDecidable :
         intro i
         apply (@le_lf_decidable _ _ _ _).1 <;> infer_instance
 decreasing_by pgame_wf_tac
-#align pgame.le_lf_decidable SetTheory.PGame.leLfDecidable
+#align pgame.le_lf_decidable SetTheory.PGame.leLFDecidable
 -/
 
 #print SetTheory.PGame.leDecidable /-
 instance SetTheory.PGame.leDecidable (x y : SetTheory.PGame.{u}) [SetTheory.PGame.Short x]
     [SetTheory.PGame.Short y] : Decidable (x ≤ y) :=
-  (SetTheory.PGame.leLfDecidable x y).1
+  (SetTheory.PGame.leLFDecidable x y).1
 #align pgame.le_decidable SetTheory.PGame.leDecidable
 -/
 
 #print SetTheory.PGame.lfDecidable /-
 instance SetTheory.PGame.lfDecidable (x y : SetTheory.PGame.{u}) [SetTheory.PGame.Short x]
     [SetTheory.PGame.Short y] : Decidable (x ⧏ y) :=
-  (SetTheory.PGame.leLfDecidable x y).2
+  (SetTheory.PGame.leLFDecidable x y).2
 #align pgame.lf_decidable SetTheory.PGame.lfDecidable
 -/
 
diff --git a/Mathbin/SetTheory/Surreal/Basic.lean b/Mathbin/SetTheory/Surreal/Basic.lean
index c365b4e544..c3e0510191 100644
--- a/Mathbin/SetTheory/Surreal/Basic.lean
+++ b/Mathbin/SetTheory/Surreal/Basic.lean
@@ -169,7 +169,7 @@ theorem SetTheory.PGame.le_of_lf {x y : SetTheory.PGame} (h : x ⧏ y)
 -/
 
 alias lf.le := le_of_lf
-#align pgame.lf.le SetTheory.PGame.Lf.le
+#align pgame.lf.le SetTheory.PGame.LF.le
 
 #print SetTheory.PGame.lt_of_lf /-
 theorem SetTheory.PGame.lt_of_lf {x y : SetTheory.PGame} (h : x ⧏ y)
@@ -179,7 +179,7 @@ theorem SetTheory.PGame.lt_of_lf {x y : SetTheory.PGame} (h : x ⧏ y)
 -/
 
 alias lf.lt := lt_of_lf
-#align pgame.lf.lt SetTheory.PGame.Lf.lt
+#align pgame.lf.lt SetTheory.PGame.LF.lt
 
 #print SetTheory.PGame.lf_iff_lt /-
 theorem SetTheory.PGame.lf_iff_lt {x y : SetTheory.PGame} (ox : SetTheory.PGame.Numeric x)
diff --git a/lake-manifest.json b/lake-manifest.json
index 6e864a1c35..252de8e38b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -12,10 +12,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "cb676af97e61067af791a964dcf807dcdb53c2e5",
+    "rev": "c591dd8e6a0e60755d35004dafaaaa4cfadcd3a4",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "cb676af97e61067af791a964dcf807dcdb53c2e5",
+    "inputRev?": "c591dd8e6a0e60755d35004dafaaaa4cfadcd3a4",
     "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": "45b31dda2ce52960302b158e06f7d1f539fd94ec",
+    "rev": "193761250a9869327056b499a7f49d676ed5e3a9",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "45b31dda2ce52960302b158e06f7d1f539fd94ec",
+    "inputRev?": "193761250a9869327056b499a7f49d676ed5e3a9",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
diff --git a/lakefile.lean b/lakefile.lean
index d5b5e1790a..9fcaa80129 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-17-06"
+def tag : String := "nightly-2023-09-18-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"@"cb676af97e61067af791a964dcf807dcdb53c2e5"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c591dd8e6a0e60755d35004dafaaaa4cfadcd3a4"
 
 @[default_target]
 lean_lib Mathbin where