diff --git a/Std/CodeAction/Basic.lean b/Std/CodeAction/Basic.lean
index eae9e4cc2b..17f8b2cac8 100644
--- a/Std/CodeAction/Basic.lean
+++ b/Std/CodeAction/Basic.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
-import Std.Lean.Name
 import Std.Lean.InfoTree
 import Std.CodeAction.Attr
 
diff --git a/Std/CodeAction/Misc.lean b/Std/CodeAction/Misc.lean
index 2b480dd006..56b0914b3e 100644
--- a/Std/CodeAction/Misc.lean
+++ b/Std/CodeAction/Misc.lean
@@ -3,9 +3,11 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Lean.Elab.BuiltinTerm
+import Lean.Elab.BuiltinNotation
 import Std.Lean.Name
 import Std.Lean.Position
-import Std.CodeAction.Basic
+import Std.CodeAction.Attr
 
 /-!
 # Miscellaneous code actions
diff --git a/Std/Control/Nondet/Basic.lean b/Std/Control/Nondet/Basic.lean
index 814e52eceb..263ba08d92 100644
--- a/Std/Control/Nondet/Basic.lean
+++ b/Std/Control/Nondet/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Tactic.Lint
+import Std.Tactic.Lint.Misc
 import Std.Data.MLList.Basic
 
 /-!
diff --git a/Std/Data/Array/Init/Lemmas.lean b/Std/Data/Array/Init/Lemmas.lean
index b940197411..39d92676b8 100644
--- a/Std/Data/Array/Init/Lemmas.lean
+++ b/Std/Data/Array/Init/Lemmas.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Std.Tactic.NoMatch
 import Std.Tactic.HaveI
 import Std.Classes.LawfulMonad
+import Std.Data.Fin.Init.Lemmas
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.List.Init.Lemmas
 import Std.Data.Array.Init.Basic
diff --git a/Std/Data/Array/Match.lean b/Std/Data/Array/Match.lean
index 966f67f4a5..f5ff981777 100644
--- a/Std/Data/Array/Match.lean
+++ b/Std/Data/Array/Match.lean
@@ -3,8 +3,8 @@ Copyright (c) 2023 F. G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-import Std.Data.Array.Basic
-import Std.Data.Array.Lemmas
+import Std.Data.Nat.Lemmas
+import Std.Data.Array.Init.Lemmas
 
 namespace Array
 
diff --git a/Std/Data/Int.lean b/Std/Data/Int.lean
index 3f2b36ad95..7bfed88cee 100644
--- a/Std/Data/Int.lean
+++ b/Std/Data/Int.lean
@@ -1,3 +1,4 @@
 import Std.Data.Int.Basic
 import Std.Data.Int.DivMod
+import Std.Data.Int.Gcd
 import Std.Data.Int.Lemmas
diff --git a/Std/Data/Int/DivMod.lean b/Std/Data/Int/DivMod.lean
index 938e2c7497..1c4a45fdd6 100644
--- a/Std/Data/Int/DivMod.lean
+++ b/Std/Data/Int/DivMod.lean
@@ -625,6 +625,8 @@ protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
 
 protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
 
+protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
+
 protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d * e, by rw [Int.mul_assoc]⟩
 
@@ -689,6 +691,14 @@ theorem dvd_natAbs {a b : Int} : a ∣ b.natAbs ↔ a ∣ b :=
   | .inl e => by rw [← e]
   | .inr e => by rw [← Int.dvd_neg, ← e]
 
+theorem natAbs_dvd_self {a : Int} : (a.natAbs : Int) ∣ a := by
+  rw [Int.natAbs_dvd]
+  exact Int.dvd_refl a
+
+theorem dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int) := by
+  rw [Int.dvd_natAbs]
+  exact Int.dvd_refl a
+
 theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
   rw [← natAbs_dvd_natAbs, natAbs_ofNat]
 
