diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index f09f51d3463c..e308041468b1 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -677,7 +677,7 @@ def initAndRunWatchdogAux : ServerM Unit := do
 def findWorkerPath : IO System.FilePath := do
   let mut workerPath ← IO.appPath
   if let some path := (←IO.getEnv "LEAN_SYSROOT") then
-    workerPath := System.FilePath.mk path / "bin" / "lean" |>.withExtension System.FilePath.exeExtension
+    workerPath := System.FilePath.mk path / "bin" / "lean" |>.addExtension System.FilePath.exeExtension
   if let some path := (←IO.getEnv "LEAN_WORKER_PATH") then
     workerPath := System.FilePath.mk path
   return workerPath
diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean
index e599f87add14..df8a322915c0 100644
--- a/src/lake/Lake/Config/InstallPath.lean
+++ b/src/lake/Lake/Config/InstallPath.lean
@@ -12,7 +12,7 @@ namespace Lake
 
 /-- Standard path of `elan` in a Elan installation. -/
 def elanExe (home : FilePath) :=
-  home / "bin" / "elan" |>.withExtension FilePath.exeExtension
+  home / "bin" / "elan" |>.addExtension FilePath.exeExtension
 
 /-- Information about the local Elan setup. -/
 structure ElanInstall where
@@ -24,19 +24,19 @@ structure ElanInstall where
 
 /-- Standard path of `lean` in a Lean installation. -/
 def leanExe (sysroot : FilePath) :=
-  sysroot / "bin" / "lean" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "lean" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `leanc` in a Lean installation. -/
 def leancExe (sysroot : FilePath) :=
-  sysroot / "bin" / "leanc" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "leanc" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `llvm-ar` in a Lean installation. -/
 def leanArExe (sysroot : FilePath) :=
-  sysroot / "bin" / "llvm-ar" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "llvm-ar" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `clang` in a Lean installation. -/
 def leanCcExe (sysroot : FilePath) :=
-  sysroot / "bin" / "clang" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "clang" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `libleanshared` in a Lean installation. -/
 def leanSharedLib (sysroot : FilePath) :=
@@ -45,7 +45,7 @@ def leanSharedLib (sysroot : FilePath) :=
       sysroot / "bin"
     else
       sysroot / "lib" / "lean"
-  dir / "libleanshared" |>.withExtension sharedLibExt
+  dir / "libleanshared" |>.addExtension sharedLibExt
 
 /-- Path information about the local Lean installation. -/
 structure LeanInstall where
@@ -80,7 +80,7 @@ def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
 
 /-- Standard path of `lake` in a Lake installation. -/
 def lakeExe (buildHome : FilePath) :=
-  buildHome / "bin" / "lake" |>.withExtension FilePath.exeExtension
+  buildHome / "bin" / "lake" |>.addExtension FilePath.exeExtension
 
 /-- Path information about the local Lake installation. -/
 structure LakeInstall where
@@ -203,7 +203,7 @@ try to return their joint home by assuming they are both located at `<home>/bin`
 def findLakeLeanJointHome? : BaseIO (Option FilePath) := do
   if let .ok appPath ← IO.appPath.toBaseIO then
     if let some appDir := appPath.parent then
-      let leanExe := appDir / "lean" |>.withExtension FilePath.exeExtension
+      let leanExe := appDir / "lean" |>.addExtension FilePath.exeExtension
       if (← leanExe.pathExists) then
         return appDir.parent
   return none
diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean
index a145f2d507f7..d9477f01eb02 100644
--- a/src/lake/Lake/Config/LeanExe.lean
+++ b/src/lake/Lake/Config/LeanExe.lean
@@ -61,7 +61,7 @@ The file name of binary executable
 (i.e., `exeName` plus the platform's `exeExtension`).
 -/
 @[inline] def fileName (self : LeanExe) : FilePath :=
-  FilePath.withExtension self.config.exeName FilePath.exeExtension
+  FilePath.addExtension self.config.exeName FilePath.exeExtension
 
 /-- The path to the executable in the package's `binDir`. -/
 @[inline] def file (self : LeanExe) : FilePath :=
diff --git a/tests/lean/filePath.lean b/tests/lean/filePath.lean
index ee4915ada5d8..77928c86d3e5 100644
--- a/tests/lean/filePath.lean
+++ b/tests/lean/filePath.lean
@@ -30,3 +30,5 @@ def norm (f : FilePath) : String :=
 #eval norm <| FilePath.withExtension "a/b.tar.gz" "xz"
 #eval norm <| FilePath.withExtension "a/b.tar.gz" ""
 #eval norm <| FilePath.withExtension "a/b" "tar.gz"
+
+#eval norm <| FilePath.addExtension "a/b.tar.gz" "bak"
diff --git a/tests/lean/filePath.lean.expected.out b/tests/lean/filePath.lean.expected.out
index da429a1e7675..7edaa5883466 100644
--- a/tests/lean/filePath.lean.expected.out
+++ b/tests/lean/filePath.lean.expected.out
@@ -17,3 +17,4 @@ none
 "a/b.tar.xz"
 "a/b.tar"
 "a/b.tar.gz"
+"a/b.tar.xz.bak"