From 08f0a01e9d5532eae4e0fac23ab2e3a0a870e0e1 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 21 Mar 2025 11:12:58 -0400
Subject: [PATCH] refactor: lint

---
 PhysLean/Electromagnetism/MaxwellEquations.lean            | 1 -
 PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean     | 2 --
 .../Particles/StandardModel/HiggsBoson/GaugeAction.lean    | 2 --
 PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean   | 7 ++++---
 .../Relativity/Lorentz/RealTensor/Vector/Pre/Basic.lean    | 2 +-
 5 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/PhysLean/Electromagnetism/MaxwellEquations.lean b/PhysLean/Electromagnetism/MaxwellEquations.lean
index 011d204..532fb5e 100644
--- a/PhysLean/Electromagnetism/MaxwellEquations.lean
+++ b/PhysLean/Electromagnetism/MaxwellEquations.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Electromagnetism.Basic
-import PhysLean.Relativity.SpaceTime.Basic
 /-!
 
 # Maxwell's equations
diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean b/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean
index f31c098..e7bd3f9 100644
--- a/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean
+++ b/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.SpaceTime.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
-import PhysLean.Meta.Informal.Basic
 /-!
 
 # The Higgs field
diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/GaugeAction.lean b/PhysLean/Particles/StandardModel/HiggsBoson/GaugeAction.lean
index 3094db6..67bfea9 100644
--- a/PhysLean/Particles/StandardModel/HiggsBoson/GaugeAction.lean
+++ b/PhysLean/Particles/StandardModel/HiggsBoson/GaugeAction.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Particles.StandardModel.HiggsBoson.Basic
-import Mathlib.RepresentationTheory.Basic
 import PhysLean.Particles.StandardModel.Basic
 import PhysLean.Particles.StandardModel.Representations
-import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 
 # The action of the gauge group on the Higgs field
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean b/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean
index 36d43f7..e44e497 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean
@@ -82,9 +82,11 @@ lemma toCoord_tprod {d : ℕ} (p : (i : Fin 1) →
       ((Lorentz.contrBasisFin d).repr (p 0))
       (indexEquiv.symm i 0) := by
   rw [toCoord_apply]
-  simp
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, C_eq_color, OverColor.mk_left, Functor.id_obj,
+    OverColor.mk_hom, Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Fin.isValue]
   erw [TensorSpecies.TensorBasis.tensorBasis_repr_tprod]
-  simp
+  simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, C_eq_color,
+    Finset.prod_singleton, cons_val_zero]
   rfl
 
 lemma tensorNode_repr_apply {d : ℕ} (p : Vector d)
@@ -294,7 +296,6 @@ lemma action_apply_eq_sum (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vecto
     rw [← mul_assoc, mul_comm _ r, mul_assoc]
   rw [← Finset.mul_sum]
   congr
-  have hl : (𝟭 Type).obj (OverColor.mk ![Color.up]).left = Fin 1 := by rfl
   simp_all only [Nat.succ_eq_add_one, OverColor.mk_left, _root_.zero_add, Functor.id_obj,
     C_eq_color, OverColor.mk_hom]
   erw [toCoord_tprod]
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Vector/Pre/Basic.lean b/PhysLean/Relativity/Lorentz/RealTensor/Vector/Pre/Basic.lean
index 16f4732..9f22dbe 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Vector/Pre/Basic.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Vector/Pre/Basic.lean
@@ -54,7 +54,7 @@ lemma contrBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
   simp only [contrBasisFin, Basis.reindex_apply, contrBasis_toFin1dℝ, Basis.coe_ofEquivFun]
 
 lemma contrBasisFin_repr_apply {d : ℕ} (p : Contr d) (i : Fin (1 + d)) :
-  (contrBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := by rfl
+    (contrBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := by rfl
 
 /-- The representation of contravariant Lorentz vectors forms a topological space, induced
   by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/