From fb4bb0bb88fed58c45396cadcfc779ae85b43d1f Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 25 Jun 2024 07:06:32 -0400
Subject: [PATCH] refactor: Shake

---
 HepLean/AnomalyCancellation/LinearMaps.lean                | 2 +-
 HepLean/AnomalyCancellation/MSSMNu/Permutations.lean       | 2 +-
 HepLean/AnomalyCancellation/PureU1/BasisLinear.lean        | 2 +-
 HepLean/AnomalyCancellation/PureU1/LowDim/One.lean         | 2 +-
 HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean       | 2 +-
 HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean         | 2 +-
 HepLean/AnomalyCancellation/PureU1/Permutations.lean       | 1 -
 HepLean/AnomalyCancellation/PureU1/Sort.lean               | 1 +
 HepLean/AnomalyCancellation/SM/Permutations.lean           | 2 +-
 HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean         | 1 +
 HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean       | 1 +
 HepLean/AnomalyCancellation/SMNu/Permutations.lean         | 2 +-
 HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean         | 1 +
 HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean | 1 -
 HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean  | 1 -
 HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean       | 1 -
 HepLean/FeynmanDiagrams/Instances/Phi4.lean                | 2 +-
 HepLean/FeynmanDiagrams/Momentum.lean                      | 5 +----
 HepLean/FlavorPhysics/CKMMatrix/Invariants.lean            | 4 +---
 .../CKMMatrix/StandardParameterization/Basic.lean          | 1 -
 HepLean/GroupTheory/SO3/Basic.lean                         | 4 +---
 HepLean/SpaceTime/AsSelfAdjointMatrix.lean                 | 2 --
 HepLean/SpaceTime/Basic.lean                               | 6 +++---
 HepLean/SpaceTime/CliffordAlgebra.lean                     | 2 +-
 HepLean/SpaceTime/LorentzAlgebra/Basic.lean                | 4 ----
 HepLean/SpaceTime/LorentzGroup/Basic.lean                  | 4 ----
 HepLean/SpaceTime/LorentzGroup/Boosts.lean                 | 3 +--
 HepLean/SpaceTime/LorentzGroup/Orthochronous.lean          | 1 -
 HepLean/SpaceTime/LorentzGroup/Proper.lean                 | 1 -
 HepLean/SpaceTime/LorentzGroup/Rotations.lean              | 4 +---
 HepLean/SpaceTime/Metric.lean                              | 5 +----
 HepLean/StandardModel/Basic.lean                           | 7 -------
 HepLean/StandardModel/HiggsBoson/Basic.lean                | 2 +-
 HepLean/StandardModel/HiggsBoson/TargetSpace.lean          | 3 +--
 HepLean/StandardModel/Representations.lean                 | 5 -----
 scripts/lint-all.sh                                        | 6 +++++-
 36 files changed, 30 insertions(+), 65 deletions(-)

diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
index a91da92..5fda3b0 100644
--- a/HepLean/AnomalyCancellation/LinearMaps.lean
+++ b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Tactic.Polyrith
 import Mathlib.Algebra.Module.LinearMap.Basic
-import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Data.Fintype.BigOperators
 /-!
 # Linear maps
 
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
index 6ec5b54..9bde049 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.MSSMNu.Basic
 import Mathlib.Tactic.Polyrith
-import HepLean.AnomalyCancellation.GroupActions
+import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of MSSM charges and solutions
 
diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
index 3383d31..2694d69 100644
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Basic
 import Mathlib.Tactic.Polyrith
-import Mathlib.RepresentationTheory.Basic
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 /-!
 # Basis of `LinSols`
 
diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/One.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/One.lean
index 4fccec6..fd91578 100644
--- a/HepLean/AnomalyCancellation/PureU1/LowDim/One.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LowDim/One.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.Basic
 /-!
 # The Pure U(1) case with 1 fermion
 
diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
index 9a9ef24..15552a3 100644
--- a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.Basic
 /-!
 # The Pure U(1) case with 3 fermion
 
diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
index bf92017..78cb609 100644
--- a/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.Basic
 /-!
 # The Pure U(1) case with 2 fermions
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index ff237b7..7571fa3 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -7,7 +7,6 @@ import HepLean.AnomalyCancellation.PureU1.Basic
 import HepLean.AnomalyCancellation.GroupActions
 import Mathlib.Tactic.Polyrith
 import Mathlib.RepresentationTheory.Basic
-import Mathlib.Data.Fin.Tuple.Sort
 /-!
 # Permutations of Pure U(1) ACC
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean
index 896ff4b..f348632 100644
--- a/HepLean/AnomalyCancellation/PureU1/Sort.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Permutations
+import Mathlib.Data.Fin.Tuple.Sort
 /-!
 # Sort for Pure U(1) charges
 
diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index 96dae43..53ce7f2 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SM.Basic
 import Mathlib.Tactic.Polyrith
-import HepLean.AnomalyCancellation.GroupActions
+import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of SM with no RHN.
 
diff --git a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
index 859ad28..caff775 100644
--- a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
+import HepLean.AnomalyCancellation.GroupActions
 /-!
 # ACC system for SM with RHN and no gravitational anomaly.
 
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
index 5de3e2d..63ce1cc 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
+import HepLean.AnomalyCancellation.GroupActions
 /-!
 # ACC system for SM with RHN (without hypercharge).
 
diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
index 9a42821..4cf274a 100644
--- a/HepLean/AnomalyCancellation/SMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.Basic
 import Mathlib.Tactic.Polyrith
-import HepLean.AnomalyCancellation.GroupActions
+import Mathlib.RepresentationTheory.Basic
 /-!
 # Permutations of SM charges with RHN.
 
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
index 933af3c..8ac6ece 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.Permutations
+import HepLean.AnomalyCancellation.GroupActions
 /-!
 # ACC system for SM with RHN
 
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index a116fa5..a0c2e64 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
-import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 /-!
 # Bound on plane dimension
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index 11baafc..0e5255f 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
-import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 /-!
 # Plane of non-solutions
 
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
index c49d76e..912464c 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
-import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 /-!
 # Properties of Quad Sols for SM with RHN
 
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 513abff..06413ec 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Momentum
+import HepLean.FeynmanDiagrams.Basic
 /-!
 # Feynman diagrams in Phi^4 theory
 
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index bf68321..65cb033 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -5,12 +5,9 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.FeynmanDiagrams.Basic
 import Mathlib.Data.Real.Basic
-import Mathlib.Algebra.Category.ModuleCat.Basic
-import Mathlib.LinearAlgebra.StdBasis
-import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.Data.Matrix.Rank
 import Mathlib.Algebra.DirectSum.Module
 import Mathlib.LinearAlgebra.SesquilinearForm
+import Mathlib.LinearAlgebra.Dimension.Finrank
 /-!
 # Momentum in Feynman diagrams
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
index d5001e7..79a7e70 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -4,9 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.FlavorPhysics.CKMMatrix.Basic
-import HepLean.FlavorPhysics.CKMMatrix.Rows
-import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+import Mathlib.Analysis.Complex.Basic
 /-!
 # Invariants of the CKM Matrix
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index b98ac01..42ab86b 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -5,7 +5,6 @@ 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 Mathlib.Analysis.SpecialFunctions.Complex.Arg
 /-!
diff --git a/HepLean/GroupTheory/SO3/Basic.lean b/HepLean/GroupTheory/SO3/Basic.lean
index f003d66..ff34705 100644
--- a/HepLean/GroupTheory/SO3/Basic.lean
+++ b/HepLean/GroupTheory/SO3/Basic.lean
@@ -6,10 +6,8 @@ Authors: Joseph Tooby-Smith
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
 import Mathlib.Data.Complex.Exponential
-import Mathlib.Geometry.Manifold.VectorBundle.Basic
 import Mathlib.LinearAlgebra.Eigenspace.Basic
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.PiL2
 /-!
 # The group SO(3)
 
diff --git a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
index a7673b8..2ab809c 100644
--- a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Metric
-import HepLean.SpaceTime.FourVelocity
-import Mathlib.GroupTheory.SpecificGroups.KleinFour
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 /-!
 # Spacetime as a self-adjoint matrix
diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index 48b6beb..46fc1d4 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/Basic.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Data.Complex.Exponential
-import Mathlib.Geometry.Manifold.VectorBundle.Basic
-import Mathlib.Analysis.InnerProductSpace.Adjoint
-
+import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.LinearAlgebra.Matrix.DotProduct
 /-!
 # Space time
 
diff --git a/HepLean/SpaceTime/CliffordAlgebra.lean b/HepLean/SpaceTime/CliffordAlgebra.lean
index 68b6114..99fec60 100644
--- a/HepLean/SpaceTime/CliffordAlgebra.lean
+++ b/HepLean/SpaceTime/CliffordAlgebra.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.Metric
+import Mathlib.Analysis.Complex.Basic
 /-!
 # The Clifford Algebra
 
diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
index 18bc2fe..a1acd4e 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
@@ -5,11 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.Metric
-import Mathlib.Analysis.InnerProductSpace.Adjoint
-import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.Algebra.Lie.Classical
-import Mathlib.Algebra.Lie.TensorProduct
-import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 # The Lorentz Algebra
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index cd76b6f..f4a7f9e 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -4,11 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Metric
-import HepLean.SpaceTime.FourVelocity
 import HepLean.SpaceTime.AsSelfAdjointMatrix
