diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean
index d41a4d07f3551..7df6126811ac3 100644
--- a/Mathlib/SetTheory/Game/Basic.lean
+++ b/Mathlib/SetTheory/Game/Basic.lean
@@ -98,11 +98,11 @@ instance instPartialOrderGame : PartialOrder Game where
 /-- The less or fuzzy relation on games.
 
 If `0 ⧏ x` (less or fuzzy with), then Left can win `x` as the first player. -/
-def Lf : Game → Game → Prop :=
-  Quotient.lift₂ PGame.Lf fun _ _ _ _ hx hy => propext (lf_congr hx hy)
-#align game.lf SetTheory.Game.Lf
+def LF : Game → Game → Prop :=
+  Quotient.lift₂ PGame.LF fun _ _ _ _ hx hy => propext (lf_congr hx hy)
+#align game.lf SetTheory.Game.LF
 
-local infixl:50 " ⧏ " => Lf
+local infixl:50 " ⧏ " => LF
 
 /-- On `Game`, simp-normal inequalities should use as few negations as possible. -/
 @[simp]
@@ -118,8 +118,8 @@ theorem not_lf : ∀ {x y : Game}, ¬x ⧏ y ↔ y ≤ x := by
   exact PGame.not_lf
 #align game.not_lf SetTheory.Game.not_lf
 
--- porting note: had to replace ⧏ with Lf, otherwise cannot differentiate with the operator on PGame
-instance : IsTrichotomous Game Lf :=
+-- porting note: had to replace ⧏ with LF, otherwise cannot differentiate with the operator on PGame
+instance : IsTrichotomous Game LF :=
   ⟨by
     rintro ⟨x⟩ ⟨y⟩
     change _ ∨ ⟦x⟧ = ⟦y⟧ ∨ _
@@ -136,7 +136,7 @@ theorem PGame.le_iff_game_le {x y : PGame} : x ≤ y ↔ (⟦x⟧ : Game) ≤ 
   Iff.rfl
 #align game.pgame.le_iff_game_le SetTheory.Game.PGame.le_iff_game_le
 
-theorem PGame.lf_iff_game_lf {x y : PGame} : PGame.Lf x y ↔ ⟦x⟧ ⧏ ⟦y⟧ :=
+theorem PGame.lf_iff_game_lf {x y : PGame} : PGame.LF x y ↔ ⟦x⟧ ⧏ ⟦y⟧ :=
   Iff.rfl
 #align game.pgame.lf_iff_game_lf SetTheory.Game.PGame.lf_iff_game_lf
 
diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean
index f3747528988fa..948f843f6261d 100644
--- a/Mathlib/SetTheory/Game/PGame.lean
+++ b/Mathlib/SetTheory/Game/PGame.lean
@@ -399,12 +399,12 @@ instance le : LE PGame :=
 /-- The less or fuzzy relation on pre-games.
 
 If `0 ⧏ x`, then Left can win `x` as the first player. -/
-def Lf (x y : PGame) : Prop :=
+def LF (x y : PGame) : Prop :=
   ¬y ≤ x
-#align pgame.lf SetTheory.PGame.Lf
+#align pgame.lf SetTheory.PGame.LF
 
 @[inherit_doc]
-scoped infixl:50 " ⧏ " => PGame.Lf
+scoped infixl:50 " ⧏ " => PGame.LF
 
 @[simp]
 protected theorem not_le {x y : PGame} : ¬x ≤ y ↔ y ⧏ x :=
@@ -420,9 +420,9 @@ theorem _root_.LE.le.not_gf {x y : PGame} : x ≤ y → ¬y ⧏ x :=
   not_lf.2
 #align has_le.le.not_gf LE.le.not_gf
 
