diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 5c79621..8226299 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Mathematics.LinearMaps
-import Mathlib.Algebra.Module.Basic
 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
 /-!
 # Basic set up for anomaly cancellation conditions
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index cdf54eb..f436a92 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -3,13 +3,7 @@ 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.Tactic.FinCases
-import Mathlib.Algebra.Module.Basic
-import Mathlib.Tactic.Ring
-import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import HepLean.AnomalyCancellation.Basic
-import Mathlib.Algebra.BigOperators.Fin
-import Mathlib.Logic.Equiv.Fin
 /-!
 # The MSSM with 3 families and RHNs
 
diff --git a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
index f12b507..0ee01f7 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.MSSMNu.Basic
-import Mathlib.Tactic.Polyrith
 /-!
 # Hypercharge in MSSM.
 
diff --git a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
index a67db47..a6b2f7e 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.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 HepLean.AnomalyCancellation.MSSMNu.Basic
 import HepLean.AnomalyCancellation.MSSMNu.Y3
 import HepLean.AnomalyCancellation.MSSMNu.B3
 /-!
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
index 8fc46d2..df04959 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
@@ -3,10 +3,7 @@ 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 HepLean.AnomalyCancellation.MSSMNu.Basic
 import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
-import Mathlib.Tactic.Polyrith
-import Mathlib.Tactic.Linarith
 /-!
 # The type of solutions perpendicular to `Y₃` and `B₃`
 
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
index a0715f6..e0babda 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@@ -3,10 +3,7 @@ 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 HepLean.AnomalyCancellation.MSSMNu.Basic
-import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
 import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.Basic
-import Mathlib.Tactic.Polyrith
 /-!
 # Plane Y₃ B₃ and an orthogonal third point
 
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 7dc2050..7b6987e 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -3,10 +3,7 @@ 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 HepLean.AnomalyCancellation.MSSMNu.Basic
-import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
 import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3.PlaneWithY3B3
-import Mathlib.Tactic.Polyrith
 /-!
 # From charges perpendicular to `Y₃` and `B₃` to solutions
 
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
index 078c3bd..357f4a4 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.MSSMNu.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of MSSM charges and solutions
diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index 79c80b1..d506c0a 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -4,9 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.Basic
-import Mathlib.Algebra.Module.Equiv.Basic
-import Mathlib.Algebra.BigOperators.Ring
-import Mathlib.Algebra.BigOperators.Fin
 /-!
 # Pure U(1) ACC system.
 
diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
index 34fef89..9f7a837 100644
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 /-!
 # Basis of `LinSols`
diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
index 8c1526a..e05ec0c 100644
--- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
+++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.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 HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.VectorLike
 /-!
 # Charges assignments with constant abs
diff --git a/HepLean/Lorentz/ComplexVector/Modules.lean b/HepLean/Lorentz/ComplexVector/Modules.lean
index 674f6ff..29df679 100644
--- a/HepLean/Lorentz/ComplexVector/Modules.lean
+++ b/HepLean/Lorentz/ComplexVector/Modules.lean
@@ -3,10 +3,7 @@ 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 HepLean.Meta.Informal.Basic
 import HepLean.Lorentz.SL2C.Basic
-import Mathlib.RepresentationTheory.Rep
-import Mathlib.Logic.Equiv.TransferInstance
 /-!
 
 ## Modules associated with complex Lorentz vectors
diff --git a/HepLean/Lorentz/Group/Boosts.lean b/HepLean/Lorentz/Group/Boosts.lean
index 6e6df8f..9c44246 100644
--- a/HepLean/Lorentz/Group/Boosts.lean
+++ b/HepLean/Lorentz/Group/Boosts.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.Group.Proper
-import Mathlib.Topology.Constructions
 import HepLean.Lorentz.RealVector.NormOne
 /-!
 # Boosts
diff --git a/HepLean/Lorentz/Group/Restricted.lean b/HepLean/Lorentz/Group/Restricted.lean
index e40d066..3812cd1 100644
--- a/HepLean/Lorentz/Group/Restricted.lean
+++ b/HepLean/Lorentz/Group/Restricted.lean
@@ -3,10 +3,7 @@ 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 HepLean.Lorentz.Group.Basic
-import HepLean.Lorentz.Group.Proper
 import HepLean.Lorentz.Group.Orthochronous
-import HepLean.Meta.Informal.Basic
 /-!
 # The Restricted Lorentz Group
 
