From 0228cd4cf1cd45da131881872dfa928b7f2dc0cd Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 19 Jun 2024 13:07:37 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean.lean                                | 1 +
 HepLean/FeynmanDiagrams/Basic.lean          | 1 -
 HepLean/FeynmanDiagrams/Instances/Phi4.lean | 3 ---
 3 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 18386db..ee22052 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -51,6 +51,7 @@ import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4
+import HepLean.FeynmanDiagrams.Momentum
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index dc69ac2..d63e93a 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -16,7 +16,6 @@ import Mathlib.Data.Fintype.Perm
 import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Combinatorics.SimpleGraph.Connectivity
 import Mathlib.SetTheory.Cardinal.Basic
-import LeanCopilot
 /-!
 # Feynman diagrams
 
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 9ecb20e..513abff 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -90,9 +90,6 @@ lemma figureEight_connected : Connected figureEight := by decide
   `#eval symmetryFactor figureEight`. -/
 lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
 
-lemma figureEight_halfEdgeToEdgeIntMatrix :
-  figureEight.halfEdgeToEdgeIntMatrix  = !![1, 0; 1, 0 ; 0, 1; 0, 1] := by decide
-
 end Example