diff --git a/Cache/Hashing.lean b/Cache/Hashing.lean
index 1efb1cc325c6d..489d24f353669 100644
--- a/Cache/Hashing.lean
+++ b/Cache/Hashing.lean
@@ -14,9 +14,9 @@ open System IO
 
 structure HashMemo where
   rootHash : UInt64
-  depsMap  : Std.HashMap FilePath (Array FilePath) := {}
-  cache    : Std.HashMap FilePath (Option UInt64) := {}
-  hashMap  : ModuleHashMap := {}
+  depsMap  : Std.HashMap FilePath (Array FilePath) := ∅
+  cache    : Std.HashMap FilePath (Option UInt64) := ∅
+  hashMap  : ModuleHashMap := ∅
   deriving Inhabited
 
 partial def insertDeps (hashMap : ModuleHashMap) (path : FilePath) (hashMemo : HashMemo) :
@@ -33,7 +33,7 @@ Filters the `hashMap` of a `HashMemo` so that it only contains key/value pairs s
 -/
 def HashMemo.filterByFilePaths (hashMemo : HashMemo) (filePaths : List FilePath) :
     IO ModuleHashMap := do
-  let mut hashMap := default
+  let mut hashMap := ∅
   for filePath in filePaths do
     if hashMemo.hashMap.contains filePath then
       hashMap := insertDeps hashMap filePath hashMemo
diff --git a/Cache/IO.lean b/Cache/IO.lean
index f2fcaf017ffad..b52573f7ebb76 100644
--- a/Cache/IO.lean
+++ b/Cache/IO.lean
@@ -276,13 +276,13 @@ If `keep` is true, the result will contain the entries that do exist;
 if `keep` is false, the result will contain the entries that do not exist.
 -/
 def filterExists (hashMap : ModuleHashMap) (keep : Bool) : IO ModuleHashMap :=
-  hashMap.foldM (init := default) fun acc path hash => do
+  hashMap.foldM (init := ∅) fun acc path hash => do
     let exist ← (CACHEDIR / hash.asLTar).pathExists
     let add := if keep then exist else !exist
     if add then return acc.insert path hash else return acc
 
 def hashes (hashMap : ModuleHashMap) : Lean.RBTree UInt64 compare :=
-  hashMap.fold (init := default) fun acc _ hash => acc.insert hash
+  hashMap.fold (init := ∅) fun acc _ hash => acc.insert hash
 
 end ModuleHashMap
 
@@ -384,7 +384,7 @@ instance : Ord FilePath where
   compare x y := compare x.toString y.toString
 
 /-- Removes all cache files except for what's in the `keep` set -/
-def cleanCache (keep : Lean.RBTree FilePath compare := default) : IO Unit := do
+def cleanCache (keep : Lean.RBTree FilePath compare := ∅) : IO Unit := do
   for path in ← getFilesWithExtension CACHEDIR "ltar" do
     if !keep.contains path then IO.FS.removeFile path
 
diff --git a/Cache/Requests.lean b/Cache/Requests.lean
index c60805031e54c..efbb5163352ae 100644
--- a/Cache/Requests.lean
+++ b/Cache/Requests.lean
@@ -277,7 +277,7 @@ inductive QueryType
 def QueryType.prefix : QueryType → String
   | files   => "&prefix=f/"
   | commits => "&prefix=c/"
-  | all     => default
+  | all     => ""
 
 def formatError {α : Type} : IO α :=
   throw <| IO.userError "Invalid format for curl return"
@@ -299,7 +299,7 @@ def getFilesInfo (q : QueryType) : IO <| List (String × String) := do
   let ret ← IO.runCurl #["-X", "GET", s!"{URL}?comp=list&restype=container{q.prefix}"]
   match ret.splitOn "<Name>" with
   | [] => formatError
-  | [_] => return default
+  | [_] => return []
   | _ :: parts =>
     parts.mapM fun part => match part.splitOn "</Name>" with
       | [name, rest] => match rest.splitOn "<Last-Modified>" with