From 2681709f934e19733b3a14a00c6c6177c5ff45b6 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 11 Jul 2024 09:20:27 -0400
Subject: [PATCH] refactor: Some lint

---
 HepLean.lean                               | 2 +-
 HepLean/SpaceTime/LorentzTensor/Basic.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 96bf060..cca5867 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -69,7 +69,7 @@ import HepLean.SpaceTime.LorentzGroup.Boosts
 import HepLean.SpaceTime.LorentzGroup.Orthochronous
 import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Rotations
-import HepLean.SpaceTime.LorentzTensors.Basic
+import HepLean.SpaceTime.LorentzTensor.Basic
 import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 import HepLean.SpaceTime.LorentzVector.Basic
 import HepLean.SpaceTime.LorentzVector.NormOne
diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean
index f5fddba..fa7cf90 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzVector.Basic
 import Mathlib.CategoryTheory.Limits.FintypeCat
-import LeanCopilot
 /-!
 
 # Lorentz Tensors
@@ -158,6 +157,7 @@ lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := by
 ## Rising and lowering indices
 
 Rising or lowering an index corresponds to changing the color of that index.
+
 -/
 
 /-! TODO: Define the rising and lowering of indices using contraction with the metric. -/