diff --git a/HepLean/Lorentz/Group/Rotations.lean b/HepLean/Lorentz/Group/Rotations.lean
index 37e748f..eb063cd 100644
--- a/HepLean/Lorentz/Group/Rotations.lean
+++ b/HepLean/Lorentz/Group/Rotations.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.Group.Basic
 import HepLean.Mathematics.SO3.Basic
-import Mathlib.Topology.Constructions
 /-!
 # Rotations
 
diff --git a/HepLean/Lorentz/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean
index b5d91bd..248e9b1 100644
--- a/HepLean/Lorentz/MinkowskiMatrix.lean
+++ b/HepLean/Lorentz/MinkowskiMatrix.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 Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Algebra.Lie.Classical
 /-!
diff --git a/HepLean/Lorentz/PauliMatrices/AsTensor.lean b/HepLean/Lorentz/PauliMatrices/AsTensor.lean
index 5aeb9df..21196da 100644
--- a/HepLean/Lorentz/PauliMatrices/AsTensor.lean
+++ b/HepLean/Lorentz/PauliMatrices/AsTensor.lean
@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Basic
-import HepLean.Mathematics.PiTensorProduct
-import HepLean.Lorentz.ComplexVector.Basic
 import HepLean.Lorentz.Weyl.Two
-import HepLean.Lorentz.PauliMatrices.Basic
 /-!
 
 ## Pauli matrices
diff --git a/HepLean/Lorentz/PauliMatrices/Basic.lean b/HepLean/Lorentz/PauliMatrices/Basic.lean
index c5928c8..e753882 100644
--- a/HepLean/Lorentz/PauliMatrices/Basic.lean
+++ b/HepLean/Lorentz/PauliMatrices/Basic.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Mathematics.PiTensorProduct
 import Mathlib.RepresentationTheory.Rep
-import Mathlib.Logic.Equiv.TransferInstance
 import HepLean.Lorentz.Group.Basic
 /-!
 
diff --git a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
index 88d6f56..3d47a1d 100644
--- a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
+++ b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
@@ -3,10 +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 HepLean.Mathematics.PiTensorProduct
-import Mathlib.RepresentationTheory.Rep
-import Mathlib.Logic.Equiv.TransferInstance
-import HepLean.Lorentz.Group.Basic
 import HepLean.Lorentz.PauliMatrices.Basic
 /-!
 
diff --git a/HepLean/Lorentz/RealVector/Basic.lean b/HepLean/Lorentz/RealVector/Basic.lean
index d95806e..efa7552 100644
--- a/HepLean/Lorentz/RealVector/Basic.lean
+++ b/HepLean/Lorentz/RealVector/Basic.lean
@@ -3,11 +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.Data.Complex.Exponential
-import Mathlib.Analysis.InnerProductSpace.PiL2
-import HepLean.Lorentz.Group.Basic
-import HepLean.Meta.Informal.Basic
-import Mathlib.RepresentationTheory.Rep
 import HepLean.Lorentz.RealVector.Modules
 /-!
 
diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean
index 70318d5..2652df7 100644
--- a/HepLean/Lorentz/RealVector/Modules.lean
+++ b/HepLean/Lorentz/RealVector/Modules.lean
@@ -4,9 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Informal.Basic
-import HepLean.Lorentz.Group.Basic
-import Mathlib.RepresentationTheory.Rep
-import Mathlib.Logic.Equiv.TransferInstance
 import HepLean.Lorentz.PauliMatrices.SelfAdjoint
 /-!
 
diff --git a/HepLean/Lorentz/Weyl/Basic.lean b/HepLean/Lorentz/Weyl/Basic.lean
index 7faf7be..25c7f79 100644
--- a/HepLean/Lorentz/Weyl/Basic.lean
+++ b/HepLean/Lorentz/Weyl/Basic.lean
@@ -3,11 +3,7 @@ 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 HepLean.Meta.Informal.Basic
-import HepLean.Lorentz.SL2C.Basic
-import Mathlib.RepresentationTheory.Rep
 import HepLean.Lorentz.Weyl.Modules
-import Mathlib.Logic.Equiv.TransferInstance
 /-!
 
 # Weyl fermions
diff --git a/HepLean/Lorentz/Weyl/Metric.lean b/HepLean/Lorentz/Weyl/Metric.lean
index 7bf9cee..3373dae 100644
--- a/HepLean/Lorentz/Weyl/Metric.lean
+++ b/HepLean/Lorentz/Weyl/Metric.lean
@@ -3,10 +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 HepLean.Lorentz.Weyl.Basic
-import HepLean.Lorentz.Weyl.Contraction
-import Mathlib.LinearAlgebra.TensorProduct.Matrix
-import HepLean.Lorentz.Weyl.Two
 import HepLean.Lorentz.Weyl.Unit
 /-!
 
