diff --git a/src/Lean/Setup.lean b/src/Lean/Setup.lean
index b5b25b5d0d..2a987ffc6e 100644
--- a/src/Lean/Setup.lean
+++ b/src/Lean/Setup.lean
@@ -29,7 +29,8 @@ structure Import where
   isExported : Bool := true
   /-- Whether all definitions (transitively) reachable through the -/
   isMeta     : Bool := false
-  deriving Repr, Inhabited, ToJson, FromJson
+  deriving Repr, Inhabited, ToJson, FromJson,
+    BEq, Hashable -- needed by Lake (in `Lake.Load.Elab.Lean`)
 
 instance : Coe Name Import := ⟨({module := ·})⟩
 
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index e65fa08450..b1f275409d 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/src/lake/Lake/Load/Lean/Elab.lean
@@ -21,8 +21,6 @@ open System Lean
 
 namespace Lake
 
-deriving instance BEq, Hashable for Import
-
 /- Cache for the imported header environment of Lake configuration files. -/
 builtin_initialize importEnvCache : IO.Ref (Std.HashMap (Array Import) Environment) ← IO.mkRef {}