From c7ad21ceb6bcaf1d0ee8856da3bb70e5ccd76676 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Apr 2024 16:04:53 -0400
Subject: [PATCH] refactor

---
 HepLean/AnomalyCancellation/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 62d3f06..4695374 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -191,7 +191,7 @@ instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols wher
     intro i
     erw [(χ.quadraticACCs i).map_smul]
     rw [S.quadSol i]
-    simp
+    simp only [mul_zero]
     ⟩
   mul_smul a b S := by
     apply QuadSols.ext
@@ -277,7 +277,7 @@ def Hom.comp {χ η ε : ACCSystem} (g : Hom η ε) (f : Hom χ η) : Hom χ ε
   charges := LinearMap.comp g.charges f.charges
   anomalyFree := g.anomalyFree ∘ f.anomalyFree
   commute := by
-    simp
+    simp only [LinearMap.coe_comp]
     rw [Function.comp.assoc]
     rw [f.commute, ← Function.comp.assoc, g.commute, Function.comp.assoc]