diff --git a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Basic.lean
index b58e6a3fc..51af2f8a7 100644
--- a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Basic.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Basic.lean
@@ -96,14 +96,14 @@ def accGrav : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     -- rw [show Rat.cast a = a from rfl]
     ring
 
@@ -163,10 +163,10 @@ def accSU3 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
     repeat rw [Finset.sum_add_distrib]
@@ -197,14 +197,14 @@ def accYY : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     repeat rw [map_smul]
     simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     -- rw [show Rat.cast a = a from rfl]
     ring
 
@@ -235,7 +235,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
     simp only
     rw [Finset.mul_sum]
     refine Fintype.sum_congr _ _ fun i ↦ ?_
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     ring)
   (by
@@ -256,9 +256,8 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
 lemma quadBiLin_decomp (S T : (SMνCharges n).Charges) :
     quadBiLin S T = ∑ i, Q S i * Q T i - 2 * ∑ i, U S i * U T i +
         ∑ i, D S i * D T i - ∑ i, L S i * L T i + ∑ i, E S i * E T i := by
-  erw [← quadBiLin.toFun_eq_coe]
   rw [quadBiLin]
-  simp only [BiLinearSymm.mk₂, AddHom.toFun_eq_coe, AddHom.coe_mk, LinearMap.coe_mk]
+  rw [BiLinearSymm.mk₂_toFun_apply]
   repeat rw [Finset.sum_add_distrib]
   repeat rw [← Finset.mul_sum]
   simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul, add_left_inj]
@@ -272,7 +271,8 @@ def accQuad : HomogeneousQuadratic (SMνCharges n).Charges :=
 lemma accQuad_decomp (S : (SMνCharges n).Charges) :
     accQuad S = ∑ i, (Q S i)^2 - 2 * ∑ i, (U S i)^2 + ∑ i, (D S i)^2 - ∑ i, (L S i)^2
     + ∑ i, (E S i)^2 := by
-  erw [quadBiLin_decomp]
+  change (quadBiLin S) S = _
+  rw [quadBiLin_decomp]
   ring_nf
 
 /-- Extensionality lemma for `accQuad`. -/
@@ -281,8 +281,7 @@ lemma accQuad_ext {S T : (SMνCharges n).Charges}
     ∑ i, ((fun a => a^2) ∘ toSpecies j T) i) :
     accQuad S = accQuad T := by
   rw [accQuad_decomp, accQuad_decomp]
-  erw [h 0, h 1, h 2, h 3, h 4]
-  rfl
+  simp_all
 
 /-- The symmetric trilinear form used to define the cubic acc. -/
 @[simps!]
