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