Refactor: Lint

HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean

@@ -40,7 +40,8 @@ lemma lineY₃B₃Charges_quad (a b : ℚ) : accQuad (lineY₃B₃Charges a b).v
   rw [quadBiLin.toHomogeneousQuad.map_smul]
   rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
   erw [quadSol Y₃.1, quadSol B₃.1]
-  simp
+  simp only [mul_zero, add_zero, quadBiLin_toFun, Fin.isValue, Fin.reduceFinMk, zero_add,
+    mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
   apply Or.inr ∘ Or.inr
   rfl
 
@@ -71,7 +72,8 @@ lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
   repeat rw [toSMSpecies_toSpecies_inv]
   rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
   rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
-  simp
+  simp only [mul_one, Fin.isValue, toSMSpecies_apply, one_mul, mul_neg, neg_neg, neg_mul, zero_mul,
+    add_zero, neg_zero, Hd_apply, Fin.reduceFinMk, Hu_apply]
   have hLin := R.linearSol
   simp at hLin
   have h1 := hLin 1

HepLean/AnomalyCancellation/MSSMNu/Permutations.lean

@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 import HepLean.AnomalyCancellation.MSSMNu.Basic
 import Mathlib.Tactic.Polyrith
 import HepLean.AnomalyCancellation.GroupActions
-universe v u
 /-!
 # Permutations of MSSM charges and solutions
 
@@ -14,6 +13,9 @@ The three family MSSM charges has a family permutation of S₃⁶. This file def
 and its action on the MSSM.
 
 -/
+
+universe v u
+
 open Nat
 open  Finset
 

HepLean/AnomalyCancellation/MSSMNu/Y3.lean

@@ -68,7 +68,8 @@ lemma doublePoint_Y₃_Y₃ (R : MSSMACC.LinSols) :
   rw [Y₃AsCharge]
   repeat rw [toSMSpecies_toSpecies_inv]
   rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
-  simp
+  simp only [mul_one, Fin.isValue, toSMSpecies_apply, one_mul, mul_neg, neg_mul, neg_neg, mul_zero,
+    zero_mul, add_zero, Hd_apply, Fin.reduceFinMk, Hu_apply]
   have hLin := R.linearSol
   simp at hLin
   have h3 := hLin 3