From e6045e5f58eb331d3e3a6956f3e0248b2150044a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Sat, 2 Nov 2024 08:03:04 +0000
Subject: [PATCH] fix: Anomaly Cancellation Group Actions & others

---
 HepLean/AnomalyCancellation/GroupActions.lean      | 14 +++++++-------
 .../AnomalyCancellation/PureU1/BasisLinear.lean    |  9 +++++----
 HepLean/AnomalyCancellation/SM/FamilyMaps.lean     |  2 +-
 HepLean/FeynmanDiagrams/Momentum.lean              |  2 +-
 4 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean
index 03ef5b8..4639d5a 100644
--- a/HepLean/AnomalyCancellation/GroupActions.lean
+++ b/HepLean/AnomalyCancellation/GroupActions.lean
@@ -89,16 +89,16 @@ instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
     rfl
 
 lemma linSolRep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
-    (S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun S g) =
+    (S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun _ _ S g) =
     G.linSolRep g (χ.quadSolsInclLinSols S) := rfl
 
 lemma rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
-    (S : χ.QuadSols) : χ.quadSolsIncl (G.quadSolAction.toFun S g) =
+    (S : χ.QuadSols) : χ.quadSolsIncl (G.quadSolAction.toFun _ _ S g) =
     G.rep g (χ.quadSolsIncl S) := rfl
 
 /-- The group action acting on solutions to the anomaly cancellation conditions. -/
 instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.Sols where
-  smul g S := ⟨G.quadSolAction.toFun S.1 g, by
+  smul g S := ⟨G.quadSolAction.toFun _ _ S.1 g, by
     simp only [MulAction.toFun_apply]
     change χ.cubicACC (G.rep g S.val) = 0
     rw [G.cubicInvariant, S.cubicSol]⟩
@@ -114,14 +114,14 @@ instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.
     rfl
 
 lemma quadSolAction_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
-    (S : χ.Sols) : χ.solsInclQuadSols (G.solAction.toFun S g) =
-    G.quadSolAction.toFun (χ.solsInclQuadSols S) g := rfl
+    (S : χ.Sols) : χ.solsInclQuadSols (G.solAction.toFun _ _ S g) =
+    G.quadSolAction.toFun _ _ (χ.solsInclQuadSols S) g := rfl
 
 lemma linSolRep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
-    (S : χ.Sols) : χ.solsInclLinSols (G.solAction.toFun S g) =
+    (S : χ.Sols) : χ.solsInclLinSols (G.solAction.toFun _ _ S g) =
     G.linSolRep g (χ.solsInclLinSols S) := rfl
 
 lemma rep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
-    (S : χ.Sols) : χ.solsIncl (G.solAction.toFun S g) = G.rep g (χ.solsIncl S) := rfl
+    (S : χ.Sols) : χ.solsIncl (G.solAction.toFun _ _ S g) = G.rep g (χ.solsIncl S) := rfl
 
 end ACCSystemGroupAction
diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
index 7136725..22fdc52 100644
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -66,7 +66,7 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
       split
       · rename_i ht
         exact (hn ht).elim
-      · rfl
+      · with_unfolding_all rfl
     · intro k _ hkj
       exact asCharges_ne_castSucc hkj.symm
     · intro hk
@@ -124,10 +124,11 @@ instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
   Module.Finite.of_basis asBasis
 
 lemma finrank_AnomalyFreeLinear :
-    FiniteDimensional.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
+    Module.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
   have h := Module.mk_finrank_eq_card_basis (@asBasis n)
-  simp only [Nat.succ_eq_add_one, finrank_eq_rank, Cardinal.mk_fintype, Fintype.card_fin] at h
-  exact FiniteDimensional.finrank_eq_of_rank_eq h
+  simp only [Nat.succ_eq_add_one, Module.finrank_eq_rank, Cardinal.mk_fintype,
+    Fintype.card_fin] at h
+  exact Module.finrank_eq_of_rank_eq h
 
 end BasisLinear
 
diff --git a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
index ac3a282..b3c2b4e 100644
--- a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
@@ -65,7 +65,7 @@ def speciesEmbed (m n : ℕ) :
     by_cases hi : i.val < m
     · erw [dif_pos hi, dif_pos hi, dif_pos hi]
     · erw [dif_neg hi, dif_neg hi, dif_neg hi]
-      rfl
+      with_unfolding_all rfl
   map_smul' a S := by
     funext i
     simp only [SMSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index ddeefde..5458749 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -182,7 +182,7 @@ allowed space of half-edge momenta.
 
 /-- The number of loops of a Feynman diagram. Defined as the dimension
   of the space of allowed Half-loop momenta. -/
-noncomputable def numberOfLoops : ℕ := FiniteDimensional.finrank ℝ F.allowedHalfEdgeMomenta
+noncomputable def numberOfLoops : ℕ := Module.finrank ℝ F.allowedHalfEdgeMomenta
 
 /-!