@@ -298,7 +297,7 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
     simp only
     rw [Finset.mul_sum]
     refine Fintype.sum_congr _ _ fun i ↦ ?_
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue]
     ring)
   (by
@@ -306,7 +305,7 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
     simp only
     rw [← Finset.sum_add_distrib]
     refine Fintype.sum_congr _ _ fun i ↦ ?_
-    repeat erw [map_add]
+    repeat rw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
     ring)
   (by
@@ -324,12 +323,10 @@ lemma cubeTriLin_decomp (S T R : (SMνCharges n).Charges) :
     cubeTriLin S T R = 6 * ∑ i, (Q S i * Q T i * Q R i) + 3 * ∑ i, (U S i * U T i * U R i) +
       3 * ∑ i, (D S i * D T i * D R i) + 2 * ∑ i, (L S i * L T i * L R i) +
       ∑ i, (E S i * E T i * E R i) + ∑ i, (N S i * N T i * N R i) := by
-  erw [← cubeTriLin.toFun_eq_coe]
   rw [cubeTriLin]
-  simp only [TriLinearSymm.mk₃, BiLinearSymm.mk₂, SMνSpecies_numberCharges, toSpecies_apply,
-    Fin.isValue, AddHom.toFun_eq_coe, AddHom.coe_mk, LinearMap.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
+  rw [TriLinearSymm.mk₃_toFun_apply_apply]
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
 
 /-- The cubic ACC. -/
 @[simp]
@@ -347,12 +344,7 @@ lemma accCube_ext {S T : (SMνCharges n).Charges}
     (h : ∀ j, ∑ i, ((fun a => a^3) ∘ toSpecies j S) i =
     ∑ i, ((fun a => a^3) ∘ toSpecies j T) i) :
     accCube S = accCube T := by
-  rw [accCube_decomp]
-  have h1 : ∀ j, ∑ i, (toSpecies j S i) ^ 3 = ∑ i, (toSpecies j T i) ^ 3 := by
-    intro j
-    erw [h]
-    rfl
-  repeat rw [h1]
-  rw [accCube_decomp]
+  repeat rw [accCube_decomp]
+  simp_all
 
 end SMνACCs
diff --git a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean
index 704d34c5b..b34facbac 100644
--- a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean
@@ -38,8 +38,8 @@ def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ]
 lemma chargesMapOfSpeciesMap_toSpecies {n m : ℕ}
     (f : (SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Charges)
     (S : (SMνCharges n).Charges) (j : Fin 6) :
-    toSpecies j (chargesMapOfSpeciesMap f S) = (LinearMap.comp f (toSpecies j)) S := by
-  erw [toSMSpecies_toSpecies_inv]
+    toSpecies j (chargesMapOfSpeciesMap f S) = (LinearMap.comp f (toSpecies j)) S :=
+  toSMSpecies_toSpecies_inv _ _
 
 /-- The projection of the `m`-family charges onto the first `n`-family charges for species. -/
 @[simps!]
@@ -68,16 +68,16 @@ def speciesEmbed (m n : ℕ) :
     funext i
     simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
     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]
+    · rw [dif_pos hi, dif_pos hi, dif_pos hi]
+    · rw [dif_neg hi, dif_neg hi, dif_neg hi]
       with_unfolding_all rfl
   map_smul' a S := by
     funext i
     simp only [SMνSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
       eq_ratCast, Rat.cast_eq_id, id_eq]
     by_cases hi : i.val < m
-    · erw [dif_pos hi, dif_pos hi]
-    · erw [dif_neg hi, dif_neg hi]
+    · rw [dif_pos hi, dif_pos hi]
+    · rw [dif_neg hi, dif_neg hi]
       exact Eq.symm (Rat.mul_zero a)
 
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
@@ -101,7 +101,7 @@ def familyUniversal (n : ℕ) : (SMνCharges 1).Charges →ₗ[ℚ] (SMνCharges
 
 lemma toSpecies_familyUniversal {n : ℕ} (j : Fin 6) (S : (SMνCharges 1).Charges)
     (i : Fin n) : toSpecies j (familyUniversal n S) i = toSpecies j S ⟨0, by simp⟩ := by
-  erw [chargesMapOfSpeciesMap_toSpecies]
+  rw [familyUniversal, chargesMapOfSpeciesMap_toSpecies]
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
diff --git a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Permutations.lean b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Permutations.lean
index 304b8dc06..88ba7d690 100644
--- a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Permutations.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Permutations.lean
@@ -52,23 +52,22 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMνCharges n).Char
     rw [charges_eq_toSpecies_eq]
     intro i
     simp only [chargeMap_apply, Pi.inv_apply, Module.End.mul_apply]
-    repeat erw [toSMSpecies_toSpecies_inv]
+    repeat rw [toSMSpecies_toSpecies_inv]
     rfl
   map_one' := by
     refine LinearMap.ext fun S => ?_
     rw [charges_eq_toSpecies_eq]
     intro i
-    erw [toSMSpecies_toSpecies_inv]
-    rfl
+    exact toSMSpecies_toSpecies_inv _ _
 
 lemma repCharges_toSpecies (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) :
-    toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
-  erw [toSMSpecies_toSpecies_inv]
+    toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j :=
+  toSMSpecies_toSpecies_inv _ _
 
 lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) :
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
-  erw [repCharges_toSpecies]
+  rw [repCharges_toSpecies]
   change ∑ i : Fin n, ((fun a => a ^ m) ∘ _) (⇑(f⁻¹ _) i) = ∑ i : Fin n, ((fun a => a ^ m) ∘ _) i
   refine Equiv.Perm.sum_comp _ _ _ ?_
   simp only [PermGroup, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
diff --git a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/HyperCharge.lean b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/HyperCharge.lean
index 10da69a96..49604ac15 100644
--- a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/HyperCharge.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/HyperCharge.lean
@@ -74,7 +74,7 @@ lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
   erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (Y n)).1]
   rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂, quadBiLin.swap, on_quadBiLin_AFL]
-  erw [accQuad.map_smul]
+  rw [← accQuad, accQuad.map_smul]
   simp
 
 lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/Basic.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/Basic.lean
