diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean
index 984d630a22c5..2d6ba911b2a0 100644
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
 prelude
+import Lean.Data.HashMap
 import Lean.Runtime
 import Lean.Compiler.NameMangling
 import Lean.Compiler.ExportAttr
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 1cca0f329391..6cb6fa9fa4df 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Power2
 import Lean.Data.AssocList
+import Std.Data.HashMap.Basic
+import Std.Data.HashMap.Raw
 namespace Lean
 
 def HashMapBucket (α : Type u) (β : Type v) :=
@@ -269,4 +271,11 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
 
+attribute [deprecated Std.HashMap] HashMap
+attribute [deprecated Std.HashMap.Raw] HashMapImp
+attribute [deprecated Std.HashMap.Raw.empty] mkHashMapImp
+attribute [deprecated Std.HashMap.empty] mkHashMap
+attribute [deprecated Std.HashMap.empty] HashMap.empty
+attribute [deprecated Std.HashMap.ofList] HashMap.ofList
+
 end Lean.HashMap
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index 5d434762af5c..30ff5814ff3d 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Power2
 import Init.Data.List.Control
+import Std.Data.HashSet.Basic
+import Std.Data.HashSet.Raw
 namespace Lean
 universe u v w
 
@@ -217,3 +219,9 @@ def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.ru
 def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
   t.fold (init := s) fun s a => s.insert a
   -- We don't use `insertMany` here because it gives weird universes.
+
+attribute [deprecated Std.HashSet] HashSet
+attribute [deprecated Std.HashSet.Raw] HashSetImp
+attribute [deprecated Std.HashSet.Raw.empty] mkHashSetImp
+attribute [deprecated Std.HashSet.empty] mkHashSet
+attribute [deprecated Std.HashSet.empty] HashSet.empty
diff --git a/src/Lean/Data/NameMap.lean b/src/Lean/Data/NameMap.lean
index 855917e465ea..6593e748bc22 100644
--- a/src/Lean/Data/NameMap.lean
+++ b/src/Lean/Data/NameMap.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashSet.Basic
+import Lean.Data.HashSet
 import Lean.Data.RBMap
 import Lean.Data.RBTree
 import Lean.Data.SSet
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 6b031a2e12f3..54a101731db8 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashMap.Basic
+import Lean.Data.HashMap
 import Lean.Data.PersistentHashMap
 universe u v w w'
 
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index eaab597c450a..18074c980629 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -8,6 +8,7 @@ import Init.Control.StateRef
 import Init.Data.Array.BinSearch
 import Init.Data.Stream
 import Lean.ImportingFlag
+import Lean.Data.HashMap
 import Lean.Data.SMap
 import Lean.Declaration
 import Lean.LocalContext
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 2e35574779a7..393b5f431b82 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.QSort
+import Lean.Data.HashMap
+import Lean.Data.HashSet
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 import Lean.Hygiene
diff --git a/src/Lean/Meta/Canonicalizer.lean b/src/Lean/Meta/Canonicalizer.lean
index 85fd5b5a0232..11da16a980e0 100644
--- a/src/Lean/Meta/Canonicalizer.lean
+++ b/src/Lean/Meta/Canonicalizer.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Data.HashMap
 import Lean.Util.ShareCommon
 import Lean.Meta.Basic
 import Lean.Meta.FunInfo
diff --git a/src/Lean/Util/Diff.lean b/src/Lean/Util/Diff.lean
index 519d62d59e2c..71956e17a95a 100644
--- a/src/Lean/Util/Diff.lean
+++ b/src/Lean/Util/Diff.lean
@@ -5,6 +5,7 @@ Authors: David Thrane Christiansen
 -/
 prelude
 import Init.Data
+import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 import Init.Omega
 
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index 38128cc71e4b..23f77b402f16 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Control.StateRef
+import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 
 namespace Lean
diff --git a/src/Lean/Util/PtrSet.lean b/src/Lean/Util/PtrSet.lean
index 592fb6f84fe2..56e57aeb06d3 100644
--- a/src/Lean/Util/PtrSet.lean
+++ b/src/Lean/Util/PtrSet.lean
@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Hashable
+import Lean.Data.HashSet
+import Lean.Data.HashMap
 import Std.Data.HashSet.Basic
 import Std.Data.HashMap.Basic
 
diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean
index 206f8cbaa9bb..2bff60132197 100644
--- a/src/Lean/Util/SCC.lean
+++ b/src/Lean/Util/SCC.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.List.Control
+import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 namespace Lean.SCC
 /-!
diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean
index 5948ea3da9c8..65b40dfb062b 100644
--- a/src/Lean/Util/ShareCommon.lean
+++ b/src/Lean/Util/ShareCommon.lean
@@ -13,6 +13,7 @@ import Lean.Data.PersistentHashSet
 open ShareCommon
 namespace Lean.ShareCommon
 
+set_option linter.deprecated false in
 def objectFactory :=
   StateFactory.mk {
     Map := HashMap, mkMap := (mkHashMap ·), mapFind? := (·.find?), mapInsert := (·.insert)
diff --git a/src/lake/Lake/Util/OrdHashSet.lean b/src/lake/Lake/Util/OrdHashSet.lean
index 9287b678fd95..fea3d04a59aa 100644
--- a/src/lake/Lake/Util/OrdHashSet.lean
+++ b/src/lake/Lake/Util/OrdHashSet.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lean.Data.HashSet
 import Std.Data.HashSet.Basic
 
 open Lean