diff --git a/HepLean/Lorentz/Weyl/Modules.lean b/HepLean/Lorentz/Weyl/Modules.lean
index 3cfa301..9076ab9 100644
--- a/HepLean/Lorentz/Weyl/Modules.lean
+++ b/HepLean/Lorentz/Weyl/Modules.lean
@@ -3,10 +3,7 @@ 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 HepLean.Meta.Informal.Basic
 import HepLean.Lorentz.SL2C.Basic
-import Mathlib.RepresentationTheory.Rep
-import Mathlib.Logic.Equiv.TransferInstance
 /-!
 
 ## Modules associated with Fermions
diff --git a/HepLean/Lorentz/Weyl/Unit.lean b/HepLean/Lorentz/Weyl/Unit.lean
index 20e5fcf..189ee00 100644
--- a/HepLean/Lorentz/Weyl/Unit.lean
+++ b/HepLean/Lorentz/Weyl/Unit.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 HepLean.Lorentz.Weyl.Basic
-import HepLean.Lorentz.Weyl.Contraction
-import Mathlib.LinearAlgebra.TensorProduct.Matrix
 import HepLean.Lorentz.Weyl.Two
 /-!
 
diff --git a/HepLean/Mathematics/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean
index c879aff..14eba5e 100644
--- a/HepLean/Mathematics/SO3/Basic.lean
+++ b/HepLean/Mathematics/SO3/Basic.lean
@@ -3,9 +3,7 @@ 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.LinearAlgebra.UnitaryGroup
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
-import Mathlib.Data.Complex.Exponential
 import Mathlib.LinearAlgebra.Eigenspace.Basic
 import Mathlib.Analysis.InnerProductSpace.PiL2
 /-!
diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean
index bb09613..414e58e 100644
--- a/HepLean/Meta/Basic.lean
+++ b/HepLean/Meta/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Batteries.Lean.HashSet
-import Lean
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.CoreM
 import ImportGraph.RequiredModules
diff --git a/HepLean/Meta/Informal/Post.lean b/HepLean/Meta/Informal/Post.lean
index b0d9c60..80103e8 100644
--- a/HepLean/Meta/Informal/Post.lean
+++ b/HepLean/Meta/Informal/Post.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Meta.Informal.Basic
 import HepLean.Meta.Basic
 /-!
 
diff --git a/HepLean/Meta/Notes/Basic.lean b/HepLean/Meta/Notes/Basic.lean
index 7fcb7d2..1065129 100644
--- a/HepLean/Meta/Notes/Basic.lean
+++ b/HepLean/Meta/Notes/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Batteries.Lean.HashSet
-import Lean
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.CoreM
 import ImportGraph.RequiredModules
diff --git a/HepLean/Meta/Notes/ToHTML.lean b/HepLean/Meta/Notes/ToHTML.lean
index 55c9c1e..deb37ab 100644
--- a/HepLean/Meta/Notes/ToHTML.lean
+++ b/HepLean/Meta/Notes/ToHTML.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Notes.HTMLNote
-import HepLean.Meta.Basic
 /-!
 
 ## Turns a delaration into a html note structure.
diff --git a/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean b/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean
index e328513..50893fd 100644
--- a/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean
+++ b/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean
@@ -3,19 +3,11 @@ 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.Logic.Equiv.Fin
 import Mathlib.Tactic.FinCases
-import Mathlib.Data.Finset.Card
-import Mathlib.CategoryTheory.IsomorphismClasses
-import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Comma.Over
-import Mathlib.Data.Fintype.Pi
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
-import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Perm
-import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
-import Mathlib.SetTheory.Cardinal.Basic
 /-!
 # Feynman diagrams
 
diff --git a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
index 42e2bd4..47eccdc 100644
--- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.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.Algebra.FreeAlgebra
-import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.Analysis.Complex.Basic
 import HepLean.PerturbationTheory.Wick.Signs.KoszulSignInsert
 /-!
 
diff --git a/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean b/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean
index cbac792..62ddc24 100644
--- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.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.Algebra.FreeAlgebra
-import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.Analysis.Complex.Basic
 import HepLean.PerturbationTheory.Wick.Signs.InsertSign
 /-!
 
