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

---
 HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
index 9809f9a..2516212 100644
--- a/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
@@ -27,7 +27,7 @@ def equiv : (PureU1 2).LinSols ≃ (PureU1 2).Sols where
     have hLin := pureU1_linear S
     simp at hLin
     erw [accCube_explicit]
-    simp
+    simp only [Fin.sum_univ_two, Fin.isValue]
     rw [show S.val (0 : Fin 2) = - S.val (1 : Fin 2) by linear_combination hLin]
     ring⟩
   invFun S := S.1.1