From f50b2547c76a144e417219abca0417e1769f3541 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 13 Jun 2024 10:59:10 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean.lean                              | 1 +
 HepLean/AnomalyCancellation/SM/Basic.lean | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/HepLean.lean b/HepLean.lean
index 429a466..4934ff8 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -68,6 +68,7 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous
 import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.Metric
+import HepLean.SpaceTime.SL2C.Basic
 import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
 import HepLean.StandardModel.HiggsBoson.TargetSpace
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index 411e2fd..83fa2dd 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -52,7 +52,7 @@ lemma charges_eq_toSpecies_eq (S T : (SMCharges n).charges) :
   exact fun a i => congrArg (⇑(toSpecies i)) a
   intro h
   apply toSpeciesEquiv.injective
-  exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ a => h x
+  exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ _ => h x
 
 lemma toSMSpecies_toSpecies_inv (i : Fin 5) (f :  (Fin 5 → Fin n → ℚ) ) :
     (toSpecies i) (toSpeciesEquiv.symm f) = f i := by