From 36752fa5c4096385289b8cf049a933ede14f37ac Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 17 Jul 2024 15:15:44 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean/SpaceTime/LorentzTensor/Real/Basic.lean | 17 ++++++++---------
 .../LorentzTensor/Real/LorentzAction.lean       |  9 +++++----
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 09cdaa4..f1249fb 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -5,9 +5,9 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Data.Real.Basic
-import Mathlib.Analysis.Normed.Field.Basic
-import Mathlib.CategoryTheory.Core
-import Mathlib.CategoryTheory.Types
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Logic.Equiv.Fin
+import Mathlib.Tactic.FinCases
 /-!
 
 # Real Lorentz Tensors
@@ -61,10 +61,9 @@ structure RealLorentzTensor (d : ℕ) (X : Type) where
   coord : RealLorentzTensor.IndexValue d color → ℝ
 
 namespace RealLorentzTensor
-open Matrix CategoryTheory
+open Matrix
 universe u1
-variable {d : ℕ} {X Y Z : Type}
-variable (c : X → Colors)
+variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
 
 /-!
 
@@ -144,7 +143,7 @@ def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
   Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
 
 lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
-      (h : i = j ∘ f) (y : IndexValue d j) (x : X) :
+    (h : i = j ∘ f) (y : IndexValue d j) (x : X) :
     (indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by
   rfl
 
@@ -324,7 +323,7 @@ def UnmarkedIndexValue (T : Marked d X n) : Type :=
 instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue :=
   Pi.fintype
 
-instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
+instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
   Fintype.decidablePiFintype
 
 /-- The index values restricted to marked indices. -/
@@ -334,7 +333,7 @@ def MarkedIndexValue (T : Marked d X n) : Type :=
 instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue :=
   Pi.fintype
 
-instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
+instance [Fintype X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
   Fintype.decidablePiFintype
 
 lemma color_eq_elim (T : Marked d X n) :
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index 05554da..a565058 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -167,12 +167,13 @@ lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y
       (oneMarkedIndexValue x) := by
   rw [toTensorRepMat_apply, toTensorRepMat_apply]
   erw [Finset.prod_singleton, Finset.prod_singleton]
-  simp
+  simp only [Fin.zero_eta, Fin.isValue, lorentzGroupIsGroup_inv]
   rw [colorMatrix_cast h, colorMatrix_dual_cast]
   rw [Matrix.reindex_apply, Matrix.reindex_apply]
-  simp
+  simp only [Fin.isValue, lorentzGroupIsGroup_inv, minkowskiMetric.dual_dual, Subtype.coe_eta,
+    Equiv.symm_symm, Matrix.submatrix_apply]
   rw [colorMatrix_transpose]
-  simp
+  simp only [Fin.isValue, Matrix.transpose_apply]
   apply congrArg
   simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk,
     Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply,
@@ -276,7 +277,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT
   rw [mapIso_apply_coord]
   rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
   let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
-    indexValueIso d f (by funext x ; simp)
+    indexValueIso d f (by funext x; simp)
   rw [← Equiv.sum_comp is]
   refine Finset.sum_congr rfl (fun j _ => ?_)
   rw [mapIso_apply_coord]