diff --git a/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean b/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean
index 580c5ae..6288fbd 100644
--- a/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.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.Algebra.FreeAlgebra
-import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.Analysis.Complex.Basic
 import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
 /-!
 
diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index 2b615c8..8f950e7 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/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 Mathlib.Data.Complex.Exponential
 import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
 import Mathlib.Analysis.InnerProductSpace.PiL2
 /-!
diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean
index 5530a90..295f198 100644
--- a/HepLean/StandardModel/Basic.lean
+++ b/HepLean/StandardModel/Basic.lean
@@ -3,9 +3,7 @@ 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.Data.Complex.Exponential
 import Mathlib.Geometry.Manifold.Instances.Real
-import Mathlib.LinearAlgebra.Matrix.ToLin
 import HepLean.SpaceTime.Basic
 import HepLean.Meta.Informal.Basic
 /-!
diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index 5e20e2b..5cfb6f9 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -4,13 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Basic
-import Mathlib.Data.Complex.Exponential
 import Mathlib.Tactic.Polyrith
-import Mathlib.Geometry.Manifold.VectorBundle.Basic
 import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Geometry.Manifold.ContMDiff.Product
 import HepLean.Meta.Informal.Basic
 /-!
 
diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean
index 5b5b9b7..091d9ab 100644
--- a/HepLean/StandardModel/HiggsBoson/Potential.lean
+++ b/HepLean/StandardModel/HiggsBoson/Potential.lean
@@ -3,9 +3,7 @@ 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.Algebra.QuadraticDiscriminant
 import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
-import HepLean.Meta.Informal.Basic
 /-!
 # The potential of the Higgs field
 
diff --git a/HepLean/StandardModel/Representations.lean b/HepLean/StandardModel/Representations.lean
index be53819..fe4682f 100644
--- a/HepLean/StandardModel/Representations.lean
+++ b/HepLean/StandardModel/Representations.lean
@@ -3,9 +3,7 @@ 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.Data.Complex.Exponential
 import Mathlib.Geometry.Manifold.Instances.Real
-import Mathlib.LinearAlgebra.Matrix.ToLin
 /-!
 # Representations appearing in the Standard Model
 
diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean
index 1a66de7..b32fcef 100644
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@@ -3,12 +3,7 @@ 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.CategoryTheory.Category.Basic
-import Mathlib.CategoryTheory.Types
-import Mathlib.CategoryTheory.Monoidal.Category
-import Mathlib.CategoryTheory.Comma.Over
 import Mathlib.CategoryTheory.Core
-import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import HepLean.Lorentz.Weyl.Basic
 import HepLean.Lorentz.ComplexVector.Basic
 /-!
diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean
index f47620b..b7863b8 100644
--- a/HepLean/Tensors/OverColor/Discrete.lean
+++ b/HepLean/Tensors/OverColor/Discrete.lean
@@ -3,10 +3,7 @@ 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 HepLean.Tensors.OverColor.Basic
 import HepLean.Tensors.OverColor.Lift
-import HepLean.Mathematics.PiTensorProduct
-import HepLean.Tensors.OverColor.Iso
 /-!
 
 # Discrete color category
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index e9765a4..dd3fc41 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -3,9 +3,7 @@ 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 HepLean.Tensors.OverColor.Basic
 import HepLean.Tensors.OverColor.Iso
-import HepLean.Mathematics.PiTensorProduct
 /-!
 
 ## Lifting functors.
diff --git a/HepLean/Tensors/TensorSpecies/Basic.lean b/HepLean/Tensors/TensorSpecies/Basic.lean
index 29dd8b5..c4bfbaa 100644
--- a/HepLean/Tensors/TensorSpecies/Basic.lean
+++ b/HepLean/Tensors/TensorSpecies/Basic.lean
@@ -3,10 +3,7 @@ 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 HepLean.Tensors.OverColor.Iso
 import HepLean.Tensors.OverColor.Discrete
-import HepLean.Tensors.OverColor.Lift
-import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
 /-!
 
 # Tensor species
diff --git a/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean b/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean
index 84b0bd5..cc06d67 100644
--- a/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean
+++ b/HepLean/Tensors/TensorSpecies/Contractions/Categorical.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 HepLean.Tensors.Tree.Elab
 import HepLean.Tensors.Tree.NodeIdentities.Basic
 import HepLean.Tensors.Tree.NodeIdentities.Congr
 /-!
