diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 596a492739..778bc415e8 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -15,7 +15,7 @@ Lake build functions, which is used by Lake to build any Lake build info.
 This module leverages the index to perform topologically-based recursive builds.
 -/
 
-open Std Lean
+open Lean
 namespace Lake
 
 /--
diff --git a/Lake/Build/Topological.lean b/Lake/Build/Topological.lean
index 8963d69d59..90faeb3370 100644
--- a/Lake/Build/Topological.lean
+++ b/Lake/Build/Topological.lean
@@ -17,7 +17,6 @@ a build store.
 This is called a suspending scheduler in *Build systems à la carte*.
 -/
 
-open Std
 namespace Lake
 
 /-!
diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean
index 45897f6a9e..082977acda 100644
--- a/Lake/Config/Module.lean
+++ b/Lake/Config/Module.lean
@@ -7,7 +7,7 @@ import Lake.Build.Trace
 import Lake.Config.LeanLib
 
 namespace Lake
-open Std System
+open Lean System
 
 /-- A buildable Lean module of a `LeanLib`. -/
 structure Module where
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index bcd6ca38ff..8b1f1c6809 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -12,7 +12,7 @@ import Lake.Config.Dependency
 import Lake.Config.Script
 import Lake.Util.DRBMap
 
-open Std System Lean
+open System Lean
 
 namespace Lake
 
diff --git a/Lake/Load/Elab.lean b/Lake/Load/Elab.lean
index 615a049ffb..98ea541e36 100644
--- a/Lake/Load/Elab.lean
+++ b/Lake/Load/Elab.lean
@@ -14,7 +14,7 @@ open Lean System
 deriving instance BEq, Hashable for Import
 
 /- Cache for the imported header environment of Lake configuration files. -/
-initialize importEnvCache : IO.Ref (Std.HashMap (List Import) Environment) ← IO.mkRef {}
+initialize importEnvCache : IO.Ref (HashMap (List Import) Environment) ← IO.mkRef {}
 
 /-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
 def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
diff --git a/Lake/Load/Materialize.lean b/Lake/Load/Materialize.lean
index 071c130071..c42bc52d5e 100644
--- a/Lake/Load/Materialize.lean
+++ b/Lake/Load/Materialize.lean
@@ -7,7 +7,7 @@ import Lake.Util.Git
 import Lake.Load.Manifest
 import Lake.Config.Dependency
 
-open Std System Lean
+open System Lean
 
 namespace Lake
 
diff --git a/Lake/Util/DRBMap.lean b/Lake/Util/DRBMap.lean
index ef64f4f1d4..b94ac26214 100644
--- a/Lake/Util/DRBMap.lean
+++ b/Lake/Util/DRBMap.lean
@@ -7,11 +7,11 @@ import Lean.Data.RBMap
 import Lake.Util.Compare
 
 namespace Lake
-open Std RBNode
+open Lean RBNode
 
 /-!
-This module includes a dependently typed adaption of the `Std.RBMap`
-defined in `Std.Data.RBMap` module of the Lean core. Most of the code is
+This module includes a dependently typed adaption of the `Lean.RBMap`
+defined in `Lean.Data.RBMap` module of the Lean core. Most of the code is
 copied directly from there with only minor edits.
 -/
 
diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean
index 2641a0363b..18f052aa5a 100644
--- a/Lake/Util/Name.lean
+++ b/Lake/Util/Name.lean
@@ -12,7 +12,7 @@ namespace Lake
 
 export Lean (Name NameMap)
 
-@[inline] def NameMap.empty : NameMap α := Std.RBMap.empty
+@[inline] def NameMap.empty : NameMap α := RBMap.empty
 
 instance : ForIn m (NameMap α) (Name × α) where
   forIn self init f := self.forIn init f
diff --git a/Lake/Util/StoreInsts.lean b/Lake/Util/StoreInsts.lean
index 3a7d2c72cb..e82f41d54f 100644
--- a/Lake/Util/StoreInsts.lean
+++ b/Lake/Util/StoreInsts.lean
@@ -7,7 +7,7 @@ import Lake.Util.DRBMap
 import Lake.Util.Family
 import Lake.Util.Store
 
-open Std Lean
+open Lean
 namespace Lake
 
 instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where