-import Mathlib.GroupTheory.SpecificGroups.KleinFour
-import Mathlib.Geometry.Manifold.Algebra.LieGroup
-import Mathlib.Analysis.Matrix
 /-!
 # The Lorentz Group
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index 78180be..3295687 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -3,10 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzGroup.Orthochronous
 import HepLean.SpaceTime.LorentzGroup.Proper
-import Mathlib.GroupTheory.SpecificGroups.KleinFour
 import Mathlib.Topology.Constructions
+import HepLean.SpaceTime.FourVelocity
 /-!
 # Boosts
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index 3dba914..8068a06 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.FourVelocity
 import HepLean.SpaceTime.LorentzGroup.Proper
-import Mathlib.GroupTheory.SpecificGroups.KleinFour
 /-!
 # The Orthochronous Lorentz Group
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean
index 670d5c5..85e8125 100644
--- a/HepLean/SpaceTime/LorentzGroup/Proper.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzGroup.Basic
-import Mathlib.GroupTheory.SpecificGroups.KleinFour
 /-!
 # The Proper Lorentz Group
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
index 4410f5e..60dbb2b 100644
--- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
@@ -3,10 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzGroup.Orthochronous
-import HepLean.SpaceTime.LorentzGroup.Proper
+import HepLean.SpaceTime.LorentzGroup.Basic
 import HepLean.GroupTheory.SO3.Basic
-import Mathlib.GroupTheory.SpecificGroups.KleinFour
 import Mathlib.Topology.Constructions
 /-!
 # Rotations
diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean
index 33ae0c7..7f5c13a 100644
--- a/HepLean/SpaceTime/Metric.lean
+++ b/HepLean/SpaceTime/Metric.lean
@@ -4,11 +4,8 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Basic
-import Mathlib.Analysis.InnerProductSpace.Adjoint
-import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.Algebra.Lie.Classical
-import Mathlib.Algebra.Lie.TensorProduct
-import Mathlib.Tactic.RewriteSearch
+import Mathlib.LinearAlgebra.QuadraticForm.Basic
 /-!
 # Spacetime Metric
 
diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean
index ba30fec..25acc73 100644
--- a/HepLean/StandardModel/Basic.lean
+++ b/HepLean/StandardModel/Basic.lean
@@ -3,16 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.Basic
 import Mathlib.Data.Complex.Exponential
-import Mathlib.Geometry.Manifold.VectorBundle.Basic
-import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
-import Mathlib.RepresentationTheory.Basic
 import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.Analysis.InnerProductSpace.Adjoint
-import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
-import Mathlib.Analysis.NormedSpace.MatrixExponential
 /-!
 # The Standard Model
 
diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index dfed84a..fe7e85e 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
+import HepLean.SpaceTime.Basic
 import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.TargetSpace
 import Mathlib.Data.Complex.Exponential
@@ -14,7 +15,6 @@ import Mathlib.RepresentationTheory.Basic
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Geometry.Manifold.ContMDiff.Product
-import Mathlib.Analysis.Complex.RealDeriv
 import Mathlib.Algebra.QuadraticDiscriminant
 /-!
 # The Higgs field
diff --git a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
index c5f8646..73797e4 100644
--- a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
+++ b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
@@ -7,14 +7,13 @@ import HepLean.StandardModel.Basic
 import HepLean.StandardModel.Representations
 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.RepresentationTheory.Basic
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Geometry.Manifold.ContMDiff.Product
 import Mathlib.Algebra.QuadraticDiscriminant
+import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
 /-!
 # The Higgs vector space
 
diff --git a/HepLean/StandardModel/Representations.lean b/HepLean/StandardModel/Representations.lean
index 6f68ae1..4500ee5 100644
--- a/HepLean/StandardModel/Representations.lean
+++ b/HepLean/StandardModel/Representations.lean
@@ -3,14 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.StandardModel.Basic
 import Mathlib.Data.Complex.Exponential
-import Mathlib.Geometry.Manifold.VectorBundle.Basic
-import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
-import Mathlib.RepresentationTheory.Basic
 import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 # Representations appearing in the Standard Model
 
diff --git a/scripts/lint-all.sh b/scripts/lint-all.sh
index 4a0f7f0..6c91394 100755
--- a/scripts/lint-all.sh
+++ b/scripts/lint-all.sh
@@ -12,4 +12,8 @@ lake build HepLean
 
 echo "Run linter"
 
-lake exe runLinter HepLean
\ No newline at end of file
+lake exe runLinter HepLean
+
+echo "Run shake"
+
+lake exe shake HepLean
\ No newline at end of file