diff --git a/Std/Data/Int/Gcd.lean b/Std/Data/Int/Gcd.lean
new file mode 100644
index 0000000000..2e12ac3e86
--- /dev/null
+++ b/Std/Data/Int/Gcd.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Std.Data.Int.DivMod
+import Std.Data.Nat.Gcd
+import Std.Tactic.Simpa
+
+/-!
+# Results about `Int.gcd`.
+-/
+
+namespace Int
+
+theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) ∣ a := by
+  have := Nat.gcd_dvd_left a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) ∣ b := by
+  have := Nat.gcd_dvd_right a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+@[simp] theorem one_gcd {a : Int} : gcd 1 a = 1 := by simp [gcd]
+@[simp] theorem gcd_one {a : Int} : gcd a 1 = 1 := by simp [gcd]
+
+@[simp] theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b := by simp [gcd]
+@[simp] theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b := by simp [gcd]
+
+/-- Computes the least common multiple of two integers, as a `Nat`. -/
+def lcm (m n : Int) : Nat := m.natAbs.lcm n.natAbs
+
+theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
+  simp only [lcm]
+  apply Nat.lcm_ne_zero <;> simpa
+
+theorem dvd_lcm_left {a b : Int} : a ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_left a.natAbs b.natAbs))
+
+theorem dvd_lcm_right {a b : Int} : b ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_right a.natAbs b.natAbs))
+
+@[simp] theorem lcm_self {a : Int} : lcm a a = a.natAbs := Nat.lcm_self _
diff --git a/Std/Data/Int/Lemmas.lean b/Std/Data/Int/Lemmas.lean
index e4896399f1..85ac931b92 100644
--- a/Std/Data/Int/Lemmas.lean
+++ b/Std/Data/Int/Lemmas.lean
@@ -676,6 +676,14 @@ protected theorem lt_of_lt_of_le {a b c : Int} (h₁ : a < b) (h₂ : b ≤ c) :
 protected theorem lt_trans {a b c : Int} (h₁ : a < b) (h₂ : b < c) : a < c :=
   Int.lt_of_le_of_lt (Int.le_of_lt h₁) h₂
 
+instance : Trans (α := Int) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨Int.le_trans⟩
+
+instance : Trans (α := Int) (· < ·) (· ≤ ·) (· < ·) := ⟨Int.lt_of_lt_of_le⟩
+
+instance : Trans (α := Int) (· ≤ ·) (· < ·) (· < ·) := ⟨Int.lt_of_le_of_lt⟩
+
+instance : Trans (α := Int) (· < ·) (· < ·) (· < ·) := ⟨Int.lt_trans⟩
+
 protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
 
 protected theorem min_def (n m : Int) : min n m = if n ≤ m then n else m := rfl
diff --git a/Std/Data/Json.lean b/Std/Data/Json.lean
index a4f7100c59..95486cd148 100644
--- a/Std/Data/Json.lean
+++ b/Std/Data/Json.lean
@@ -3,7 +3,7 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: E.W.Ayers, Wojciech Nawrocki
 -/
-import Std.Lean.Json
+import Lean.Data.Json.FromToJson
 import Lean.Syntax
 
 /-!
diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean
index d04fa79f7c..71540888f8 100644
--- a/Std/Data/List/Basic.lean
+++ b/Std/Data/List/Basic.lean
@@ -7,7 +7,6 @@ import Std.Classes.SetNotation
 import Std.Tactic.NoMatch
 import Std.Data.Option.Init.Lemmas
 import Std.Data.Array.Init.Lemmas
-import Std.Data.List.Init.Attach
 
 namespace List
 
diff --git a/Std/Data/List/Init/Lemmas.lean b/Std/Data/List/Init/Lemmas.lean
index 5ccffccb51..6dca88f867 100644
--- a/Std/Data/List/Init/Lemmas.lean
+++ b/Std/Data/List/Init/Lemmas.lean
@@ -3,7 +3,6 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
-import Std.Data.Fin.Init.Lemmas
 import Std.Classes.SetNotation
 import Std.Logic
 
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 094d647fb3..3ce9de736c 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -5,8 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Std.Control.ForInStep.Lemmas
 import Std.Data.Bool
-import Std.Data.Fin.Lemmas
-import Std.Data.Nat.Lemmas
+import Std.Data.Fin.Basic
 import Std.Data.List.Basic
 import Std.Data.Option.Lemmas
 import Std.Classes.BEq
diff --git a/Std/Data/List/Perm.lean b/Std/Data/List/Perm.lean
index 6bc843ce69..c49139522f 100644
--- a/Std/Data/List/Perm.lean
+++ b/Std/Data/List/Perm.lean
@@ -7,6 +7,7 @@ import Std.Tactic.Relation.Rfl
 import Std.Data.List.Lemmas
 import Std.Data.List.Count
 import Std.Data.List.Pairwise
+import Std.Data.List.Init.Attach
 
 /-!
 # List Permutations
diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 4a5f6b2bc5..9a861fdf18 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -107,6 +107,9 @@ there is some `c` such that `b = a * c`.
 -/
 instance : Dvd Nat := ⟨fun a b => ∃ c, b = a * c⟩
 
+/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
+def lcm (m n : Nat) : Nat := m * n / gcd m n
+
 /-- Sum of a list of natural numbers. -/
 protected def sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
diff --git a/Std/Data/Nat/Gcd.lean b/Std/Data/Nat/Gcd.lean
index ed5514fe0c..e430e3a5a3 100644
--- a/Std/Data/Nat/Gcd.lean
+++ b/Std/Data/Nat/Gcd.lean
@@ -26,9 +26,6 @@ theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
     | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
     n
 
-/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
-def lcm (m n : Nat) : Nat := m * n / gcd m n
-
 /-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/
 @[reducible] def Coprime (m n : Nat) : Prop := gcd m n = 1
 
diff --git a/Std/Data/Option/Basic.lean b/Std/Data/Option/Basic.lean
index 8d0eace1e1..92ea519057 100644
--- a/Std/Data/Option/Basic.lean
+++ b/Std/Data/Option/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Classes.SetNotation
-import Std.Classes.LawfulMonad
 import Std.Tactic.NoMatch
 
 namespace Option
diff --git a/Std/Data/Prod/Lex.lean b/Std/Data/Prod/Lex.lean
index f37998e9e6..1fad8987df 100644
--- a/Std/Data/Prod/Lex.lean
+++ b/Std/Data/Prod/Lex.lean
@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 import Std.Tactic.LeftRight
 import Std.Tactic.RCases
-import Std.Logic
 
 namespace Prod
 
diff --git a/Std/Data/Range/Lemmas.lean b/Std/Data/Range/Lemmas.lean
index 791820c0bb..1ff0fc8b6f 100644
--- a/Std/Data/Range/Lemmas.lean
+++ b/Std/Data/Range/Lemmas.lean
@@ -1,5 +1,6 @@
 import Std.Tactic.ByCases
 import Std.Data.List.Lemmas
+import Std.Data.List.Init.Attach
 
 namespace Std.Range
 
diff --git a/Std/Data/String/Basic.lean b/Std/Data/String/Basic.lean
index 82e6fc1293..072fbe0222 100644
--- a/Std/Data/String/Basic.lean
+++ b/Std/Data/String/Basic.lean
@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg, James Gallicchio, F. G. Dorais
 -/
-
-import Std.Data.Char
 import Std.Data.Nat.Lemmas
 import Std.Data.Array.Match
 
diff --git a/Std/Lean/Json.lean b/Std/Lean/Json.lean
index b8c66e5545..cbb8514fac 100644
--- a/Std/Lean/Json.lean
+++ b/Std/Lean/Json.lean
@@ -3,8 +3,7 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: E.W.Ayers, Mario Carneiro
 -/
-
-import Lean.Data.Json
+import Lean.Data.Json.FromToJson
 import Std.Lean.Float
 
 open Lean
diff --git a/Std/Lean/Meta/Basic.lean b/Std/Lean/Meta/Basic.lean
index 7583fb31cb..b594d2099c 100644
--- a/Std/Lean/Meta/Basic.lean
+++ b/Std/Lean/Meta/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jannis Limperg
 -/
-import Lean.Meta
+import Lean.Elab.Term
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Replace
 import Std.Lean.LocalContext
 
 open Lean Lean.Meta
@@ -291,7 +293,7 @@ def isIndependentOf (L : List MVarId) (g : MVarId) : MetaM Bool := g.withContext
     -- If the goal is a subsingleton, it is independent of any other goals.
     return true
   -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
-  L.allM fun g' => do pure !((← getMVars (← g'.getType)).contains g)
+  L.allM fun g' => do pure !((← getMVarDependencies g').contains g)
 
 /-- Solve a goal by synthesizing an instance. -/
 -- FIXME: probably can just be `g.inferInstance` once leanprover/lean4#2054 is fixed
diff --git a/Std/Lean/Meta/Inaccessible.lean b/Std/Lean/Meta/Inaccessible.lean
index b70ce2b1f2..e308364616 100644
--- a/Std/Lean/Meta/Inaccessible.lean
+++ b/Std/Lean/Meta/Inaccessible.lean
@@ -1,4 +1,9 @@
-import Lean.Meta
+/-
+Copyright (c) 2022 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+import Lean.Meta.InferType
 
 open Lean Lean.Meta
 
