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/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index e7ca6bb..f70a265 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -3,10 +3,8 @@ 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.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.VectorLike
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the even case
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index b29c946..ac9e7bd 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -3,13 +3,8 @@ 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.Basic
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
 import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import Mathlib.RepresentationTheory.Basic
-import Mathlib.Tactic.Polyrith
 /-!
 
 # Line In Cubic Even case
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
index 0331c98..5d1ba6a 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -3,14 +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.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
-import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
-import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import Mathlib.RepresentationTheory.Basic
-import Mathlib.Tactic.Polyrith
 /-!
 # Parameterization in even case
 
diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index 3f06057..53a0d75 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.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 HepLean.AnomalyCancellation.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.VectorLike
 import HepLean.AnomalyCancellation.PureU1.ConstAbs
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 # Line in plane condition
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index 41c58bb..3d48445 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -3,10 +3,8 @@ 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.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.VectorLike
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the odd case
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index bba9360..e37adcc 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -3,14 +3,8 @@ 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.Basic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.VectorLike
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
 import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
 import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 
 # Line In Cubic Odd case
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
index ad719f8..cbc8db1 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -3,14 +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.PureU1.Basic
-import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.VectorLike
-import HepLean.AnomalyCancellation.PureU1.ConstAbs
-import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
 import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 # Parameterization in odd case
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index 8f97c65..440d62c 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -5,8 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Basic
 import HepLean.AnomalyCancellation.GroupActions
-import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of Pure U(1) ACC
 
diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
index d7d8170..37f1087 100644
--- a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
+++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.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.Sorts
-import Mathlib.Logic.Equiv.Fin
 /-!
 # Vector like charges
 
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index 07737f2..711dbe6 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/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
 /-!
 # Anomaly cancellation conditions for n family SM.
 
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
index c5dc03e..c682dc9 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.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.SM.Basic
-import HepLean.AnomalyCancellation.SM.NoGrav.Basic
 import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
-import Mathlib.NumberTheory.FLT.Three
 /-!
 # Lemmas for 1 family SM Accs
 
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 5b00d24..86594c4 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.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 HepLean.AnomalyCancellation.SM.Basic
 import HepLean.AnomalyCancellation.SM.NoGrav.Basic
-import Mathlib.Tactic.FieldSimp
-import Mathlib.Tactic.Linarith
-import Mathlib.NumberTheory.FLT.Basic
-import Mathlib.Algebra.QuadraticDiscriminant
 import Mathlib.NumberTheory.FLT.Three
 /-!
 # Parameterizations for solutions to the linear ACCs for 1 family
diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index 3b1c395..b49700c 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/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.SM.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.RepresentationTheory.Basic
 /-!
 
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index 447ccf6..8f7414c 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/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
 /-!
 # Anomaly cancellation conditions for n family SM.
 -/
diff --git a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
index c26ca78..04f4d0e 100644
--- a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/NoGrav/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 HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.GroupActions
 /-!
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
index b0fed2e..1341156 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/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 HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.GroupActions
 /-!
diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
index 1c5f29a..f961655 100644
--- a/HepLean/AnomalyCancellation/SMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SMNu/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.SMNu.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of SM charges with RHN.
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
index bb935fe..6327fb0 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.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.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 /-!
 # B Minus L in SM with RHN.
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
index f09e06f..7c79194 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/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 HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.GroupActions
 /-!
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index a95804e..ec3692d 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.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.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 /-!
 # Bound on plane dimension
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
index 9543aad..dfa91de 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.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.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 /-!
 # Hypercharge in SM with RHN.
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
index 967d2a6..8787d9c 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.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.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
 /-!
 # Solutions from quad solutions
diff --git a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
index a1ce918..382c70b 100644
--- a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.Basic
-import HepLean.Meta.Informal.Basic
 /-!
 
 # The Georgi-Glashow Model
diff --git a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
index 41558a5..8ee2bb3 100644
--- a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.Basic
-import HepLean.Meta.Informal.Basic
 /-!
 
 # The Pati-Salam Model
diff --git a/HepLean/BeyondTheStandardModel/Spin10/Basic.lean b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
index 62c20d7..a57d7c9 100644
--- a/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
 import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
-import HepLean.Meta.Informal.Basic
 /-!
 
 # The Spin(10) Model
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
index f27d805..63c4453 100644
--- a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
@@ -7,7 +7,6 @@ import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.StandardModel.HiggsBoson.GaugeAction
 import Mathlib.LinearAlgebra.Matrix.PosDef
 import Mathlib.Analysis.CStarAlgebra.Matrix
