diff --git a/ImportGraph.lean b/ImportGraph.lean
index 4905310..183f1ac 100644
--- a/ImportGraph.lean
+++ b/ImportGraph.lean
@@ -1,8 +1,5 @@
 import ImportGraph.Cli
 import ImportGraph.Imports
-import ImportGraph.Lean.List
-import ImportGraph.Lean.NameMap
-import ImportGraph.Lean.Process
-import ImportGraph.Lean.TermUnsafe
-import ImportGraph.Name
+import ImportGraph.CurrentModule
+import ImportGraph.Lean.Name
 import ImportGraph.RequiredModules
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
index 97bad41..814b441 100644
--- a/ImportGraph/Cli.lean
+++ b/ImportGraph/Cli.lean
@@ -5,12 +5,12 @@ Authors: Scott Morrison
 -/
 import Lean
 import Cli.Basic
+import Std.Lean.IO.Process
+import Std.Lean.Util.Path
+import Std.Util.TermUnsafe
 import ImportGraph.CurrentModule
-import ImportGraph.Lean.Path
-import ImportGraph.Lean.Process
-import ImportGraph.Lean.TermUnsafe
 import ImportGraph.Imports
-import ImportGraph.Name
+import ImportGraph.Lean.Name
 
 open Cli
 
@@ -75,3 +75,5 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
         IO.eprintln s!"Make sure you have `graphviz` installed and the file is writable."
         throw ex
   return 0
+
+#minimize_imports
diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean
index df24536..c9e3e86 100644
--- a/ImportGraph/Imports.lean
+++ b/ImportGraph/Imports.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean
+import Std.Lean.NameMap
 import ImportGraph.RequiredModules
-import ImportGraph.Lean.List
-import ImportGraph.Lean.NameMap
 
 /-!
 # Tools for analyzing imports.
@@ -140,7 +139,7 @@ def transitiveFilteredUpstream (node : Name) (graph : NameMap (Array Name))
         | none => transitiveFilteredUpstream source graph filter
         | some repl => .cons repl <| transitiveFilteredUpstream source graph filter
       -- If the node is not filtered, we leave the edge `source → node` intact.
-      else [source]).eraseDup'
+      else [source]).eraseDups
 
 /--
 Filters the `graph` removing all nodes where `filter n` returns false. Additionally,
@@ -159,13 +158,13 @@ def filterGraph (graph : NameMap (Array Name)) (filter : Name → Bool)
   -- and remove all imports starting with `Mathlib` to avoid loops.
   let replImports := graph.toList.bind
     (fun ⟨n, i⟩ => if filter n then i.toList else [])