diff --git a/Std/Lean/Meta/Simp.lean b/Std/Lean/Meta/Simp.lean
index 334126aeb4..b14a6acabb 100644
--- a/Std/Lean/Meta/Simp.lean
+++ b/Std/Lean/Meta/Simp.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Gabriel Ebner, Floris van Doorn
 -/
+import Lean.Elab.Tactic.Simp
 import Std.Tactic.OpenPrivate
-import Std.Lean.Meta.DiscrTree
 
 /-!
 # Helper functions for using the simplifier.
diff --git a/Std/Lean/Meta/UnusedNames.lean b/Std/Lean/Meta/UnusedNames.lean
index 3022af001c..76c13ef81c 100644
--- a/Std/Lean/Meta/UnusedNames.lean
+++ b/Std/Lean/Meta/UnusedNames.lean
@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
-import Lean.Meta
 import Std.Data.String.Basic
 
 open Lean Lean.Meta
diff --git a/Std/Lean/System/IO.lean b/Std/Lean/System/IO.lean
index 973d822918..02950c85be 100644
--- a/Std/Lean/System/IO.lean
+++ b/Std/Lean/System/IO.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Std.Data.List.Lemmas
-import Std.Data.MLList.Basic
 
 /-!
 # Functions for manipulating a list of tasks
diff --git a/Std/Lean/Util/EnvSearch.lean b/Std/Lean/Util/EnvSearch.lean
index e465953d94..df6b99d97a 100644
--- a/Std/Lean/Util/EnvSearch.lean
+++ b/Std/Lean/Util/EnvSearch.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Shing Tak Lam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
-import Lean.Modifiers
 import Std.Tactic.Lint.Misc
 
 namespace Lean
diff --git a/Std/Tactic/Case.lean b/Std/Tactic/Case.lean
index 1686e2439a..0e24234244 100644
--- a/Std/Tactic/Case.lean
+++ b/Std/Tactic/Case.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Lean.Elab.Tactic
+import Lean.Elab.Tactic.Conv.Pattern
 
 /-!
 # Extensions to the `case` tactic
diff --git a/Std/Tactic/FalseOrByContra.lean b/Std/Tactic/FalseOrByContra.lean
index 61943fecff..bcf9a9e125 100644
--- a/Std/Tactic/FalseOrByContra.lean
+++ b/Std/Tactic/FalseOrByContra.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Lean.Expr
+import Lean.Elab.Tactic.Basic
 import Std.Lean.Meta.Basic
 
 /-!
diff --git a/Std/Tactic/LibrarySearch.lean b/Std/Tactic/LibrarySearch.lean
index 48b3cbaa12..61dbc45cbc 100644
--- a/Std/Tactic/LibrarySearch.lean
+++ b/Std/Tactic/LibrarySearch.lean
@@ -7,6 +7,7 @@ import Std.Lean.CoreM
 import Std.Lean.Expr
 import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.LazyDiscrTree
+import Std.Data.Option.Basic
 import Std.Tactic.SolveByElim
 import Std.Util.Pickle
 
diff --git a/Std/Tactic/Lint/Basic.lean b/Std/Tactic/Lint/Basic.lean
index d4e51e42c6..16f89daf29 100644
--- a/Std/Tactic/Lint/Basic.lean
+++ b/Std/Tactic/Lint/Basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
 -/
-
 import Std.Util.TermUnsafe
-import Std.Lean.NameMapAttribute
+
 open Lean Meta
 
 namespace Std.Tactic.Lint
diff --git a/Std/Tactic/Omega/Coeffs/IntList.lean b/Std/Tactic/Omega/Coeffs/IntList.lean
index 1877294382..bcae0c9927 100644
--- a/Std/Tactic/Omega/Coeffs/IntList.lean
+++ b/Std/Tactic/Omega/Coeffs/IntList.lean
@@ -1,5 +1,4 @@
 import Std.Tactic.Omega.IntList
-import Std.Tactic.Omega.MinNatAbs
 
 /-!
 # `Coeffs` as a wrapper for `IntList`
diff --git a/Std/Tactic/Omega/Constraint.lean b/Std/Tactic/Omega/Constraint.lean
index c1ac082a18..a4834d0936 100644
--- a/Std/Tactic/Omega/Constraint.lean
+++ b/Std/Tactic/Omega/Constraint.lean
@@ -3,9 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import Std.Classes.Order
 import Std.Tactic.RCases
 import Std.Tactic.NormCast