-import Mathlib.Analysis.Matrix
 /-!
 
 # Gauge orbits for the 2HDM
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 49c581e..b254b56 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.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.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Rows
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
 # Relations for the CKM Matrix
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index 1efdb33..034bff6 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -3,10 +3,8 @@ 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.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
 # Standard parameterization for the CKM Matrix
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
index de0a34c..5bf79a2 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -3,12 +3,8 @@ 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.FlavorPhysics.CKMMatrix.Basic
-import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
-import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
 # Standard parameters for the CKM Matrix
 
diff --git a/HepLean/Lorentz/Algebra/Basic.lean b/HepLean/Lorentz/Algebra/Basic.lean
index b0622c4..9eeb235 100644
--- a/HepLean/Lorentz/Algebra/Basic.lean
+++ b/HepLean/Lorentz/Algebra/Basic.lean
@@ -3,8 +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.MinkowskiMatrix
-import Mathlib.Algebra.Lie.Classical
 import HepLean.Lorentz.RealVector.Basic
 /-!
 # The Lorentz Algebra
diff --git a/HepLean/Lorentz/ComplexTensor/Basic.lean b/HepLean/Lorentz/ComplexTensor/Basic.lean
index 50b28e9..52695a5 100644
--- a/HepLean/Lorentz/ComplexTensor/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Basic.lean
@@ -3,15 +3,9 @@ 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.Tree.Dot
-import HepLean.Lorentz.Weyl.Contraction
 import HepLean.Lorentz.Weyl.Metric
-import HepLean.Lorentz.Weyl.Unit
-import HepLean.Lorentz.ComplexVector.Contraction
 import HepLean.Lorentz.ComplexVector.Metric
-import HepLean.Lorentz.ComplexVector.Unit
-import HepLean.Mathematics.PiTensorProduct
 import HepLean.Lorentz.PauliMatrices.AsTensor
 /-!
 
diff --git a/HepLean/Lorentz/ComplexTensor/Basis.lean b/HepLean/Lorentz/ComplexTensor/Basis.lean
index 05a02ed..a0344c0 100644
--- a/HepLean/Lorentz/ComplexTensor/Basis.lean
+++ b/HepLean/Lorentz/ComplexTensor/Basis.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.Tensors.Tree.Elab
-import HepLean.Lorentz.ComplexTensor.Basic
-import Mathlib.LinearAlgebra.TensorProduct.Basis
-import HepLean.Tensors.Tree.NodeIdentities.Basic
 import HepLean.Tensors.Tree.NodeIdentities.PermProd
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
 import HepLean.Tensors.Tree.NodeIdentities.ProdComm
diff --git a/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean b/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean
index c97a812..af0cde5 100644
--- a/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean
@@ -4,14 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basic
-import HepLean.Tensors.Tree.NodeIdentities.ProdContr
-import HepLean.Tensors.Tree.NodeIdentities.PermContr
-import HepLean.Tensors.Tree.NodeIdentities.PermProd
-import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
-import HepLean.Tensors.Tree.NodeIdentities.ContrContr
-import HepLean.Tensors.Tree.NodeIdentities.ProdComm
-import HepLean.Tensors.Tree.NodeIdentities.Congr
-import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
 /-!
 
 ## Bispinors
diff --git a/HepLean/Lorentz/ComplexTensor/Lemmas.lean b/HepLean/Lorentz/ComplexTensor/Lemmas.lean
index 94e847a..bea8f29 100644
--- a/HepLean/Lorentz/ComplexTensor/Lemmas.lean
+++ b/HepLean/Lorentz/ComplexTensor/Lemmas.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexTensor.Basis
-import HepLean.Tensors.Tree.NodeIdentities.PermProd
 /-!
 
 ## Lemmas related to complex Lorentz tensors.
diff --git a/HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean b/HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean
index d6d66d9..6d890c1 100644
--- a/HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean
@@ -9,7 +9,6 @@ import HepLean.Tensors.Tree.NodeIdentities.ProdContr
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
 import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
-import HepLean.Tensors.Tree.NodeIdentities.Congr
 /-!
 
 ## Metrics as complex Lorentz tensors
diff --git a/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean b/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean
index c36a89a..dea01b0 100644
--- a/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean
+++ b/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexTensor.Metrics.Basis
 import HepLean.Lorentz.ComplexTensor.Units.Basic
-import HepLean.Lorentz.ComplexTensor.Basis
 /-!
 
 ## Basic lemmas regarding metrics
diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
index 93992e8..b9b95f5 100644
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
@@ -3,13 +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.NodeIdentities.ProdAssoc
-import HepLean.Tensors.Tree.NodeIdentities.ProdComm
-import HepLean.Tensors.Tree.NodeIdentities.ProdContr
-import HepLean.Tensors.Tree.NodeIdentities.ContrContr
-import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
-import HepLean.Tensors.Tree.NodeIdentities.PermContr
-import HepLean.Tensors.Tree.NodeIdentities.Congr
 import HepLean.Lorentz.ComplexTensor.Metrics.Lemmas
 /-!
 
diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
index 7f77907..cd2c2f6 100644
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basic
-import HepLean.Lorentz.ComplexTensor.Basis
 /-!
 
 ## Pauli matrices and the basis of complex Lorentz tensors
diff --git a/HepLean/Lorentz/ComplexTensor/Units/Basic.lean b/HepLean/Lorentz/ComplexTensor/Units/Basic.lean
index 8ec6da9..9d687c0 100644
--- a/HepLean/Lorentz/ComplexTensor/Units/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Units/Basic.lean
@@ -9,7 +9,6 @@ import HepLean.Tensors.Tree.NodeIdentities.ProdContr
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
 import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
-import HepLean.Tensors.Tree.NodeIdentities.Congr
 /-!
 
 ## Metrics as complex Lorentz tensors
diff --git a/HepLean/Lorentz/ComplexTensor/Units/Symm.lean b/HepLean/Lorentz/ComplexTensor/Units/Symm.lean
index acc6d0c..541a097 100644
--- a/HepLean/Lorentz/ComplexTensor/Units/Symm.lean
+++ b/HepLean/Lorentz/ComplexTensor/Units/Symm.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexTensor.Metrics.Basis
 import HepLean.Lorentz.ComplexTensor.Units.Basic
-import HepLean.Lorentz.ComplexTensor.Basis
 /-!
 
 ## Symmetry lemmas relating to units
diff --git a/HepLean/Lorentz/ComplexVector/Basic.lean b/HepLean/Lorentz/ComplexVector/Basic.lean
index 2b4c7a5..f234191 100644
--- a/HepLean/Lorentz/ComplexVector/Basic.lean
+++ b/HepLean/Lorentz/ComplexVector/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.Data.Complex.Exponential
-import Mathlib.Analysis.InnerProductSpace.PiL2
-import HepLean.Lorentz.SL2C.Basic
 import HepLean.Lorentz.ComplexVector.Modules
-import HepLean.Meta.Informal.Basic
-import Mathlib.RepresentationTheory.Rep
-import HepLean.Lorentz.PauliMatrices.SelfAdjoint
 /-!
 
 # Complex Lorentz vectors
diff --git a/HepLean/Lorentz/ComplexVector/Metric.lean b/HepLean/Lorentz/ComplexVector/Metric.lean
index d407147..062e206 100644
--- a/HepLean/Lorentz/ComplexVector/Metric.lean
+++ b/HepLean/Lorentz/ComplexVector/Metric.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.ComplexVector.Two
-import HepLean.Lorentz.MinkowskiMatrix
-import HepLean.Lorentz.ComplexVector.Contraction
 import HepLean.Lorentz.ComplexVector.Unit
 /-!
 
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/SL2C/Basic.lean b/HepLean/Lorentz/SL2C/Basic.lean
index 66e5daa..17270c9 100644
--- a/HepLean/Lorentz/SL2C/Basic.lean
+++ b/HepLean/Lorentz/SL2C/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 HepLean.Lorentz.Group.Basic
-import HepLean.Lorentz.RealVector.Basic
-import Mathlib.RepresentationTheory.Basic
 import HepLean.Lorentz.Group.Restricted
-import HepLean.Lorentz.PauliMatrices.SelfAdjoint
-import HepLean.Meta.Informal.Basic
 /-!
 # The group SL(2, ℂ) and it's relation to the Lorentz group
 
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/Two.lean b/HepLean/Lorentz/Weyl/Two.lean
index b6ee63e..fdbf7c1 100644
--- a/HepLean/Lorentz/Weyl/Two.lean
+++ b/HepLean/Lorentz/Weyl/Two.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.Lorentz.Weyl.Basic
 import HepLean.Lorentz.Weyl.Contraction
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
 /-!
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/HTMLNote.lean b/HepLean/Meta/Notes/HTMLNote.lean
index 31de871..205970a 100644
--- a/HepLean/Meta/Notes/HTMLNote.lean
+++ b/HepLean/Meta/Notes/HTMLNote.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Notes.NoteFile
-import HepLean.Meta.Basic
 import HepLean.Meta.Informal.Post
 /-!
 
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/KoszulOrder.lean b/HepLean/PerturbationTheory/Wick/KoszulOrder.lean
index 85a5a06..f22a9fa 100644
--- a/HepLean/PerturbationTheory/Wick/KoszulOrder.lean
+++ b/HepLean/PerturbationTheory/Wick/KoszulOrder.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.StaticWickCoef
 /-!
 
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