diff --git a/HepLean/Tensors/TensorSpecies/DualRepIso.lean b/HepLean/Tensors/TensorSpecies/DualRepIso.lean
index 0cc556c..194ab95 100644
--- a/HepLean/Tensors/TensorSpecies/DualRepIso.lean
+++ b/HepLean/Tensors/TensorSpecies/DualRepIso.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 HepLean.Tensors.TensorSpecies.Basic
 import HepLean.Tensors.TensorSpecies.MetricTensor
 import HepLean.Tensors.Tree.NodeIdentities.Assoc
 /-!
diff --git a/HepLean/Tensors/TensorSpecies/MetricTensor.lean b/HepLean/Tensors/TensorSpecies/MetricTensor.lean
index de512cf..12adca0 100644
--- a/HepLean/Tensors/TensorSpecies/MetricTensor.lean
+++ b/HepLean/Tensors/TensorSpecies/MetricTensor.lean
@@ -4,11 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.TensorSpecies.UnitTensor
-import HepLean.Tensors.TensorSpecies.Contractions.Categorical
-import HepLean.Tensors.Tree.NodeIdentities.ProdComm
-import HepLean.Tensors.Tree.NodeIdentities.PermProd
-import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
-import HepLean.Tensors.Tree.NodeIdentities.PermContr
 /-!
 
 ## Metrics in tensor trees
diff --git a/HepLean/Tensors/TensorSpecies/UnitTensor.lean b/HepLean/Tensors/TensorSpecies/UnitTensor.lean
index a7c93f9..f2492cf 100644
--- a/HepLean/Tensors/TensorSpecies/UnitTensor.lean
+++ b/HepLean/Tensors/TensorSpecies/UnitTensor.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 HepLean.Tensors.Tree.Elab
-import HepLean.Tensors.Tree.NodeIdentities.Basic
-import HepLean.Tensors.Tree.NodeIdentities.Congr
 import HepLean.Tensors.Tree.NodeIdentities.ProdComm
 import HepLean.Tensors.Tree.NodeIdentities.PermProd
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
diff --git a/HepLean/Tensors/Tree/Dot.lean b/HepLean/Tensors/Tree/Dot.lean
index c05551e..d8c0097 100644
--- a/HepLean/Tensors/Tree/Dot.lean
+++ b/HepLean/Tensors/Tree/Dot.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.Tree.Basic
-import Lean.Elab.Term
 /-!
 
 ## Tensor trees to dot files
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index fa82d4f..733a0f9 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.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 HepLean.Tensors.Tree.Basic
-import Lean.Elab.Term
-import HepLean.Tensors.Tree.Dot
 import HepLean.Lorentz.ComplexTensor.Basic
 /-!
 
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean b/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
index 0b7147f..a722fd9 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Assoc.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 HepLean.Tensors.Tree.Elab
-import HepLean.Tensors.Tree.NodeIdentities.Basic
-import HepLean.Tensors.Tree.NodeIdentities.Congr
 import HepLean.Tensors.Tree.NodeIdentities.ProdComm
 import HepLean.Tensors.Tree.NodeIdentities.PermProd
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
index efb0911..c6e57b3 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.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 HepLean.Tensors.Tree.Basic
 import HepLean.Tensors.Tree.NodeIdentities.Congr
 import HepLean.Tensors.Tree.NodeIdentities.Basic
 /-!
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean
index 1ee3281..b8c4070 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.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 HepLean.Tensors.Tree.Basic
 import HepLean.Tensors.Tree.NodeIdentities.Basic
 /-!
 
diff --git a/lakefile.toml b/lakefile.toml
index f223dc7..f0efd5d 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -88,6 +88,12 @@ name = "informal"
 supportInterpreter = true
 srcDir = "scripts/MetaPrograms"
 
+[[lean_exe]]
+name = "redundent_imports"
+supportInterpreter = true
+srcDir = "scripts/MetaPrograms"
+
+
 # -- Optional inclusion of openAI_doc_check. Needs `llm` above.
 #[[lean_exe]]
 #name = "openAI_doc_check"
diff --git a/scripts/MetaPrograms/redundent_imports.lean b/scripts/MetaPrograms/redundent_imports.lean
new file mode 100644
index 0000000..0817f64
--- /dev/null
+++ b/scripts/MetaPrograms/redundent_imports.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Basic
+import ImportGraph.Imports
+/-!
+
+# Extracting commands with no doc strings.
+
+-/
+
+open Lean System Meta HepLean
+
+
+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! x.toList
+  return 0
+
+unsafe def main (_ : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  let imports ← allImports
+  let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.RedundentImports).run'
+  return 0