-    |>.eraseDup' |>.filter (¬ Name.isPrefixOf `Mathlib ·) |>.toArray
+    |>.eraseDups |>.filter (¬ Name.isPrefixOf `Mathlib ·) |>.toArray
   let graph := graph.filterMap (fun node edges => if filter node then none else some <|
     -- If the node `node` is not filtered, modify the `edges` going into `node`.
     edges.toList.bind (fun source =>
       if filter source then
         transitiveFilteredUpstream source graph filter (replacement := replacement)
-      else [source]) |>.eraseDup'.toArray)
+      else [source]) |>.eraseDups.toArray)
   -- Add a replacement node if provided.
   match replacement with
   | none => graph
diff --git a/ImportGraph/Lean/List.lean b/ImportGraph/Lean/List.lean
deleted file mode 100644
index f752363..0000000
--- a/ImportGraph/Lean/List.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-
-
-/-- `eraseDup' l` removes duplicates from `l` (taking only the last occurrence).
-
-Note: imitates `Std`s `List.eraseDup` -/
-@[inline] def List.eraseDup' [DecidableEq α] (l : List α) : List α := -- pwFilter (· ≠ ·)
-  l.foldl (fun IH x => if x ∈ IH then IH else x :: IH) []
diff --git a/ImportGraph/Lean/Name.lean b/ImportGraph/Lean/Name.lean
new file mode 100644
index 0000000..ac1e302
--- /dev/null
+++ b/ImportGraph/Lean/Name.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2023 Jon Eugster. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Eugster
+-/
+import Lean.Data.Name
+import Lean.CoreM
+import Std.Data.HashMap.Basic
+import Std.Lean.Name
+import Std.Lean.SMap
+
+namespace Lean.Name
+
+open Lean Meta Elab
+open Std
+
+/-- Note: copied from `Mathlib.Lean.Name` -/
+private def isBlackListed (declName : Name) : CoreM Bool := do
+  if declName.toString.startsWith "Lean" then return true
+  let env ← getEnv
+  pure $ declName.isInternalDetail
+   || isAuxRecursor env declName
+   || isNoConfusion env declName
+  <||> isRec declName <||> isMatcher declName
+
+/--
+Retrieve all names in the environment satisfying a predicate.
+
+Note: copied from `Mathlib.Lean.Name`
+-/
+def allNames (p : Name → Bool) : CoreM (Array Name) := do
+  (← getEnv).constants.foldM (init := #[]) fun names n _ => do
+    if p n && !(← isBlackListed n) then
+      return names.push n
+    else
+      return names
+
+/--
+Retrieve all names in the environment satisfying a predicate,
+gathered together into a `HashMap` according to the module they are defined in.
+
+Note: copied from `Mathlib.Lean.Name`
+-/
+def allNamesByModule (p : Name → Bool) : CoreM (Std.HashMap Name (Array Name)) := do
+  (← getEnv).constants.foldM (init := Std.HashMap.empty) fun names n _ => do
+    if p n && !(← isBlackListed n) then
+      let some m ← findModuleOf? n | return names
+      -- TODO use `Std.HashMap.modify` when we bump Std4 (or `alter` if that is written).
+      match names.find? m with
+      | some others => return names.insert m (others.push n)
+      | none => return names.insert m #[n]
+    else
+      return names
+
+/-- Returns the very first part of a name: for `ImportGraph.Lean.NameMap` it
+returns `ImportGraph`.
+-/
+def getModule (name : Name) (s := "") : Name :=
+  match name with
+    | .anonymous => s
+    | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}."
+    | .str pre s => getModule pre s
diff --git a/ImportGraph/Lean/NameMap.lean b/ImportGraph/Lean/NameMap.lean
deleted file mode 100644
index 6b7c9b0..0000000
--- a/ImportGraph/Lean/NameMap.lean
+++ /dev/null
@@ -1,42 +0,0 @@
-/-
-Copyright (c) 2023 Jon Eugster. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jon Eugster
--/
-import Lean
--- import Lean.Data.NameMap
-
-/-!
-# Additional functions on `Lean.NameMap`.
-
-We provide `NameMap.filter` and `NameMap.filterMap`.
--/
-
-namespace Lean.NameMap
-
-instance : ForIn m (NameMap β) (Name × β) :=
-  inferInstanceAs <| ForIn m (RBMap Name β _) _
-
-/--
-`filter f m` returns the `NameMap` consisting of all
-"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
--/
-def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α :=
-  m.fold process {}
-where
-  process (r : NameMap α) (n : Name) (i : α) :=
-    if f n i then r.insert n i else r
-
-/--
-`filterMap f m` allows to filter a `NameMap` and simultaneously modify the filtered values.
-
-It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
-The resulting entries with non-`none` value are collected to form the output `NameMap`.
--/
-def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β :=
-  m.fold process {}
-where
-  process (r : NameMap β) (n : Name) (i : α) :=
-    match f n i with
-    | none => r
-    | some b => r.insert n b
diff --git a/ImportGraph/Lean/Path.lean b/ImportGraph/Lean/Path.lean
deleted file mode 100644
index 77d476a..0000000
--- a/ImportGraph/Lean/Path.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2022 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-import Lean
--- import Lean.Elab.Term
-
-/-
-Copied from Std!
-
-# `compile_time_search_path%` term elaborator.
-
-Use this as `searchPathRef.set compile_time_search_path%`.
--/
-
-open Lean System
-
-namespace ImportGraph
-
--- Ideally this instance would be constructed simply by `deriving instance ToExpr for FilePath`
--- but for now we have decided not to upstream the `ToExpr` derive handler from `Mathlib`.
--- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/ToExpr.20derive.20handler/near/386476438
-instance : ToExpr FilePath where
-  toTypeExpr := mkConst ``FilePath
-  toExpr path := mkApp (mkConst ``FilePath.mk) (toExpr path.1)
-
-/--
-Term elaborator that retrieves the current `SearchPath`.
-
-Typical usage is `searchPathRef.set compile_time_search_path%`.
-
-This must not be used in files that are potentially compiled on another machine and then
-imported.
-(That is, if used in an imported file it will embed the search path from whichever machine
-compiled the `.olean`.)
--/
-elab "compile_time_search_path%" : term =>
-  return toExpr (← searchPathRef.get)
diff --git a/ImportGraph/Lean/Process.lean b/ImportGraph/Lean/Process.lean
deleted file mode 100644
index 2b97336..0000000
--- a/ImportGraph/Lean/Process.lean
+++ /dev/null
@@ -1,49 +0,0 @@
-/-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-
-/-!
-# Running external commands.
-
-This is copied from `Mathlib.Lean.IO.Process`.
--/
-
-namespace ImportGraph
-
-open ImportGraph
-
-/--
-Pipe `input` into stdin of the spawned process,
-then return `(exitCode, stdout, stdErr)` upon completion.
-
-Note: duplicated from `Mathlib.Lean.IO.Process`.
--/
--- TODO We could reduce some code duplication by centralising some functions like this,
--- which are used here, in `cache`, and in https://github.com/leanprover-community/llm.
-def runCmdWithInput' (cmd : String) (args : Array String)
-    (input : String := "") (throwFailure := true) : IO (UInt32 × String × String) := do
-  let child ← IO.Process.spawn
-    { cmd := cmd, args := args, stdin := .piped, stdout := .piped, stderr := .piped }
-  let (stdin, child) ← child.takeStdin
-  stdin.putStr input
-  stdin.flush
-  let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
-  let err ← child.stderr.readToEnd
-  let exitCode ← child.wait
-  if exitCode != 0 && throwFailure then
-    throw $ IO.userError err
-  else
-    let out ← IO.ofExcept stdout.get
-    return (exitCode, out, err)
-
-/--
-Pipe `input` into stdin of the spawned process,
-then return the entire content of stdout as a `String` upon completion.
-
-Note: duplicated from `Mathlib.Lean.IO.Process`.
--/
-def runCmdWithInput (cmd : String) (args : Array String)
-    (input : String := "") (throwFailure := true) : IO String := do
-  return (← runCmdWithInput' cmd args input throwFailure).2.1
diff --git a/ImportGraph/Lean/TermUnsafe.lean b/ImportGraph/Lean/TermUnsafe.lean
deleted file mode 100644
index 05c8dba..0000000
--- a/ImportGraph/Lean/TermUnsafe.lean
+++ /dev/null
@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-import Lean.Elab.ElabRules
-import Lean.Meta.Closure
-import Lean.Compiler.ImplementedByAttr
-
--- TODO: COPIED FROM STD!
-
-/-!
-Defines term syntax to call unsafe functions.
-
-```
-def cool :=
-  unsafe (unsafeCast () : Nat)
-
-#eval cool
-```
--/
-
-namespace ImportGraph.TermUnsafe
-open Lean Meta Elab Term
-
-/-- Construct an auxiliary name based on the current declaration name and the given `hint` base. -/
-def mkAuxName (hint : Name) : TermElabM Name :=
-  withFreshMacroScope do
-    let name := (← getDeclName?).getD Name.anonymous ++ hint
-    pure $ addMacroScope (← getMainModule) name (← getCurrMacroScope)
-
-/--
-`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
-body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
-wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
-but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
-the compiler is unable to guarantee the safety of the operation.
-
-For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
-you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
-particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
--/
-elab "unsafe " t:term : term <= expectedType => do
-  let mut t ← elabTerm t expectedType
-  t ← instantiateMVars t
-  if t.hasExprMVar then
-    synthesizeSyntheticMVarsNoPostponing
-    t ← instantiateMVars t
-  if ← logUnassignedUsingErrorInfos (← getMVars t) then throwAbortTerm
-  t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
-  let Expr.const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
-  let ConstantInfo.defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
-  let implName ← mkAuxName `impl
-  addDecl <| Declaration.defnDecl {
-    name := implName
-    type := unsafeDefn.type
-    levelParams := unsafeDefn.levelParams
-    value := ← mkOfNonempty unsafeDefn.type
-    hints := ReducibilityHints.opaque
-    safety := DefinitionSafety.safe
-  }
-  setImplementedBy implName unsafeFn
-  pure $ mkAppN (mkConst implName unsafeLvls) t.getAppArgs
diff --git a/ImportGraph/Name.lean b/ImportGraph/Name.lean
deleted file mode 100644
index 4e625e5..0000000
--- a/ImportGraph/Name.lean
+++ /dev/null
@@ -1,94 +0,0 @@
-/-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-import Lean.Data.SMap
-import Lean
-
-/-!
-Note: [TODO] This file contains random stuff copied from mathlib
-
-
-# Additional functions on `Lean.Name`.
-
-We provide `Name.getModule`,
-and `allNames` and `allNamesByModule`.
--/
-
-
-/-!
-# Extra functions on Lean.SMap
--/
-
-set_option autoImplicit true
-
-open Lean Meta Elab
-
-/-- Monadic fold over a staged map.
-
-Copied from `Mathlib.Lean.SMap`-/
-def Lean.SMap.foldM__importGraph {m : Type w → Type w} [Monad m] [BEq α] [Hashable α]
-    (f : σ → α → β → m σ) (init : σ) (map : Lean.SMap α β) : m σ := do
-  map.map₂.foldlM f (← map.map₁.foldM f init)
-
-/-- Lean 4 makes declarations which are technically not internal
-(that is, head string does not start with `_`) but which sometimes should
-be treated as such. For example, the `to_additive` attribute needs to
-transform `proof_1` constants generated by `Lean.Meta.mkAuxDefinitionFor`.
-This might be better fixed in core, but until then, this method can act
-as a polyfill. This method only looks at the name to decide whether it is probably internal.
-Note: this declaration also occurs as `shouldIgnore` in the Lean 4 file `test/lean/run/printDecls`.
-
-Note: copied from `Mathlib.Lean.Expr.Basic`
--/
-def Lean.Name.isInternal'__importGraph (declName : Name) : Bool :=
-  declName.isInternal ||
-  match declName with
-  | .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s
-  | _        => true
-
-
-/-! The remaining section is copied from `Mathlib.Lean.Name` -/
-namespace ImportGraph
-open ImportGraph
-
-private def isBlackListed (declName : Name) : CoreM Bool := do
-  if declName.toString.startsWith "Lean" then return true
-  let env ← getEnv
-  pure $ declName.isInternal'__importGraph
-   || isAuxRecursor env declName
-   || isNoConfusion env declName
-  <||> isRec declName <||> isMatcher declName
-
-/--
-Retrieve all names in the environment satisfying a predicate.
--/
-def allNames (p : Name → Bool) : CoreM (Array Name) := do
-  (← getEnv).constants.foldM__importGraph (init := #[]) fun names n _ => do
-    if p n && !(← isBlackListed n) then
-      return names.push n
-    else
-      return names
-
-/--
-Retrieve all names in the environment satisfying a predicate,
-gathered together into a `HashMap` according to the module they are defined in.
--/
-def allNamesByModule (p : Name → Bool) : CoreM (HashMap Name (Array Name)) := do
-  (← getEnv).constants.foldM__importGraph (init := HashMap.empty) fun names n _ => do
-    if p n && !(← isBlackListed n) then
-      let some m ← findModuleOf? n | return names
-      -- TODO use `Std.HashMap.modify` when we bump Std4 (or `alter` if that is written).
-      match names.find? m with
-      | some others => return names.insert m (others.push n)
-      | none => return names.insert m #[n]
-    else
-      return names
-
-/-- Returns the very first part of a name: for `Graph.Lean.Data.Set.Basic` it returns `Graph.Lean`. -/
-def getModule (name : Name) (s := "") : Name :=
-  match name with
-    | .anonymous => s
-    | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}."
-    | .str pre s => getModule pre s
diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean
index 53a7290..3ae567d 100644
--- a/ImportGraph/RequiredModules.lean
+++ b/ImportGraph/RequiredModules.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
 import Lean
 
 namespace Lean
diff --git a/lake-manifest.json b/lake-manifest.json
index 9d0ad4d..22ac066 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -9,6 +9,15 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/joneugster/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "baf66c6d1704a93328d759e6347b825f427137c7",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "upstream_from_mathlib_for_graph",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "importGraph",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index a9cdb1c..c400a97 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,6 +5,7 @@ package «importGraph» where
   -- add package configuration options here
 
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
+require std from git "https://github.com/joneugster/std4" @ "upstream_from_mathlib_for_graph"
 
 @[default_target]
 lean_lib «ImportGraph» where
diff --git a/lean-toolchain b/lean-toolchain
index 91ccf6a..3f21e50 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:v4.5.0-rc1