diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
index c2fd079..ec23b72 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Particles.StandardModel.HiggsBoson.Potential
-import PhysLean.Meta.TODO.Basic
 /-!
 
 # The Two Higgs Doublet Model
diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
index 4b1bd45..4129d64 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
 import PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction
-import Mathlib.LinearAlgebra.Matrix.PosDef
 import Mathlib.Analysis.CStarAlgebra.Matrix
 /-!
 
diff --git a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean
index c53fbf2..c3474bc 100644
--- a/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.LinearAlgebra.UnitaryGroup
-import Mathlib.Data.Complex.Exponential
 import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Tactic.Polyrith
 /-!
diff --git a/PhysLean/Relativity/Lorentz/ComplexTensor/Metrics/Basic.lean b/PhysLean/Relativity/Lorentz/ComplexTensor/Metrics/Basic.lean
index 711ec28..306630e 100644
--- a/PhysLean/Relativity/Lorentz/ComplexTensor/Metrics/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/ComplexTensor/Metrics/Basic.lean
@@ -6,9 +6,9 @@ Authors: Joseph Tooby-Smith
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.ProdAssoc
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.ProdComm
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.ProdContr
-import PhysLean.Relativity.Tensors.Tree.NodeIdentities.ContrContr
-import PhysLean.Relativity.Tensors.Tree.NodeIdentities.ContrSwap
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.PermContr
+import PhysLean.Relativity.Lorentz.ComplexTensor.Basic
+import PhysLean.Relativity.Tensors.Tree.NodeIdentities.Basic
 /-!
 
 ## Metrics as complex Lorentz tensors
diff --git a/PhysLean/Relativity/Lorentz/ComplexVector/Basic.lean b/PhysLean/Relativity/Lorentz/ComplexVector/Basic.lean
index 37ff9ce..f39a0cd 100644
--- a/PhysLean/Relativity/Lorentz/ComplexVector/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/ComplexVector/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.Lorentz.ComplexVector.Modules
-import PhysLean.Meta.TODO.Basic
 /-!
 
 # Complex Lorentz vectors
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Basic.lean b/PhysLean/Relativity/Lorentz/RealTensor/Basic.lean
index 5ef8da6..3ee9479 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Basic.lean
@@ -3,11 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.Relativity.Tensors.Tree.Dot
-import PhysLean.Relativity.Lorentz.Weyl.Metric
 import PhysLean.Relativity.Lorentz.RealTensor.Metrics.Pre
-import PhysLean.Relativity.Lorentz.RealTensor.Vector.Pre.Basic
-import PhysLean.Relativity.Lorentz.PauliMatrices.AsTensor
 import PhysLean.Relativity.Lorentz.ComplexTensor.Basic
 /-!
 
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean b/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean
index f19f526..93b1dd9 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean
@@ -3,11 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.Relativity.Tensors.Tree.Dot
-import PhysLean.Relativity.Lorentz.Weyl.Metric
 import PhysLean.Relativity.Lorentz.RealTensor.Basic
-import PhysLean.Relativity.Lorentz.RealTensor.Vector.Pre.Basic
-import PhysLean.Relativity.Lorentz.PauliMatrices.AsTensor
 /-!
 
 ## Derivative of Real Lorentz tensors
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Basic.lean b/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Basic.lean
index 2483c2a..dbadc1e 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Basic.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.PermContr
 import PhysLean.Relativity.Lorentz.RealTensor.Basic
-import PhysLean.Relativity.Tensors.Tree.NodeIdentities.Basic
 /-!
 
 ## Metrics as real Lorentz tensors
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Pre.lean b/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Pre.lean
index fac3c60..80a7849 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Pre.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Metrics/Pre.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.Lorentz.RealTensor.Units.Pre
-import PhysLean.Relativity.Lorentz.RealTensor.Matrix.Pre
 /-!
 
 # Metric for real Lorentz vectors
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean b/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean
index 63eeb80..e134a51 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean
@@ -5,7 +5,6 @@ Authors: Matteo Cipollina, Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.Lorentz.RealTensor.Metrics.Basic
 import Mathlib.Geometry.Manifold.IsManifold.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
 /-!
 
 ## Metrics as real Lorentz tensors
diff --git a/PhysLean/Relativity/SpaceTime/Basic.lean b/PhysLean/Relativity/SpaceTime/Basic.lean
index ff7f5a4..ec50c48 100644
--- a/PhysLean/Relativity/SpaceTime/Basic.lean
+++ b/PhysLean/Relativity/SpaceTime/Basic.lean
@@ -3,9 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import Mathlib.Geometry.Manifold.IsManifold.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
-import PhysLean.Meta.TODO.Basic
 import PhysLean.Relativity.Lorentz.RealTensor.Vector.Basic
 /-!
 # Space time
diff --git a/PhysLean/Relativity/Special/TwinParadox/Basic.lean b/PhysLean/Relativity/Special/TwinParadox/Basic.lean
index 8927f46..e6c2042 100644
--- a/PhysLean/Relativity/Special/TwinParadox/Basic.lean
+++ b/PhysLean/Relativity/Special/TwinParadox/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.SpaceTime.ProperTime
-import PhysLean.Relativity.Lorentz.RealTensor.Vector.Causality
 /-!
 # Twin Paradox
 
diff --git a/PhysLean/Relativity/Tensors/TensorSpecies/Basis.lean b/PhysLean/Relativity/Tensors/TensorSpecies/Basis.lean
index bdc561c..d6b7299 100644
--- a/PhysLean/Relativity/Tensors/TensorSpecies/Basis.lean
+++ b/PhysLean/Relativity/Tensors/TensorSpecies/Basis.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.Relativity.Tensors.TensorSpecies.Basic
 import PhysLean.Relativity.Tensors.TensorSpecies.Contractions.ContrMap
 /-!
 
diff --git a/PhysLean/Relativity/Tensors/Tree/Basic.lean b/PhysLean/Relativity/Tensors/Tree/Basic.lean
index f161eca..14d0e37 100644
--- a/PhysLean/Relativity/Tensors/Tree/Basic.lean
+++ b/PhysLean/Relativity/Tensors/Tree/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.Relativity.Tensors.TensorSpecies.Contractions.ContrMap
 import PhysLean.Relativity.Tensors.TensorSpecies.Basis
 /-!
 
diff --git a/scripts/MetaPrograms/redundent_imports.lean b/scripts/MetaPrograms/redundent_imports.lean
index 09d4be8..b448772 100644
--- a/scripts/MetaPrograms/redundent_imports.lean
+++ b/scripts/MetaPrograms/redundent_imports.lean
@@ -5,6 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Meta.Basic
 import ImportGraph.Imports
+import Mathlib.Lean.CoreM
+
 /-!
 
 # Extracting commands with no doc strings.
@@ -18,7 +20,7 @@ def Imports.RedundentImports (imp : Import) : MetaM UInt32 := do
   let x ← redundantImports (some imp.module)
   if x.isEmpty then return 0
   println! "\n"
-  println! (← Name.toFile imp.module)
+  println! (Name.toFilePath imp.module)
   println! x.toList
   return 0