diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index f4d352eec856..16cd0925e8df 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -12,6 +12,7 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
+import Std.Data.HashMap
 
 namespace Lean.Elab.Command
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 2ea1877310b4..dc4ac7ffce49 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -16,6 +16,7 @@ import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
 import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Elab.DeclarationRange
+import Std.Data.HashMap
 
 namespace Lean.Elab
 open Lean.Parser.Term