diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index d36d222..53a0d75 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.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.Basic
 import HepLean.AnomalyCancellation.PureU1.ConstAbs
 /-!
 # Line in plane condition
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index 2144568..711dbe6 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/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.Tactic.Ring
 import HepLean.AnomalyCancellation.Basic
 /-!
 # Anomaly cancellation conditions for n family SM.
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/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/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
 /-!