index 9b7777e23..b34e7625c 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/Basic.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/Basic.lean
@@ -86,14 +86,14 @@ def accGrav : (SMCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
     ring
 
@@ -103,10 +103,9 @@ lemma accGrav_ext {S T : (SMCharges n).Charges}
     accGrav S = accGrav T := by
   simp only [accGrav, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
     AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  erw [hj, hj, hj, hj, hj]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 /-- The `SU(2)` anomaly equation. -/
 @[simp]
@@ -116,14 +115,14 @@ def accSU2 : (SMCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
     ring
 
@@ -133,8 +132,8 @@ lemma accSU2_ext {S T : (SMCharges n).Charges}
     accSU2 S = accSU2 T := by
   simp only [accSU2, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
     AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
   exact Mathlib.Tactic.LinearCombination.add_eq_eq (congrArg (HMul.hMul 3) (hj 0)) (hj 3)
 
 /-- The `SU(3)` anomaly equations. -/
@@ -145,14 +144,14 @@ def accSU3 : (SMCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
     ring
 
@@ -162,10 +161,9 @@ lemma accSU3_ext {S T : (SMCharges n).Charges}
     accSU3 S = accSU3 T := by
   simp only [accSU3, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
     AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  erw [hj, hj, hj]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 /-- The `Y²` anomaly equation. -/
 @[simp]
@@ -176,14 +174,14 @@ def accYY : (SMCharges n).Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
       Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
       eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     ring
 
 /-- Extensionality lemma for `accYY`. -/
@@ -192,10 +190,9 @@ lemma accYY_ext {S T : (SMCharges n).Charges}
     accYY S = accYY T := by
   simp only [accYY, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
     AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  erw [hj, hj, hj, hj, hj]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 /-- The quadratic bilinear map. -/
 @[simps!]
@@ -211,7 +208,7 @@ def quadBiLin : BiLinearSymm (SMCharges n).Charges := BiLinearSymm.mk₂
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     ring)
   (by
@@ -220,7 +217,7 @@ def quadBiLin : BiLinearSymm (SMCharges n).Charges := BiLinearSymm.mk₂
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
     intro i
-    repeat erw [map_add]
+    repeat rw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
       one_mul]
     ring)
@@ -243,14 +240,11 @@ lemma accQuad_ext {S T : (SMCharges n).Charges}
     ∑ i, ((fun a => a^2) ∘ toSpecies j T) i) :
     accQuad S = accQuad T := by
   simp only [HomogeneousQuadratic, accQuad, BiLinearSymm.toHomogeneousQuad_apply]
-  erw [← quadBiLin.toFun_eq_coe]
-  rw [quadBiLin]
-  simp only [BiLinearSymm.mk₂, AddHom.toFun_eq_coe, AddHom.coe_mk, LinearMap.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
+  simp only [quadBiLin, BiLinearSymm.mk₂_toFun_apply]
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
   ring_nf
-  erw [h 0, h 1, h 2, h 3, h 4]
-  rfl
+  simp_all
 
 /-- The trilinear function defining the cubic. -/
 @[simps!]
@@ -266,7 +260,7 @@ def cubeTriLin : TriLinearSymm (SMCharges n).Charges := TriLinearSymm.mk₃
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue]
     ring)
   (by
@@ -275,7 +269,7 @@ def cubeTriLin : TriLinearSymm (SMCharges n).Charges := TriLinearSymm.mk₃
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
     intro i
-    repeat erw [map_add]
+    repeat rw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
     ring)
   (by
@@ -303,13 +297,9 @@ lemma accCube_ext {S T : (SMCharges n).Charges}
     accCube S = accCube T := by
   simp only [HomogeneousCubic, accCube, cubeTriLin, TriLinearSymm.toCubic_apply,
     TriLinearSymm.mk₃_toFun_apply_apply]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
   ring_nf
-  have h1 : ∀ j, ∑ i, (toSpecies j S i)^3 = ∑ i, (toSpecies j T i)^3 := by
-    intro j
-    erw [h]
-    rfl
-  repeat rw [h1]
+  simp_all
 
 end SMACCs
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean
index 08e273b0a..faf30dc87 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean
@@ -66,16 +66,16 @@ def speciesEmbed (m n : ℕ) :
     funext i
     simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
     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]
+    · rw [dif_pos hi, dif_pos hi, dif_pos hi]
+    · rw [dif_neg hi, dif_neg hi, dif_neg hi]
       with_unfolding_all rfl
   map_smul' a S := by
     funext i
     simp only [SMSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
       eq_ratCast, Rat.cast_eq_id, id_eq]
     by_cases hi : i.val < m
-    · erw [dif_pos hi, dif_pos hi]
-    · erw [dif_neg hi, dif_neg hi]
+    · rw [dif_pos hi, dif_pos hi]
+    · rw [dif_neg hi, dif_neg hi]
       exact Eq.symm (Rat.mul_zero a)
 
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
index f776cb388..ceb85e580 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
@@ -43,12 +43,12 @@ lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
   rw [accGrav]
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
-  erw [hQ, E_zero_iff_Q_zero.mp hQ]
+  rw [hQ, E_zero_iff_Q_zero.mp hQ]
   have h1 := SU2Sol S.1.1
   have h2 := SU3Sol S.1.1
   simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
       Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk, accSU3] at h1 h2
-  erw [hQ] at h1 h2
+  rw [hQ] at h1 h2
   simp_all
   linear_combination 3 * h2
 
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
index 296880dba..3e88529e0 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
@@ -69,12 +69,12 @@ def asLinear (S : linearParameters) : (SMNoGrav 1).LinSols :=
   chargeToLinear S.asCharges (by
     simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
       Fin.isValue, Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
-    erw [speciesVal, speciesVal]
+    rw [speciesVal, speciesVal]
     simp)
     (by
     simp only [accSU3, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
       Fin.isValue, Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
-    repeat erw [speciesVal]
+    repeat rw [speciesVal]
     simp only [asCharges, neg_add_rev]
     ring)
 
@@ -88,7 +88,7 @@ lemma cubic (S : linearParameters) :
     TriLinearSymm.mk₃_toFun_apply_apply]
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton]
-  repeat erw [speciesVal]
+  repeat rw [speciesVal]
   simp only [asCharges, neg_add_rev, neg_mul, mul_neg, neg_neg]
   ring
 
@@ -125,7 +125,8 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
     apply linearParameters.ext
     · rfl
     · simp only [Fin.isValue]
-      repeat erw [speciesVal]
+      repeat rw [asLinear_val]
+      repeat rw [speciesVal]
       simp only [asCharges, neg_add_rev]
       ring
     · rfl
@@ -141,7 +142,7 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
       ext
       simp
     subst hj
-    erw [speciesVal]
+    rw [speciesVal]
     have h1 := SU3Sol S
     simp only [accSU3, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
       Fin.isValue, toSpecies_apply, Finset.sum_singleton,
@@ -180,7 +181,7 @@ lemma grav (S : linearParameters) :
   rw [accGrav]
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
-  repeat erw [speciesVal]
+  repeat rw [speciesVal]
   simp only [asCharges, neg_add_rev, neg_mul, mul_neg]
   ring_nf
   rw [add_comm, add_eq_zero_iff_eq_neg]
@@ -276,9 +277,12 @@ def bijection : linearParametersQENeqZero ≃
     {S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} :=
   bijectionLinearParameters.trans (linearParameters.bijectionQEZero)
 
+lemma bijection_coe_val (S : linearParametersQENeqZero) :
+    (bijection S).1.val = (bijectionLinearParameters S : linearParameters).asCharges := rfl
+
 lemma cubic (S : linearParametersQENeqZero) :
     accCube (bijection S).1.val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1 := by
-  erw [linearParameters.cubic]
+  rw [bijection_coe_val, linearParameters.cubic]
   simp only [ne_eq, bijectionLinearParameters_apply_coe_Q', neg_mul,
     bijectionLinearParameters_apply_coe_Y, div_pow, bijectionLinearParameters_apply_coe_E']
   have hvw := S.hvw
@@ -350,7 +354,7 @@ lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val
   · simpa [hx] using cube_w_zero S h hx
 
 lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ S.v + S.w = -1 := by
-  erw [linearParameters.grav]
+  rw [bijection_coe_val, linearParameters.grav]
   have hvw := S.hvw
   have hQ := S.hx
   field_simp
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/Permutations.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/Permutations.lean
index f7db0cf7b..2f49357a7 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/Permutations.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/Permutations.lean
@@ -62,14 +62,13 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMCharges n).Charge
     intro S
     rw [charges_eq_toSpecies_eq]
     intro i
-    erw [toSMSpecies_toSpecies_inv]
-    rfl
+    exact toSMSpecies_toSpecies_inv _ _
 
 /-- The species charges of a set of charges acted on by a family permutation is the permutation
   of those species charges with the corresponding part of the family permutation. -/
 lemma repCharges_toSpecies (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
-    toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
-  erw [toSMSpecies_toSpecies_inv]
+    toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j :=
+  toSMSpecies_toSpecies_inv _ _
 
 /-- The sum over every charge in any species to some power `m` is invariant under the group
   action. -/
diff --git a/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean b/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
index b469f4dc1..4634194ec 100644
--- a/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
+++ b/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
@@ -236,8 +236,8 @@ lemma gaugeGroupI_smul_inner (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec)
       simp
       rfl
     _ = (ψ ⬝ᵥ star (φ.toFin2ℂ)) := by
-      erw [dotProduct_smul, smul_dotProduct, smul_smul, Unitary.star_mul_self]
-      simp
+      rw [dotProduct_smul, WithLp.ofLp_smul, smul_dotProduct, smul_smul, Unitary.star_mul_self,
+        one_smul]
 
 @[simp]
 lemma gaugeGroupI_smul_norm (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
diff --git a/Physlib/Particles/StandardModel/Representations.lean b/Physlib/Particles/StandardModel/Representations.lean
index 82d906e4f..d58482f5b 100644
--- a/Physlib/Particles/StandardModel/Representations.lean
+++ b/Physlib/Particles/StandardModel/Representations.lean
@@ -30,7 +30,7 @@ noncomputable def repU1Map (g : unitary ℂ) : unitaryGroup (Fin 2) ℂ :=
     simp only [SubmonoidClass.mk_pow, Submonoid.mk_smul, star_smul, star_pow, RCLike.star_def,
       star_one]
     rw [smul_smul, ← mul_pow]
-    erw [(Unitary.mem_iff.mp g.prop).2]
+    rw [← star_def, (Unitary.mem_iff.mp g.prop).2]
     simp only [one_pow, one_smul]⟩
 
 /-- The 2d representation of U(1) with charge 3 as a homomorphism
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean
index ca2ef553d..3752b7220 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean
@@ -144,7 +144,7 @@ def accGrav : MSSMCharges.Charges →ₗ[ℚ] ℚ where
     ring
   map_smul' a S := by
     repeat rw [(toSMSpecies _).map_smul]
-    erw [Hd.map_smul, Hu.map_smul]
+    simp_rw [Hd.map_smul, Hu.map_smul]
     simp only [MSSMSpecies_numberCharges, HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply,
       reduceMul, Hd_apply, Fin.reduceFinMk, Hu_apply, eq_ratCast, Rat.cast_eq_id, id_eq]
     repeat rw [Finset.sum_add_distrib]
@@ -158,11 +158,9 @@ lemma accGrav_ext {S T : MSSMCharges.Charges}
     accGrav S = accGrav T := by
   simp only [accGrav, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue,
     LinearMap.coe_mk, AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
-  rw [hd, hu]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 /-- The anomaly cancellation condition for SU(2) anomaly. -/
 @[simp]
@@ -172,15 +170,15 @@ def accSU2 : MSSMCharges.Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [MSSMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add,
       toSMSpecies_apply, reduceMul, Fin.isValue, mul_add, Hd_apply, Fin.reduceFinMk, Hu_apply]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     repeat rw [(toSMSpecies _).map_smul]
-    erw [Hd.map_smul, Hu.map_smul]
+    rw [Hd.map_smul, Hu.map_smul]
     simp only [MSSMSpecies_numberCharges, HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply,
       reduceMul, Hd_apply, Fin.reduceFinMk, Hu_apply, eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
     ring
 
@@ -191,11 +189,9 @@ lemma accSU2_ext {S T : MSSMCharges.Charges}
     accSU2 S = accSU2 T := by
   simp only [accSU2, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue,
     LinearMap.coe_mk, AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
-  rw [hd, hu]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 /-- The anomaly cancellation condition for SU(3) anomaly. -/
 @[simp]
@@ -205,14 +201,14 @@ def accSU3 : MSSMCharges.Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [MSSMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add,
       toSMSpecies_apply, reduceMul, Fin.isValue, mul_add]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     repeat rw [(toSMSpecies _).map_smul]
     simp only [MSSMSpecies_numberCharges, HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply,
       reduceMul, eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
     ring
 
@@ -222,10 +218,9 @@ lemma accSU3_ext {S T : MSSMCharges.Charges}
     accSU3 S = accSU3 T := by
   simp only [accSU3, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, LinearMap.coe_mk,
     AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 /-- The ACC for `Y²`. -/
 @[simp]
@@ -236,15 +231,15 @@ def accYY : MSSMCharges.Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [MSSMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add,
       toSMSpecies_apply, reduceMul, Fin.isValue, mul_add, Hd_apply, Fin.reduceFinMk, Hu_apply]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     repeat rw [(toSMSpecies _).map_smul]
-    erw [Hd.map_smul, Hu.map_smul]
+    rw [Hd.map_smul, Hu.map_smul]
     simp only [MSSMSpecies_numberCharges, HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply,
       reduceMul, Hd_apply, Fin.reduceFinMk, Hu_apply, eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     -- rw [show Rat.cast a = a from rfl]
     ring
 
@@ -255,11 +250,9 @@ lemma accYY_ext {S T : MSSMCharges.Charges}
     accYY S = accYY T := by
   simp only [accYY, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue,
     LinearMap.coe_mk, AddHom.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
-  rw [hd, hu]
-  rfl
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
+  simp_all
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The symmetric bilinear function used to define the quadratic ACC. -/
@@ -276,7 +269,7 @@ def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂
     · rw [Finset.mul_sum]
       apply Fintype.sum_congr
       intro i
-      repeat erw [map_smul]
+      repeat rw [map_smul]
       simp only [HSMul.hSMul, SMul.smul, toSMSpecies_apply, Fin.isValue, neg_mul, one_mul]
       ring
     · simp only [map_smul, Hd_apply, Fin.reduceFinMk, Fin.isValue, smul_eq_mul, neg_mul, Hu_apply]
@@ -292,7 +285,7 @@ def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂
     · rw [← Finset.sum_add_distrib]
       apply Fintype.sum_congr
       intro i
-      repeat erw [map_add]
+      repeat rw [map_add]
       simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSMSpecies_apply, Fin.isValue, neg_mul,
         one_mul]
       ring
@@ -320,10 +313,9 @@ lemma accQuad_ext {S T : (MSSMCharges).Charges}
     (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
     accQuad S = accQuad T := by
   simp only [HomogeneousQuadratic, accQuad, BiLinearSymm.toHomogeneousQuad_apply]
-  erw [← quadBiLin.toFun_eq_coe]
-  simp only [quadBiLin, BiLinearSymm.mk₂, AddHom.toFun_eq_coe, AddHom.coe_mk, LinearMap.coe_mk]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
+  simp only [quadBiLin, BiLinearSymm.mk₂_toFun_apply]
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
   ring_nf
   have h1 : ∀ j, ∑ i, (toSMSpecies j S i)^2 = ∑ i, (toSMSpecies j T i)^2 := fun j => h j
   repeat rw [h1]
@@ -350,7 +342,7 @@ lemma cubeTriLinToFun_map_smul₁ (a : ℚ) (S T R : MSSMCharges.Charges) :
   · rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
-    repeat erw [map_smul]
+    repeat rw [map_smul]
     simp only [HSMul.hSMul, SMul.smul, toSMSpecies_apply, Fin.isValue]
     ring
   · simp only [map_smul, Hd_apply, Fin.reduceFinMk, Fin.isValue, smul_eq_mul, Hu_apply]
@@ -368,7 +360,7 @@ lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
   · rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
     intro i
-    repeat erw [map_add]
+    repeat rw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSMSpecies_apply, Fin.isValue]
     ring
   · rw [Hd.map_add, Hu.map_add]
@@ -418,15 +410,10 @@ lemma accCube_ext {S T : MSSMCharges.Charges}
     accCube S = accCube T := by
   simp only [HomogeneousCubic, accCube, cubeTriLin, TriLinearSymm.toCubic_apply,
     TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun]
-  repeat erw [Finset.sum_add_distrib]
-  repeat erw [← Finset.mul_sum]
+  repeat rw [Finset.sum_add_distrib]
+  repeat rw [← Finset.mul_sum]
   ring_nf
-  have h1 : ∀ j, ∑ i, (toSMSpecies j S i)^3 = ∑ i, (toSMSpecies j T i)^3 := by
-    intro j
-    erw [h]
-    rfl
-  repeat rw [h1]
-  rw [hd, hu]
+  simp_all
 
 end MSSMACCs
 
@@ -452,6 +439,8 @@ def MSSMACC : ACCSystem where
 namespace MSSMACC
 open MSSMCharges
 
+lemma cubicACC_apply (S : MSSMACC.Charges) : MSSMACC.cubicACC S = cubeTriLin.toCubic S := rfl
+
 lemma quadSol (S : MSSMACC.QuadSols) : accQuad S.val = 0 := by
   have hS := S.quadSol
   simp only [MSSMACC_numberQuadratic, HomogeneousQuadratic, MSSMACC_quadraticACCs] at hS
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
index 3db5ad6fc..f8d8a0625 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
@@ -31,6 +31,9 @@ open BigOperators
 /-- The line through $Y_3$ and $B_3$ as `LinSols`. -/
 def lineY₃B₃Charges (a b : ℚ) : MSSMACC.LinSols := a • Y₃.1.1 + b • B₃.1.1
 
+lemma lineY₃B₃Charges_val (a b : ℚ) :
+    (lineY₃B₃Charges a b).val = a • Y₃.1.1.val + b • B₃.1.1.val := rfl
+
 set_option backward.isDefEq.respectTransparency false in
 lemma lineY₃B₃Charges_quad (a b : ℚ) : accQuad (lineY₃B₃Charges a b).val = 0 := by
   change accQuad (a • Y₃.val + b • B₃.val) = 0
@@ -39,7 +42,8 @@ lemma lineY₃B₃Charges_quad (a b : ℚ) : accQuad (lineY₃B₃Charges a b).v
   rw [quadBiLin.toHomogeneousQuad.map_smul]
   rw [quadBiLin.toHomogeneousQuad.map_smul]
   rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
-  erw [quadSol Y₃.1, quadSol B₃.1]
+  rw [← accQuad]
+  rw [quadSol Y₃.1, quadSol B₃.1]
   simp only [mul_zero, add_zero, zero_add, mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
   apply Or.inr ∘ Or.inr
   with_unfolding_all rfl
@@ -53,7 +57,8 @@ lemma lineY₃B₃Charges_cubic (a b : ℚ) : accCube (lineY₃B₃Charges a b).
   rw [cubeTriLin.toCubic.map_smul]
   rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
   rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
-  erw [Y₃.cubicSol, B₃.cubicSol]
+  repeat rw [← cubicACC_apply]
+  rw [Y₃.cubicSol, B₃.cubicSol]
   rw [show cubeTriLin Y₃.val Y₃.val B₃.val = 0 by with_unfolding_all rfl]
   rw [show cubeTriLin B₃.val B₃.val Y₃.val = 0 by with_unfolding_all rfl]
   simp
@@ -62,6 +67,9 @@ lemma lineY₃B₃Charges_cubic (a b : ℚ) : accCube (lineY₃B₃Charges a b).
 def lineY₃B₃ (a b : ℚ) : MSSMACC.Sols :=
   AnomalyFreeMk' (lineY₃B₃Charges a b) (lineY₃B₃Charges_quad a b) (lineY₃B₃Charges_cubic a b)
 
+lemma lineY₃B₃_val (a b : ℚ) : (lineY₃B₃ a b).val = a • Y₃.val + b • B₃.val := by
+  simp [lineY₃B₃, lineY₃B₃Charges_val]
+
 set_option backward.isDefEq.respectTransparency false in
 lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
     cubeTriLin Y₃.val B₃.val R.val = 0 := by
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
index 581601749..2c038fff9 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
@@ -98,7 +98,9 @@ lemma quad_self_proj (T : MSSMACC.Sols) :
   rw [proj_val]
   rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
   rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
-  erw [quadSol T.1]
+  rw [← quadBiLin.toHomogeneousQuad_apply]
+  rw [← accQuad]
+  rw [quadSol T.1]
   rw [quadBiLin.swap T.val Y₃.val, quadBiLin.swap T.val B₃.val]
   ring
 
@@ -145,7 +147,7 @@ lemma cube_proj_proj_B₃ (T : MSSMACC.LinSols) :
     (dot Y₃.val B₃.val)^2 * cubeTriLin T.val T.val B₃.val := by
   rw [proj_val]
   rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
-  erw [lineY₃B₃_doublePoint]
+  rw [← lineY₃B₃_val, lineY₃B₃_doublePoint, lineY₃B₃_val]
   rw [cubeTriLin.map_add₂, cubeTriLin.swap₂, cubeTriLin.map_add₁, cubeTriLin.map_smul₁,
     cubeTriLin.map_smul₃, doublePoint_Y₃_B₃]
   rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₃, cubeTriLin.swap₁, doublePoint_B₃_B₃]
@@ -164,12 +166,14 @@ lemma cube_proj_proj_self (T : MSSMACC.Sols) :
     (dot Y₃.val T.val - 2 * dot B₃.val T.val) * cubeTriLin T.val T.val B₃.val) := by
   rw [proj_val]
   rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
-  erw [lineY₃B₃_doublePoint]
+  rw [← lineY₃B₃_val, lineY₃B₃_doublePoint, lineY₃B₃_val]
   repeat rw [cubeTriLin.map_add₁]
   repeat rw [cubeTriLin.map_smul₁]
   repeat rw [cubeTriLin.map_add₂]
   repeat rw [cubeTriLin.map_smul₂]
-  erw [T.cubicSol]
+  rw [← cubeTriLin.toCubic_apply]
+  rw [← cubicACC_apply]
+  rw [T.cubicSol]
   rw [cubeTriLin.swap₁ Y₃.val T.val T.val, cubeTriLin.swap₂ T.val Y₃.val T.val]
   rw [cubeTriLin.swap₁ B₃.val T.val T.val, cubeTriLin.swap₂ T.val B₃.val T.val]
   ring
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
index bd8c390cf..61b768fc0 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
@@ -53,9 +53,9 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
   have h1 := congrArg (fun S => dot Y₃.val S) h
   have h2 := congrArg (fun S => dot B₃.val S) h
   simp only at h1 h2
-  erw [dot.map_add₂, dot.map_add₂] at h1 h2
-  erw [dot.map_add₂ Y₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h1
-  erw [dot.map_add₂ B₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h2
+  rw [dot.map_add₂, dot.map_add₂] at h1 h2
+  rw [dot.map_add₂ Y₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h1
+  rw [dot.map_add₂ B₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h2
   rw [dot.map_add₂] at h1 h2
   rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂] at h1 h2
   rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂] at h1 h2
@@ -97,7 +97,9 @@ lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
     + 2 * b * quadBiLin B₃.val R.val + c * quadBiLin R.val R.val) := by
   rw [planeY₃B₃_val]
   rw [accQuad, BiLinearSymm.toHomogeneousQuad_add]
-  erw [lineY₃B₃Charges_quad]
+  rw [← lineY₃B₃Charges_val, ← accQuad]
+  rw [lineY₃B₃Charges_quad]
+  rw [lineY₃B₃Charges_val, accQuad]
   rw [quadBiLin.toHomogeneousQuad.map_smul]
   rw [quadBiLin.map_add₁, quadBiLin.map_smul₁, quadBiLin.map_smul₁]
   rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂]
@@ -110,9 +112,12 @@ lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
     (3 * a * cubeTriLin R.val R.val Y₃.val
     + 3 * b * cubeTriLin R.val R.val B₃.val + c * cubeTriLin R.val R.val R.val) := by
   rw [planeY₃B₃_val]
-  rw [accCube, TriLinearSymm.toCubic_add]
-  erw [lineY₃B₃Charges_cubic]
-  erw [lineY₃B₃_doublePoint (c • R.1) a b]
+  rw [accCube, TriLinearSymm.toCubic_add, ← accCube]
+  rw [← lineY₃B₃Charges_val]
+  rw [lineY₃B₃Charges_cubic]
+  rw [TriLinearSymm.map_smul₃, lineY₃B₃Charges_val, ← lineY₃B₃_val]
+  rw [lineY₃B₃_doublePoint]
+  rw [lineY₃B₃_val, accCube]
   rw [cubeTriLin.toCubic.map_smul]
   rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
   rw [cubeTriLin.map_add₃, cubeTriLin.map_smul₃, cubeTriLin.map_smul₃]
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
index 74fabe423..fc7c406ac 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
@@ -287,7 +287,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
 /-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
 def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
   AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃)
-    (by erw [planeY₃B₃_quad, R.prop.1, R.prop.2.1, R.prop.2.2]; simp)
+    (by rw [lineCube, planeY₃B₃_quad, R.prop.1, R.prop.2.1, R.prop.2.2]; simp)
       (lineCube_cube R.val.val a₁ a₂ a₃)
 
 lemma inQuadToSol_smul (R : InQuad) (c₁ c₂ c₃ d : ℚ) :
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Permutations.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Permutations.lean
index 27335d0c5..d90d6d3c3 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Permutations.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Permutations.lean
@@ -53,8 +53,8 @@ def chargeMap (f : PermGroup) : MSSMCharges.Charges →ₗ[ℚ] MSSMCharges.Char
     rfl
 
 lemma chargeMap_toSpecies (f : PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) :
-    toSMSpecies j (chargeMap f S) = toSMSpecies j S ∘ f j := by
-  erw [toSMSpecies_toSpecies_inv]
+    toSMSpecies j (chargeMap f S) = toSMSpecies j S ∘ f j :=
+  toSMSpecies_toSpecies_inv _ _
 
 /-- The representation of `permGroup` acting on the vector space of charges. -/
 @[simp]
@@ -78,12 +78,11 @@ def repCharges : Representation ℚ PermGroup (MSSMCharges).Charges where
     rw [charges_eq_toSpecies_eq]
     refine And.intro ?_ $ Prod.mk_inj.mp rfl
     intro i
-    erw [toSMSpecies_toSpecies_inv]
-    rfl
+    exact toSMSpecies_toSpecies_inv _ _
 
 lemma repCharges_toSMSpecies (f : PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) :
-    toSMSpecies j (repCharges f S) = toSMSpecies j S ∘ f⁻¹ j := by
-  erw [toSMSpecies_toSpecies_inv]
+    toSMSpecies j (repCharges f S) = toSMSpecies j S ∘ f⁻¹ j :=
+  toSMSpecies_toSpecies_inv _ _
 
 lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) :
     ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j (repCharges f S)) i =