-import Std.Tactic.Omega.OmegaM
+import Std.Tactic.Omega.Coeffs.IntList
 
 /-!
 A `Constraint` consists of an optional lower and upper bound (inclusive),
diff --git a/Std/Tactic/Omega/Core.lean b/Std/Tactic/Omega/Core.lean
index 73e05e74eb..654319f512 100644
--- a/Std/Tactic/Omega/Core.lean
+++ b/Std/Tactic/Omega/Core.lean
@@ -5,7 +5,8 @@ Authors: Scott Morrison
 -/
 import Std.Tactic.Omega.OmegaM
 import Std.Tactic.Omega.Constraint
-import Std.Data.HashMap
+import Std.Tactic.Omega.MinNatAbs
+import Std.Data.HashMap.Basic
 
 open Lean (HashSet)
 
diff --git a/Std/Tactic/Relation/Symm.lean b/Std/Tactic/Relation/Symm.lean
index 2d9f68b1be..2369a4efd6 100644
--- a/Std/Tactic/Relation/Symm.lean
+++ b/Std/Tactic/Relation/Symm.lean
@@ -3,6 +3,8 @@ Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
 -/
+import Lean.Meta.Reduce
+import Lean.Elab.Tactic.Location
 import Std.Lean.Meta.Basic
 
 /-!
diff --git a/Std/Tactic/SolveByElim.lean b/Std/Tactic/SolveByElim.lean
index 71bd1bfa51..773472abed 100644
--- a/Std/Tactic/SolveByElim.lean
+++ b/Std/Tactic/SolveByElim.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, David Renshaw
 -/
-import Std.Data.Option.Basic
 import Std.Data.Sum.Basic
 import Std.Tactic.LabelAttr
 import Std.Tactic.Relation.Symm
diff --git a/Std/Util/ProofWanted.lean b/Std/Util/ProofWanted.lean
index ef6955f550..97f1473f70 100644
--- a/Std/Util/ProofWanted.lean
+++ b/Std/Util/ProofWanted.lean
@@ -5,7 +5,6 @@ Authors: David Thrane Christiansen
 -/
 import Lean.Elab.Exception
 import Lean.Elab.Command
-import Lean.Parser
 
 
 open Lean Parser Elab Command
diff --git a/test/isIndependentOf.lean b/test/isIndependentOf.lean
new file mode 100644
index 0000000000..74348f1d2d
--- /dev/null
+++ b/test/isIndependentOf.lean
@@ -0,0 +1,43 @@
+import Std.Tactic.PermuteGoals
+import Std.Tactic.GuardMsgs
+
+open Lean Meta Elab.Tactic
+
+elab "check_indep" : tactic => do
+  match ← getGoals with
+  | [] => throwError "Expected goal"
+  | g :: l =>
+    let res := if ←g.isIndependentOf l then "" else "not "
+    let t ← instantiateMVars (← g.getType)
+    logWarning s!"{←ppExpr (.mvar g)} : {←ppExpr t} is {res}independent of:"
+    l.forM fun g' => do
+      logInfo s!"  {←ppExpr (.mvar g')} : {←ppExpr (← g'.getType)}"
+      let ppD (l : LocalDecl) : TacticM PUnit := do
+        logInfo s!"    {←ppExpr (.fvar l.fvarId)} : {←ppExpr l.type}"
+      let _ ← (←g'.getDecl).lctx.forM ppD
+      pure ()
+
+/-- warning: ?w : Nat is not independent of: -/
+#guard_msgs(warning) in
+example : ∃ (n : Nat), ∀(x : Fin n), x.val = 0 := by
+  apply Exists.intro
+  intro x
+  swap
+  check_indep
+  exact 0
+  revert x
+  intro ⟨x, lt⟩
+  contradiction
+
+-- This is a tricker one, where the dependency is via a hypothesis.
+/-- warning: ?w : Nat is not independent of: -/
+#guard_msgs(warning) in
+example : ∃ (n : Nat), ∀(x : Fin n) (y : Nat), x.val = y → y = 0 := by
+  apply Exists.intro
+  intro x y p
+  swap
+  check_indep
+  exact 0
+  revert x
+  intro ⟨x, lt⟩
+  contradiction