-theorem Lf.not_ge {x y : PGame} : x ⧏ y → ¬y ≤ x :=
+theorem LF.not_ge {x y : 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
 
 /-- Definition of `x ≤ y` on pre-games, in terms of `⧏`.
 
@@ -454,7 +454,7 @@ The ordering here is chosen so that `or.inl` refer to moves by Left, and `or.inr
 moves by Right. -/
 theorem lf_iff_exists_le {x y : PGame} :
     x ⧏ y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y := by
-  rw [Lf, le_iff_forall_lf, not_and_or]
+  rw [LF, le_iff_forall_lf, not_and_or]
   simp
 #align pgame.lf_iff_exists_le SetTheory.PGame.lf_iff_exists_le
 
@@ -581,8 +581,8 @@ instance : Trans (· ⧏ ·) (· ≤ ·) (· ⧏ ·) := ⟨lf_of_lf_of_le⟩
 alias _root_.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
+alias LF.trans_le := lf_of_lf_of_le
+#align pgame.lf.trans_le SetTheory.PGame.LF.trans_le
 
 @[trans]
 theorem lf_of_lt_of_lf {x y z : PGame} (h₁ : x < y) (h₂ : y ⧏ z) : x ⧏ z :=
@@ -597,8 +597,8 @@ theorem lf_of_lf_of_lt {x y z : PGame} (h₁ : x ⧏ y) (h₂ : y < z) : x ⧏ z
 alias _root_.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
+alias LF.trans_lt := lf_of_lf_of_lt
+#align pgame.lf.trans_lt SetTheory.PGame.LF.trans_lt
 
 theorem moveLeft_lf {x : PGame} : ∀ i, x.moveLeft i ⧏ x :=
   le_rfl.moveLeft_lf
@@ -809,14 +809,14 @@ instance : Trans
     ((· ≤ ·) : PGame → PGame → Prop) where
   trans := le_of_equiv_of_le
 
-theorem Lf.not_equiv {x y : PGame} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
-#align pgame.lf.not_equiv SetTheory.PGame.Lf.not_equiv
+theorem LF.not_equiv {x y : PGame} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
+#align pgame.lf.not_equiv SetTheory.PGame.LF.not_equiv
 
-theorem Lf.not_equiv' {x y : PGame} (h : x ⧏ y) : ¬(y ≈ x) := fun h' => h.not_ge h'.1
-#align pgame.lf.not_equiv' SetTheory.PGame.Lf.not_equiv'
+theorem LF.not_equiv' {x y : PGame} (h : x ⧏ y) : ¬(y ≈ x) := fun h' => h.not_ge h'.1
+#align pgame.lf.not_equiv' SetTheory.PGame.LF.not_equiv'
 
-theorem Lf.not_gt {x y : PGame} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le
-#align pgame.lf.not_gt SetTheory.PGame.Lf.not_gt
+theorem LF.not_gt {x y : PGame} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le
+#align pgame.lf.not_gt SetTheory.PGame.LF.not_gt
 
 theorem le_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ ≤ y₁) : x₂ ≤ y₂ :=
   hx.2.trans (h.trans hy.1)
diff --git a/Mathlib/SetTheory/Game/Short.lean b/Mathlib/SetTheory/Game/Short.lean
index 18bbc42ca1dc8..353e43f87ddaa 100644
--- a/Mathlib/SetTheory/Game/Short.lean
+++ b/Mathlib/SetTheory/Game/Short.lean
@@ -274,36 +274,36 @@ instance shortBit1 (x : PGame.{u}) [Short x] : Short (bit1 x) := by dsimp [bit1]
 We build `Decidable (x ≤ y)` and `Decidable (x ⧏ y)` in a simultaneous induction.
 Instances for the two projections separately are provided below.
 -/
-def leLfDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤ y) × Decidable (x ⧏ y)
+def leLFDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤ y) × Decidable (x ⧏ y)
   | mk xl xr xL xR, mk yl yr yL yR, shortx, shorty => by
     constructor
     · refine' @decidable_of_iff' _ _ mk_le_mk (id _)
       apply @And.decidable _ _ ?_ ?_
       · apply @Fintype.decidableForallFintype xl _ ?_ _
         intro i
-        apply (leLfDecidable _ _).2
+        apply (leLFDecidable _ _).2
       · apply @Fintype.decidableForallFintype yr _ ?_ _
         intro i
-        apply (leLfDecidable _ _).2
+        apply (leLFDecidable _ _).2
     · refine' @decidable_of_iff' _ _ mk_lf_mk (id _)
       apply @Or.decidable _ _ ?_ ?_
       · apply @Fintype.decidableExistsFintype yl _ ?_ _
         intro i
-        apply (leLfDecidable _ _).1
+        apply (leLFDecidable _ _).1
       · apply @Fintype.decidableExistsFintype xr _ ?_ _
         intro i
-        apply (leLfDecidable _ _).1
+        apply (leLFDecidable _ _).1
 -- Porting note: In Lean 3 `using_well_founded` didn't need this to be explicit.
-termination_by leLfDecidable x y _ _ => Prod.mk x y
+termination_by leLFDecidable x y _ _ => Prod.mk x y
 -- Porting note: `decreasing_by pgame_wf_tac` is no longer needed.
-#align pgame.le_lf_decidable SetTheory.PGame.leLfDecidable
+#align pgame.le_lf_decidable SetTheory.PGame.leLFDecidable
 
 instance leDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ≤ y) :=
-  (leLfDecidable x y).1
+  (leLFDecidable x y).1
 #align pgame.le_decidable SetTheory.PGame.leDecidable
 
 instance lfDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ⧏ y) :=
-  (leLfDecidable x y).2
+  (leLFDecidable x y).2
 #align pgame.lf_decidable SetTheory.PGame.lfDecidable
 
 instance ltDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x < y) :=
diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean
index 075a1a0303122..007650831d182 100644
--- a/Mathlib/SetTheory/Surreal/Basic.lean
+++ b/Mathlib/SetTheory/Surreal/Basic.lean
@@ -135,15 +135,15 @@ theorem le_of_lf {x y : PGame} (h : x ⧏ y) (ox : Numeric x) (oy : Numeric y) :
   not_lf.1 (lf_asymm ox oy h)
 #align pgame.le_of_lf SetTheory.PGame.le_of_lf
 
-alias Lf.le := le_of_lf
-#align pgame.lf.le SetTheory.PGame.Lf.le
+alias LF.le := le_of_lf
+#align pgame.lf.le SetTheory.PGame.LF.le
 
 theorem lt_of_lf {x y : PGame} (h : x ⧏ y) (ox : Numeric x) (oy : Numeric y) : x < y :=
   (lt_or_fuzzy_of_lf h).resolve_right (not_fuzzy_of_le (h.le ox oy))
 #align pgame.lt_of_lf SetTheory.PGame.lt_of_lf
 
-alias Lf.lt := lt_of_lf
-#align pgame.lf.lt SetTheory.PGame.Lf.lt
+alias LF.lt := lt_of_lf
+#align pgame.lf.lt SetTheory.PGame.LF.lt
 
 theorem lf_iff_lt {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x ⧏ y ↔ x < y :=
   ⟨fun h => h.lt ox oy, lf_of_lt⟩