fix: File import

HepLean.lean

@@ -73,6 +73,8 @@ import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.LorentzTensor.Basic
 import HepLean.SpaceTime.LorentzTensor.Contraction
 import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Basic
+import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.IndexNotation
+import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Lemmas
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.AreDual
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean

@@ -10,7 +10,6 @@ import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Basic
 
 # Index notation for Einstein tensors
 
-
 -/
 
 instance : IndexNotation einsteinTensorColor.Color where
@@ -36,14 +35,13 @@ variable {R : Type} [CommSemiring R] {n m : ℕ}
 instance : IndexNotation (einsteinTensor R n).Color := instIndexNotationColorEinsteinTensorColor
 instance : DecidableEq (einsteinTensor R n).Color := instDecidableEqColorEinsteinTensorColor
 
-
 @[simp]
 lemma indexNotation_eq_color : @einsteinTensor.instIndexNotationColor R _ n =
     instIndexNotationColorEinsteinTensorColor := by
   rfl
 
 @[simp]
-lemma decidableEq_eq_color : @einsteinTensor.instDecidableEqColor R _ n  =
+lemma decidableEq_eq_color : @einsteinTensor.instDecidableEqColor R _ n =
     instDecidableEqColorEinsteinTensorColor := by
   rfl
 
@@ -55,7 +53,6 @@ lemma einsteinTensor_color : (einsteinTensor R n).Color = einsteinTensorColor.Co
 lemma toTensorColor_eq : (einsteinTensor R n).toTensorColor = einsteinTensorColor := by
   rfl
 
-
 /-- The construction of a tensor index from a tensor and a string satisfying conditions
   which can be automatically checked. This is a modified version of
   `TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/
@@ -86,14 +83,12 @@ lemma fromIndexStringColor_indexList {R : Type} [CommSemiring R]
     (fromIndexStringColor T s hs hn hD hC hd).toIndexList = toIndexList' s hs := by
   rfl
 
-
 /-- A tactic used to prove `boolFin` for real Lornetz tensors. -/
 macro "dualMapTactic" : tactic =>
     `(tactic| {
     simp only [toTensorColor_eq]
     decide })
 
-
 /-- Notation for the construction of a tensor index from a tensor and a string.
   Conditions are checked automatically. -/
 notation:20 T "|" S:21 => fromIndexStringColor T S
@@ -119,8 +114,6 @@ lemma mem_fin_list (n : ℕ) (i : Fin n) : i ∈ Fin.list n := by
 instance (n : ℕ) (i : Fin n) : Decidable (i ∈ Fin.list n) :=
   isTrue (mem_fin_list n i)
 
-
-
 /-- The product of Real Lorentz tensors. Conditions on indices are checked automatically. -/
 notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (by prodTactic)
 /-- An example showing the allowed constructions. -/

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/lemmas.lean

@@ -9,7 +9,6 @@ import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.IndexNotation
 
 # Lemmas regarding Einstein tensors
 
-
 -/
 namespace einsteinTensor
 
@@ -17,10 +16,9 @@ open einsteinTensorColor
 open IndexNotation IndexString
 open TensorStructure TensorIndex
 
-
 variable {R : Type} [CommSemiring R] {n m : ℕ}
 /-lemma swap_eq_transpose (T : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit]) :
-     (T|"ᵢ₁ᵢ₂") ≈ ((toMatrix.symm (toMatrix T).transpose)|"ᵢ₂ᵢ₁") := by
+    (T|"ᵢ₁ᵢ₂") ≈ ((toMatrix.symm (toMatrix T).transpose)|"ᵢ₂ᵢ₁") := by
   apply And.intro
   · apply And.intro
     simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr, fromIndexStringColor,