diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
index 2147ac2..07fa185 100644
--- a/HepLean/AnomalyCancellation/LinearMaps.lean
+++ b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -20,11 +20,9 @@ In particular a HomogeneousQuadratic should be a map `V →ₗ[ℚ] V →ₗ[ℚ
 -/
 
 /-- The structure defining a homogeneous quadratic equation. -/
-structure HomogeneousQuadratic (V : Type) [AddCommMonoid V] [Module ℚ V] where
-  /-- The quadratic equation. -/
-  toFun : V → ℚ
-  /-- The equation is homogeneous. -/
-  map_smul' : ∀ a S,  toFun (a • S) = a ^ 2 * toFun S
+@[simp]
+def HomogeneousQuadratic (V : Type) [AddCommMonoid V] [Module ℚ V] : Type :=
+  V →ₑ[((fun a => a ^ 2) : ℚ → ℚ)] ℚ
 
 namespace HomogeneousQuadratic
 
@@ -37,71 +35,15 @@ instance instFun : FunLike (HomogeneousQuadratic V) V ℚ where
     cases g
     simp_all
 
-/-- Given an equivariant function from `V` to `ℚ` we get a `HomogeneousQuadratic V`. -/
-def fromEquivariant (f : V →ₑ[((fun a => a ^ 2) : ℚ → ℚ)] ℚ) : HomogeneousQuadratic V where
-  toFun := f
-  map_smul' a S := by
-    rw [map_smulₛₗ]
-    rfl
-
 lemma map_smul (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a ^ 2 * f S :=
   f.map_smul' a S
 
 end HomogeneousQuadratic
 
-/-- The structure of a bilinear map. -/
-structure BiLinear (V : Type) [AddCommMonoid V] [Module ℚ V] where
-  /-- The underling function. -/
-  toFun : V × V → ℚ
-  map_smul₁' : ∀ a S T, toFun (a • S, T) = a * toFun (S, T)
-  map_smul₂' : ∀ a S T , toFun (S, a • T) = a * toFun (S, T)
-  map_add₁' : ∀ S1 S2 T, toFun (S1 + S2, T) = toFun (S1, T) + toFun (S2, T)
-  map_add₂' : ∀ S T1 T2, toFun (S, T1 + T2) = toFun (S, T1) + toFun (S, T2)
-
-namespace BiLinear
-
-variable {V : Type} [AddCommMonoid V] [Module ℚ V]
-
-instance instFun : FunLike (BiLinear V) (V × V) ℚ where
-  coe f := f.toFun
-  coe_injective' f g h := by
-    cases f
-    cases g
-    simp_all
-
-/-- A bilinear map from a linear function ` V →ₗ[ℚ] V →ₗ[ℚ] ℚ`. -/
-def fromLinearToHom (f : V →ₗ[ℚ] V →ₗ[ℚ] ℚ) : BiLinear V where
-  toFun S := f S.1 S.2
-  map_smul₁' a S T := by
-    simp only [LinearMapClass.map_smul]
-    rfl
-  map_smul₂' a S T := (f S).map_smul a T
-  map_add₁' S1 S2 T := by
-    simp only [f.map_add]
-    rfl
-  map_add₂' S T1 T2 := (f S).map_add T1 T2
-
-lemma map_smul₁ (f : BiLinear V) (a : ℚ) (S T : V) : f (a • S, T) = a * f (S, T) :=
-  f.map_smul₁' a S T
-
-lemma map_smul₂ (f : BiLinear V) (S : V) (a : ℚ) (T : V) : f (S, a • T) = a * f (S, T) :=
-  f.map_smul₂' a S T
-
-lemma map_add₁ (f : BiLinear V) (S1 S2 T : V) : f (S1 + S2, T) = f (S1, T) + f (S2, T) :=
-  f.map_add₁' S1 S2 T
-
-lemma map_add₂ (f : BiLinear V) (S : V) (T1 T2 : V) : f (S, T1 + T2) = f (S, T1) + f (S, T2) :=
-  f.map_add₂' S T1 T2
-
-end BiLinear
 
 /-- The structure of a symmetric bilinear function. -/
-structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] where
-  /-- The underlying function. -/
-  toFun : V × V → ℚ
-  map_smul₁' : ∀ a S T, toFun (a • S, T) = a * toFun (S, T)
-  map_add₁' : ∀ S1 S2 T, toFun (S1 + S2, T) = toFun (S1, T) + toFun (S2, T)
-  swap' : ∀ S T, toFun (S, T) = toFun (T, S)
+structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
+  swap' : ∀ S T, toFun S T = toFun T S
 
 /-- A symmetric bilinear function. -/
 class IsSymmetric {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V →ₗ[ℚ] V →ₗ[ℚ] ℚ) : Prop where
@@ -113,61 +55,79 @@ open BigOperators
 variable {V : Type} [AddCommMonoid V] [Module ℚ V]
 
 instance instFun (V : Type) [AddCommMonoid V] [Module ℚ V] :
-    FunLike (BiLinearSymm V) (V × V) ℚ where
+    FunLike (BiLinearSymm V) (V) (V →ₗ[ℚ] ℚ ) where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
     cases g
     simp_all
 
-/-- A bilinear symmetric function from a symemtric `V →ₗ[ℚ] V →ₗ[ℚ] ℚ`. -/
-def fromSymmToHom (f : V →ₗ[ℚ] V →ₗ[ℚ] ℚ) [IsSymmetric f] : BiLinearSymm V where
-  toFun S := f S.1 S.2
-  map_smul₁' a S T := by
-    simp only [LinearMapClass.map_smul]
-    rfl
-  map_add₁' S1 S2 T := by
-    simp only [f.map_add]
-    rfl
-  swap' S T := IsSymmetric.swap S T
+@[simps!]
+def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S, T))
+    (map_add : ∀ S1 S2 T, f (S1 + S2, T) = f (S1, T) + f (S2, T))
+    (swap : ∀ S T, f (S, T) = f (T, S)) : BiLinearSymm V where
+  toFun := fun S => {
+    toFun := fun T => f (S, T)
+    map_add' := by
+      intro T1 T2
+      simp
+      rw [swap, map_add]
+      rw [swap T1 S, swap T2 S]
+    map_smul' :=by
+      intro a T
+      simp
+      rw [swap, map_smul]
+      rw [swap T S]
+  }
+  map_smul' := by
+    intro a S
+    apply LinearMap.ext
+    intro T
+    exact map_smul a S T
+  map_add' := by
+    intro S1 S2
+    apply LinearMap.ext
+    intro T
+    exact map_add S1 S2 T
+  swap' := swap
 
-lemma toFun_eq_coe (f : BiLinearSymm V) : f.toFun = f := rfl
+lemma map_smul₁ (f : BiLinearSymm V) (a : ℚ) (S T : V) : f (a • S) T = a * f S T := by
+  erw [f.map_smul a S]
+  rfl
 
-lemma map_smul₁ (f : BiLinearSymm V) (a : ℚ) (S T : V) : f (a • S, T) = a * f (S, T) :=
-  f.map_smul₁' a S T
-
-lemma swap (f : BiLinearSymm V) (S T : V) : f (S, T) = f (T, S) :=
+lemma swap (f : BiLinearSymm V) (S T : V) : f S T = f T S :=
   f.swap' S T
 
-lemma map_smul₂ (f : BiLinearSymm V) (a : ℚ)  (S : V) (T : V) : f (S, a • T) = a * f (S, T) := by
+lemma map_smul₂ (f : BiLinearSymm V) (a : ℚ)  (S : V) (T : V) : f S (a • T) = a * f S T := by
   rw [f.swap, f.map_smul₁, f.swap]
 
-lemma map_add₁ (f : BiLinearSymm V) (S1 S2 T : V) : f (S1 + S2, T) = f (S1, T) + f (S2, T) :=
-  f.map_add₁' S1 S2 T
+lemma map_add₁ (f : BiLinearSymm V) (S1 S2 T : V) : f (S1 + S2) T = f S1 T + f S2 T := by
+  erw [f.map_add]
+  rfl
 
 lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
-    f (S, T1 + T2) = f (S, T1) + f (S, T2) := by
+    f S (T1 + T2) = f S T1 + f S T2 := by
   rw [f.swap, f.map_add₁, f.swap T1 S, f.swap T2 S]
 
 /-- Fixing the second input vectors, the resulting linear map. -/
 def toLinear₁  (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
-  toFun S := f (S, T)
+  toFun S := f S T
   map_add' S1 S2 := by
     simp only [f.map_add₁]
   map_smul' a S := by
     simp only [f.map_smul₁]
     rfl
 
-lemma toLinear₁_apply (f : BiLinearSymm V) (S T : V) : f (S, T) = f.toLinear₁ T S := rfl
+lemma toLinear₁_apply (f : BiLinearSymm V) (S T : V) : f S T = f.toLinear₁ T S := rfl
 
 lemma map_sum₁ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V)  :
-    f (∑ i, S i, T) = ∑ i, f (S i, T) := by
+    f (∑ i, S i) T = ∑ i, f (S i) T := by
   rw [f.toLinear₁_apply]
   rw [map_sum]
   rfl
 
 lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
-    f ( T, ∑ i, S i) = ∑ i, f (T, S i) := by
+    f T (∑ i, S i) = ∑ i, f T (S i) := by
   rw [swap, map_sum₁]
   apply Fintype.sum_congr
   intro i
@@ -178,28 +138,28 @@ lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
 @[simps!]
 def toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V]
     (τ : BiLinearSymm V) : HomogeneousQuadratic V where
-  toFun S := τ (S, S)
+  toFun S := τ S S
   map_smul' a S := by
     simp only
     rw [τ.map_smul₁, τ.map_smul₂]
-    ring
+    ring_nf
+    rfl
 
 lemma toHomogeneousQuad_add {V : Type} [AddCommMonoid V] [Module ℚ V]
     (τ : BiLinearSymm V) (S T : V) :
     τ.toHomogeneousQuad (S + T) = τ.toHomogeneousQuad S +
-    τ.toHomogeneousQuad T + 2 * τ (S, T) := by
-  simp only [toHomogeneousQuad_toFun]
-  rw [τ.map_add₁, τ.map_add₂, τ.map_add₂, τ.swap T S]
+    τ.toHomogeneousQuad T + 2 * τ S T := by
+  simp [toHomogeneousQuad_apply]
+  rw [τ.map_add₁, τ.map_add₁, τ.swap T S]
   ring
 
 
 end BiLinearSymm
 
 /-- The structure of a homogeneous cubic equation. -/
-structure HomogeneousCubic (V : Type) [AddCommMonoid V] [Module ℚ V] where
-  /-- The underlying function. -/
-  toFun : V → ℚ
-  map_smul' : ∀ a S, toFun (a • S) = a ^ 3 * toFun S
+@[simp]
+def HomogeneousCubic (V : Type) [AddCommMonoid V] [Module ℚ V] : Type :=
+  V →ₑ[((fun a => a ^ 3) : ℚ → ℚ)] ℚ
 
 namespace HomogeneousCubic
 
@@ -217,29 +177,6 @@ lemma map_smul (f : HomogeneousCubic V) (a : ℚ) (S : V) : f (a • S) = a ^ 3
 
 end HomogeneousCubic
 
-/-- The structure of a trilinear function. -/
-structure TriLinear (V : Type) [AddCommMonoid V] [Module ℚ V] where
-  /-- The underlying function. -/
-  toFun : V × V × V → ℚ
-  map_smul₁' : ∀ a S T L, toFun (a • S, T, L) = a * toFun (S, T, L)
-  map_smul₂' : ∀ a S T L, toFun (S, a • T, L) = a * toFun (S, T, L)
-  map_smul₃' : ∀ a S T L, toFun (S, T, a • L) = a * toFun (S, T, L)
-  map_add₁' : ∀ S1 S2 T L, toFun (S1 + S2, T, L) = toFun (S1, T, L) + toFun (S2, T, L)
-  map_add₂' : ∀ S T1 T2 L, toFun (S, T1 + T2, L) = toFun (S, T1, L) + toFun (S, T2, L)
-  map_add₃' : ∀ S T L1 L2, toFun (S, T, L1 + L2) = toFun (S, T, L1) + toFun (S, T, L2)
-
-namespace TriLinear
-
-variable {V : Type} [AddCommMonoid V] [Module ℚ V]
-
-instance instFun : FunLike (TriLinear V) (V × V × V) ℚ where
-  coe f := f.toFun
-  coe_injective' f g h := by
-    cases f
-    cases g
-    simp_all
-
-end TriLinear
 /-- The structure of a symmetric trilinear function. -/
 structure TriLinearSymm' (V : Type) [AddCommMonoid V] [Module ℚ V] extends
     V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
@@ -350,7 +287,7 @@ def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
     (τ : TriLinearSymm charges) : HomogeneousCubic charges where
   toFun S := τ (S, S, S)
   map_smul' a S := by
-    simp only
+    simp
     rw [τ.map_smul₁, τ.map_smul₂, τ.map_smul₃]
     ring
 
@@ -358,7 +295,7 @@ lemma toCubic_add {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
     (τ : TriLinearSymm charges) (S T : charges) :
     τ.toCubic (S + T) = τ.toCubic S +
     τ.toCubic T + 3 * τ (S, S, T) + 3 * τ (T, T, S) := by
-  simp only [toCubic_toFun]
+  simp only [HomogeneousCubic, toCubic_apply]
   rw [τ.map_add₁, τ.map_add₂, τ.map_add₂, τ.map_add₃, τ.map_add₃, τ.map_add₃, τ.map_add₃]
   rw [τ.swap₂ S T S, τ.swap₁ T S S, τ.swap₂ S T S, τ.swap₂ T S T, τ.swap₁ S T T, τ.swap₂ T S T]
   ring
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index 1e2fd5f..495faa5 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -270,13 +270,13 @@ lemma accYY_ext {S T : MSSMCharges.charges}
   rw [hd, hu]
   rfl
 
-/-- The symmetric bilinear form used to define the quadratic ACC. -/
 @[simps!]
-def quadBiLin  : BiLinearSymm MSSMCharges.charges where
-  toFun S := ∑ i, (Q S.1 i *  Q S.2 i + (- 2) * (U S.1 i *  U S.2 i) +
+def quadBiLin  : BiLinearSymm MSSMCharges.charges := BiLinearSymm.mk₂ (
+  fun S => ∑ i, (Q S.1 i *  Q S.2 i + (- 2) * (U S.1 i *  U S.2 i) +
     D S.1 i *  D S.2 i + (- 1) * (L S.1 i * L S.2 i)  + E S.1 i * E S.2 i) +
-    (- Hd S.1 * Hd S.2 + Hu S.1 * Hu S.2)
-  map_smul₁' a S T := by
+    (- Hd S.1 * Hd S.2 + Hu S.1 * Hu S.2))
+  (by
+    intro a S T
     simp only
     rw [mul_add]
     congr 1
@@ -287,8 +287,9 @@ def quadBiLin  : BiLinearSymm MSSMCharges.charges where
     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]
-    ring
-  map_add₁' S T R := by
+    ring)
+  (by
+    intro S T R
     simp only
     rw [add_assoc, ← add_assoc (-Hd S * Hd R + Hu S * Hu R) _ _]
     rw [add_comm (-Hd S * Hd R + Hu S * Hu R) _]
@@ -303,15 +304,17 @@ def quadBiLin  : BiLinearSymm MSSMCharges.charges where
       one_mul]
     ring
     rw [Hd.map_add, Hu.map_add]
-    ring
-  swap' S L := by
+    ring)
+  (by
+    intro S L
     simp only [MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, neg_mul, one_mul,
       Hd_apply, Fin.reduceFinMk, Hu_apply]
     congr 1
     rw [Fin.sum_univ_three, Fin.sum_univ_three]
     simp only [Fin.isValue]
     ring
-    ring
+    ring)
+
 
 /-- The quadratic ACC. -/
 @[simp]
@@ -323,10 +326,9 @@ lemma accQuad_ext {S T : (MSSMCharges).charges}
     ∑ i, ((fun a => a^2) ∘ toSMSpecies j T) i)
     (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
     accQuad S = accQuad T := by
-  simp only [accQuad, BiLinearSymm.toHomogeneousQuad_toFun]
+  simp only [HomogeneousQuadratic, accQuad, BiLinearSymm.toHomogeneousQuad_apply]
   erw [← quadBiLin.toFun_eq_coe]
-  rw [quadBiLin]
-  simp only
+  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]
   ring_nf
@@ -337,6 +339,7 @@ lemma accQuad_ext {S T : (MSSMCharges).charges}
   repeat rw [h1]
   rw [hd, hu]
 
+
 /-- The function underlying the symmetric trilinear form used to define the cubic ACC. -/
 @[simp]
 def cubeTriLinToFun
@@ -461,7 +464,7 @@ open MSSMCharges
 
 lemma quadSol  (S : MSSMACC.QuadSols) : accQuad S.val = 0 := by
   have hS := S.quadSol
-  simp  [MSSMACCs.accQuad, HomogeneousQuadratic.toFun] at hS
+  simp only [MSSMACC_numberQuadratic, HomogeneousQuadratic, MSSMACC_quadraticACCs] at hS
   exact hS 0
 
 /-- A solution from a charge satisfying the ACCs. -/
@@ -523,30 +526,33 @@ lemma AnomalyFreeMk''_val (S : MSSMACC.QuadSols)
 
 /-- The dot product on the vector space of charges. -/
 @[simps!]
-def dot  : BiLinearSymm MSSMCharges.charges where
-  toFun S := ∑ i, (Q S.1 i *  Q S.2 i +  U S.1 i *  U S.2 i +
+def dot  : BiLinearSymm MSSMCharges.charges := BiLinearSymm.mk₂
+  (fun S => ∑ i, (Q S.1 i *  Q S.2 i +  U S.1 i *  U S.2 i +
     D S.1 i *  D S.2 i + L S.1 i * L S.2 i  + E S.1 i * E S.2 i
-    + N S.1 i * N S.2 i) + Hd S.1 * Hd S.2 + Hu S.1 * Hu S.2
-  map_smul₁' a S T := by
+    + N S.1 i * N S.2 i) + Hd S.1 * Hd S.2 + Hu S.1 * Hu S.2)
+  (by
+    intro a S T
     simp only [MSSMSpecies_numberCharges]
     repeat rw [(toSMSpecies _).map_smul]
     rw [Hd.map_smul, Hu.map_smul]
     rw [Fin.sum_univ_three, Fin.sum_univ_three]
     simp only [HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply, Hd_apply, Fin.reduceFinMk,
       Hu_apply]
-    ring
-  map_add₁' S T R := by
+    ring)
+  (by
+    intro S1 S2 T
     simp only [MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue,
       ACCSystemCharges.chargesAddCommMonoid_add, map_add, Hd_apply, Fin.reduceFinMk, Hu_apply]
     repeat erw [AddHom.map_add]
     rw [Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
     simp only [Fin.isValue]
-    ring
-  swap' S L := by
+    ring)
+  (by
+    intro S T
     simp only [MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, Hd_apply, Fin.reduceFinMk,
       Hu_apply]
     rw [Fin.sum_univ_three, Fin.sum_univ_three]
     simp only [Fin.isValue]
-    ring
+    ring)
 
 end MSSMACC
diff --git a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
index 0db4fb7..c77df0f 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
@@ -40,7 +40,7 @@ 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 only [mul_zero, add_zero, quadBiLin_toFun, Fin.isValue, Fin.reduceFinMk, zero_add,
+  simp only [mul_zero, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add,
     mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
   apply Or.inr ∘ Or.inr
   rfl
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
index 99c551b..cd3a157 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
@@ -29,42 +29,42 @@ open BigOperators
 
 /-- The type of linear solutions orthogonal to $Y_3$ and $B_3$. -/
 structure AnomalyFreePerp extends MSSMACC.LinSols where
-  perpY₃ : dot (Y₃.val, val) = 0
-  perpB₃ : dot (B₃.val, val) = 0
+  perpY₃ : dot Y₃.val val = 0
+  perpB₃ : dot B₃.val val = 0
 
 /-- The projection of an object in `MSSMACC.AnomalyFreeLinear` onto the subspace
   orthgonal to `Y₃` and`B₃`. -/
 def proj (T : MSSMACC.LinSols) : MSSMACC.AnomalyFreePerp :=
-  ⟨(dot (B₃.val, T.val) - dot (Y₃.val, T.val)) • Y₃.1.1
-  + (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) • B₃.1.1
-  + dot (Y₃.val, B₃.val) • T,
+  ⟨(dot B₃.val T.val - dot Y₃.val T.val) • Y₃.1.1
+  + (dot Y₃.val T.val - 2 * dot B₃.val T.val) • B₃.1.1
+  + dot Y₃.val B₃.val • T,
   by
-    change dot (_, _ • Y₃.val + _ • B₃.val + _ • T.val) = 0
+    change dot _ (_ • Y₃.val + _ • B₃.val + _ • T.val) = 0
     rw [dot.map_add₂, dot.map_add₂]
     rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂]
-    rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
-    rw [show dot (Y₃.val, Y₃.val) = 216 by rfl]
+    rw [show dot Y₃.val B₃.val = 108 by rfl]
+    rw [show dot Y₃.val Y₃.val = 216 by rfl]
     ring,
   by
-    change dot (_, _ • Y₃.val + _ • B₃.val + _ • T.val) = 0
+    change dot _ (_ • Y₃.val + _ • B₃.val + _ • T.val) = 0
     rw [dot.map_add₂, dot.map_add₂]
     rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂]
-    rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
-    rw [show dot (B₃.val, Y₃.val) = 108 by rfl]
-    rw [show dot (B₃.val, B₃.val) = 108 by rfl]
+    rw [show dot Y₃.val B₃.val = 108 by rfl]
+    rw [show dot B₃.val Y₃.val = 108 by rfl]
+    rw [show dot B₃.val B₃.val = 108 by rfl]
     ring⟩
 
 lemma proj_val (T : MSSMACC.LinSols) :
-    (proj T).val = (dot (B₃.val, T.val) - dot (Y₃.val, T.val)) • Y₃.val +
-    ( (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val))) • B₃.val +
-    dot (Y₃.val, B₃.val) • T.val := by
+    (proj T).val = (dot B₃.val T.val - dot Y₃.val T.val) • Y₃.val +
+    ( (dot Y₃.val T.val - 2 * dot B₃.val T.val)) • B₃.val +
+    dot Y₃.val B₃.val • T.val := by
   rfl
 
 lemma Y₃_plus_B₃_plus_proj (T : MSSMACC.LinSols) (a b c : ℚ) :
     a • Y₃.val + b • B₃.val + c • (proj T).val =
-    (a + c * (dot (B₃.val, T.val) - dot (Y₃.val, T.val))) • Y₃.val
-    + (b + c * (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val))) • B₃.val
-    + (dot (Y₃.val, B₃.val) * c) • T.val:= by
+    (a + c * (dot B₃.val T.val - dot Y₃.val T.val)) • Y₃.val
+    + (b + c * (dot Y₃.val T.val - 2 * dot B₃.val T.val)) • B₃.val
+    + (dot Y₃.val B₃.val * c) • T.val:= by
   rw [proj_val]
   rw [DistribMulAction.smul_add, DistribMulAction.smul_add]
   rw [add_assoc (_ • _ • Y₃.val), ← add_assoc (_ • Y₃.val + _ • B₃.val), add_assoc (_ • Y₃.val)]
@@ -81,27 +81,27 @@ lemma Y₃_plus_B₃_plus_proj (T : MSSMACC.LinSols) (a b c : ℚ) :
 
 
 lemma quad_Y₃_proj (T : MSSMACC.LinSols) :
-    quadBiLin (Y₃.val, (proj T).val) = dot (Y₃.val, B₃.val) * quadBiLin (Y₃.val, T.val) := by
+    quadBiLin Y₃.val (proj T).val = dot Y₃.val B₃.val * quadBiLin Y₃.val T.val := by
   rw [proj_val]
   rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
   rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
-  rw [show quadBiLin (Y₃.val, B₃.val) = 0 by rfl]
-  rw [show quadBiLin (Y₃.val, Y₃.val) = 0 by rfl]
+  rw [show quadBiLin Y₃.val B₃.val = 0 by rfl]
+  rw [show quadBiLin Y₃.val Y₃.val = 0 by rfl]
   ring
 
 lemma quad_B₃_proj (T : MSSMACC.LinSols) :
-    quadBiLin (B₃.val, (proj T).val) = dot (Y₃.val, B₃.val) * quadBiLin (B₃.val, T.val) := by
+    quadBiLin B₃.val (proj T).val = dot Y₃.val B₃.val * quadBiLin B₃.val T.val := by
   rw [proj_val]
   rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
   rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
-  rw [show quadBiLin (B₃.val, Y₃.val) = 0 by rfl]
-  rw [show quadBiLin (B₃.val, B₃.val) = 0 by rfl]
+  rw [show quadBiLin B₃.val Y₃.val = 0 by rfl]
+  rw [show quadBiLin B₃.val B₃.val = 0 by rfl]
   ring
 
 lemma quad_self_proj (T : MSSMACC.Sols) :
-    quadBiLin (T.val, (proj T.1.1).val) =
-    (dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * quadBiLin (Y₃.val, T.val) +
-    (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) * quadBiLin (B₃.val, T.val) := by
+    quadBiLin T.val (proj T.1.1).val =
+    (dot B₃.val T.val - dot Y₃.val T.val) * quadBiLin Y₃.val T.val +
+    (dot Y₃.val T.val - 2 * dot B₃.val T.val) * quadBiLin B₃.val T.val := by
   rw [proj_val]
   rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
   rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
@@ -110,9 +110,9 @@ lemma quad_self_proj (T : MSSMACC.Sols) :
   ring
 
 lemma quad_proj (T : MSSMACC.Sols) :
-    quadBiLin ((proj T.1.1).val, (proj T.1.1).val) = 2 * (dot (Y₃.val, B₃.val)) *
-     ((dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * quadBiLin (Y₃.val, T.val) +
-   (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) * quadBiLin (B₃.val, T.val) ) := by
+    quadBiLin (proj T.1.1).val (proj T.1.1).val = 2 * dot Y₃.val B₃.val *
+     ((dot B₃.val T.val - dot Y₃.val T.val) * quadBiLin Y₃.val T.val +
+   (dot Y₃.val T.val - 2 * dot B₃.val T.val) * quadBiLin B₃.val T.val ) := by
   nth_rewrite 1 [proj_val]
   repeat rw [quadBiLin.map_add₁]
   repeat rw [quadBiLin.map_smul₁]
@@ -122,7 +122,7 @@ lemma quad_proj (T : MSSMACC.Sols) :
 
 lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
     cubeTriLin ((proj T).val, (proj T).val, Y₃.val) =
-    (dot (Y₃.val, B₃.val))^2 * cubeTriLin (T.val, T.val, Y₃.val):= by
+    (dot Y₃.val B₃.val)^2 * cubeTriLin (T.val, T.val, Y₃.val) := by
   rw [proj_val]
   rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
   erw [lineY₃B₃_doublePoint]
@@ -144,7 +144,7 @@ lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
 
 lemma cube_proj_proj_B₃ (T : MSSMACC.LinSols) :
     cubeTriLin ((proj T).val, (proj T).val, B₃.val) =
-    (dot (Y₃.val, B₃.val))^2 * cubeTriLin (T.val, T.val, B₃.val):= by
+    (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]
@@ -160,9 +160,9 @@ lemma cube_proj_proj_B₃ (T : MSSMACC.LinSols) :
 
 lemma cube_proj_proj_self (T : MSSMACC.Sols) :
     cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, T.val) =
-    2 * dot (Y₃.val, B₃.val) *
-    ((dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * cubeTriLin (T.val, T.val, Y₃.val)  +
-    ( dot (Y₃.val, T.val)- 2 * dot (B₃.val, T.val)) * cubeTriLin (T.val, T.val, B₃.val)) := by
+    2 * dot Y₃.val B₃.val *
+    ((dot B₃.val T.val - dot Y₃.val T.val) * cubeTriLin (T.val, T.val, Y₃.val)  +
+    ( 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]
@@ -177,9 +177,9 @@ lemma cube_proj_proj_self (T : MSSMACC.Sols) :
 
 lemma cube_proj (T : MSSMACC.Sols) :
     cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, (proj T.1.1).val) =
-    3 *  dot (Y₃.val, B₃.val) ^ 2 *
-    ((dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * cubeTriLin (T.val, T.val, Y₃.val) +
-        (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) * cubeTriLin (T.val, T.val, B₃.val)) := by
+    3 *  dot Y₃.val B₃.val ^ 2 *
+    ((dot B₃.val T.val - dot Y₃.val T.val) * cubeTriLin (T.val, T.val, Y₃.val) +
+        (dot Y₃.val T.val - 2 * dot B₃.val T.val) * cubeTriLin (T.val, T.val, B₃.val)) := by
   nth_rewrite 3 [proj_val]
   repeat rw [cubeTriLin.map_add₃]
   repeat rw [cubeTriLin.map_smul₃]
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
index 22eedbd..66326fb 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@@ -53,8 +53,8 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
     (h : (planeY₃B₃ R a b c).val = (planeY₃B₃ R a' b' c').val) :
      a = a' ∧ b = b' ∧ c = c' := by
   rw [planeY₃B₃_val, planeY₃B₃_val] at h
-  have h1 := congrArg (fun S => dot (Y₃.val, S)) h
-  have h2 := congrArg (fun S => dot (B₃.val, S)) h
+  have h1 := congrArg (fun S => dot Y₃.val S) h
+  have h2 := congrArg (fun S => dot B₃.val S) h
   simp only [ Fin.isValue, ACCSystemCharges.chargesAddCommMonoid_add, Fin.reduceFinMk] 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
@@ -64,10 +64,10 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
   rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂] at h1 h2
   rw [R.perpY₃] at h1
   rw [R.perpB₃] at h2
-  rw [show dot (Y₃.val, Y₃.val) = 216 by rfl] at h1
-  rw [show dot (B₃.val, B₃.val) = 108 by rfl] at h2
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h1
-  rw [show dot (B₃.val, Y₃.val) = 108 by rfl] at h2
+  rw [show dot Y₃.val Y₃.val = 216 by rfl] at h1
+  rw [show dot B₃.val B₃.val = 108 by rfl] at h2
+  rw [show dot Y₃.val B₃.val = 108 by rfl] at h1
+  rw [show dot B₃.val Y₃.val = 108 by rfl] at h2
   simp_all
   have ha : a = a' := by
     linear_combination h1 / 108 + -1 * h2 / 108
@@ -102,15 +102,15 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
 
 
 lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
-    accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin (Y₃.val, R.val)
-    + 2 * b * quadBiLin (B₃.val, R.val) + c * quadBiLin (R.val, R.val)) := by
+    accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin Y₃.val R.val
+    + 2 * b * quadBiLin B₃.val R.val + c * quadBiLin R.val R.val) := by
   rw [planeY₃B₃_val]
   erw [BiLinearSymm.toHomogeneousQuad_add]
   erw [lineY₃B₃Charges_quad]
   rw [quadBiLin.toHomogeneousQuad.map_smul]
   rw [quadBiLin.map_add₁, quadBiLin.map_smul₁, quadBiLin.map_smul₁]
   rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂]
-  rw [show (BiLinearSymm.toHomogeneousQuad quadBiLin) R.val = quadBiLin (R.val, R.val) by rfl]
+  rw [show (BiLinearSymm.toHomogeneousQuad quadBiLin) R.val = quadBiLin R.val R.val by rfl]
   ring
 
 lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
@@ -130,9 +130,9 @@ lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
 /-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic,
 as `LinSols`. -/
 def lineQuadAFL (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.LinSols :=
-  planeY₃B₃ R (c2 * quadBiLin (R.val, R.val) - 2 * c3 * quadBiLin (B₃.val, R.val))
-  (2 * c3 * quadBiLin (Y₃.val, R.val) - c1 * quadBiLin (R.val, R.val))
-  (2 * c1 * quadBiLin (B₃.val, R.val) - 2 * c2 * quadBiLin (Y₃.val, R.val))
+  planeY₃B₃ R (c2 * quadBiLin R.val R.val - 2 * c3 * quadBiLin B₃.val R.val)
+  (2 * c3 * quadBiLin Y₃.val R.val - c1 * quadBiLin R.val R.val)
+  (2 * c1 * quadBiLin B₃.val R.val - 2 * c2 * quadBiLin Y₃.val R.val)
 
 lemma lineQuadAFL_quad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
     accQuad (lineQuadAFL R c1 c2 c3).val = 0 := by
@@ -146,10 +146,10 @@ def lineQuad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.QuadSols :
   AnomalyFreeQuadMk' (lineQuadAFL R c1 c2 c3) (lineQuadAFL_quad R c1 c2 c3)
 
 lemma lineQuad_val (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
-    (lineQuad R c1 c2 c3).val = (planeY₃B₃ R
-    (c2 * quadBiLin (R.val, R.val) - 2 * c3 * quadBiLin (B₃.val, R.val))
-    (2 * c3 * quadBiLin (Y₃.val, R.val) - c1 * quadBiLin (R.val, R.val))
-    (2 * c1 * quadBiLin (B₃.val, R.val) - 2 * c2 * quadBiLin (Y₃.val, R.val))).val  := by
+  (lineQuad R c1 c2 c3).val = (planeY₃B₃ R
+  (c2 * quadBiLin R.val R.val - 2 * c3 * quadBiLin B₃.val R.val)
+  (2 * c3 * quadBiLin Y₃.val R.val - c1 * quadBiLin R.val R.val)
+  (2 * c1 * quadBiLin B₃.val R.val - 2 * c2 * quadBiLin Y₃.val R.val)).val  := by
   rfl
 
 lemma lineQuad_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
@@ -163,26 +163,26 @@ lemma lineQuad_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
 
 /-- A helper function to simplify following expressions. -/
 def α₁ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
-  (3 * cubeTriLin (T.val, T.val, B₃.val) * quadBiLin (T.val, T.val) -
-   2 * cubeTriLin (T.val, T.val, T.val) * quadBiLin (B₃.val, T.val))
+  (3 * cubeTriLin (T.val, T.val, B₃.val) * quadBiLin T.val T.val -
+    2 * cubeTriLin (T.val, T.val, T.val) * quadBiLin B₃.val T.val)
 
-/-- A helper function to simplify following expressions. -/
-def α₂ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
-  (2 * cubeTriLin (T.val, T.val, T.val) * quadBiLin (Y₃.val, T.val) -
-  3 * cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin (T.val, T.val))
+  /-- A helper function to simplify following expressions. -/
+  def α₂ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
+    (2 * cubeTriLin (T.val, T.val, T.val) * quadBiLin Y₃.val T.val -
+    3 * cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin T.val T.val)
 
-/-- A helper function to simplify following expressions. -/
-def α₃ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
-  6 * ((cubeTriLin (T.val, T.val, Y₃.val)) * quadBiLin (B₃.val, T.val) -
-      (cubeTriLin (T.val, T.val, B₃.val)) * quadBiLin (Y₃.val, T.val))
+  /-- A helper function to simplify following expressions. -/
+  def α₃ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
+    6 * ((cubeTriLin (T.val, T.val, Y₃.val)) * quadBiLin B₃.val T.val -
+        (cubeTriLin (T.val, T.val, B₃.val)) * quadBiLin Y₃.val T.val)
 
-lemma lineQuad_cube (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ : ℚ) :
-    accCube (lineQuad R c₁ c₂ c₃).val =
-    - 4 * ( c₁ * quadBiLin (B₃.val, R.val) - c₂ * quadBiLin (Y₃.val, R.val)) ^ 2 *
-    ( α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃ ) := by
-  rw [lineQuad_val]
-  rw [planeY₃B₃_cubic, α₁, α₂, α₃]
-  ring
+  lemma lineQuad_cube (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ : ℚ) :
+      accCube (lineQuad R c₁ c₂ c₃).val =
+      - 4 * ( c₁ * quadBiLin B₃.val R.val - c₂ * quadBiLin Y₃.val R.val) ^ 2 *
+      ( α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃ ) := by
+    rw [lineQuad_val]
+    rw [planeY₃B₃_cubic, α₁, α₂, α₃]
+    ring
 
 /-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the cubic. -/
 def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
@@ -220,21 +220,21 @@ lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
 section proj
 
 lemma α₃_proj  (T : MSSMACC.Sols) : α₃ (proj T.1.1) =
-    6 * dot (Y₃.val, B₃.val) ^ 3 * (
-    cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin (B₃.val, T.val) -
-    cubeTriLin (T.val, T.val, B₃.val) * quadBiLin (Y₃.val, T.val)) := by
+    6 * dot Y₃.val B₃.val ^ 3 * (
+    cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin B₃.val T.val -
+    cubeTriLin (T.val, T.val, B₃.val) * quadBiLin Y₃.val T.val) := by
   rw [α₃]
   rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, quad_B₃_proj, quad_Y₃_proj]
   ring
 
 lemma α₂_proj (T : MSSMACC.Sols) : α₂ (proj T.1.1) =
-    - α₃ (proj T.1.1) * (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val))   := by
+    - α₃ (proj T.1.1) * (dot Y₃.val T.val - 2 * dot B₃.val T.val)   := by
   rw [α₃_proj, α₂]
   rw [cube_proj_proj_Y₃, quad_Y₃_proj, quad_proj, cube_proj]
   ring
 
 lemma α₁_proj (T : MSSMACC.Sols) : α₁ (proj T.1.1) =
-    - α₃ (proj T.1.1) * (dot (B₃.val, T.val) - dot (Y₃.val, T.val))   := by
+    - α₃ (proj T.1.1) * (dot B₃.val T.val - dot Y₃.val T.val)   := by
   rw [α₃_proj, α₁]
   rw [cube_proj_proj_B₃, quad_B₃_proj, quad_proj, cube_proj]
   ring
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 53c35b0..619cd61 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -46,12 +46,12 @@ instance (R : MSSMACC.AnomalyFreePerp) : Decidable (lineEqProp R) := by
 /-- A condition on `Sols` which we will show in `linEqPropSol_iff_proj_linEqProp` that is equivalent
  to the condition that the `proj` of the solution satisfies `lineEqProp`. -/
 def lineEqPropSol (R : MSSMACC.Sols) : Prop :=
-  cubeTriLin (R.val, R.val, Y₃.val) * quadBiLin (B₃.val, R.val) -
-  cubeTriLin (R.val, R.val, B₃.val) * quadBiLin (Y₃.val, R.val) = 0
+  cubeTriLin (R.val, R.val, Y₃.val) * quadBiLin B₃.val R.val -
+  cubeTriLin (R.val, R.val, B₃.val) * quadBiLin Y₃.val R.val = 0
 
 /-- A rational which appears in `toSolNS` acting on sols, and which been zero is
 equivalent to satisfying `lineEqPropSol`. -/
-def lineEqCoeff (T : MSSMACC.Sols) : ℚ := dot (Y₃.val, B₃.val) * α₃ (proj T.1.1)
+def lineEqCoeff (T : MSSMACC.Sols) : ℚ := dot Y₃.val B₃.val * α₃ (proj T.1.1)
 
 lemma lineEqPropSol_iff_lineEqCoeff_zero (T : MSSMACC.Sols) :
     lineEqPropSol T ↔ lineEqCoeff T = 0 := by
@@ -59,7 +59,7 @@ lemma lineEqPropSol_iff_lineEqCoeff_zero (T : MSSMACC.Sols) :
   simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero,
     false_or]
   rw [cube_proj_proj_B₃, cube_proj_proj_Y₃, quad_B₃_proj, quad_Y₃_proj]
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
+  rw [show dot Y₃.val B₃.val = 108 by rfl]
   simp only [Fin.isValue, Fin.reduceFinMk, OfNat.ofNat_ne_zero, false_or]
   ring_nf
   rw [mul_comm _ 1259712, mul_comm _ 1259712, ← mul_sub]
@@ -70,10 +70,10 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) :
   rw [lineEqPropSol_iff_lineEqCoeff_zero, lineEqCoeff, lineEqProp]
   apply Iff.intro
   intro h
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h
+  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
   simp at h
   rw [α₁_proj, α₂_proj, h]
-  simp only [neg_zero, dot_toFun, Fin.isValue, Fin.reduceFinMk, zero_mul, and_self]
+  simp only [neg_zero, Fin.isValue, Fin.reduceFinMk, zero_mul, and_self]
   intro h
   rw [h.2.2]
   simp
@@ -82,7 +82,7 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) :
 /-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
 entirely in the quadratic surface. -/
 def inQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
-    quadBiLin (R.val, R.val) = 0 ∧ quadBiLin (Y₃.val, R.val) = 0 ∧ quadBiLin (B₃.val, R.val) = 0
+    quadBiLin R.val R.val = 0 ∧ quadBiLin Y₃.val R.val = 0 ∧ quadBiLin B₃.val R.val = 0
 
 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (inQuadProp R) := by
   apply And.decidable
@@ -90,23 +90,23 @@ instance (R : MSSMACC.AnomalyFreePerp) : Decidable (inQuadProp R) := by
 /-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃`
 lies entirely in the quadratic surface. -/
 def inQuadSolProp (R : MSSMACC.Sols) : Prop :=
-    quadBiLin (Y₃.val, R.val) = 0 ∧ quadBiLin (B₃.val, R.val) = 0
+    quadBiLin Y₃.val R.val = 0 ∧ quadBiLin B₃.val R.val = 0
 
 /-- A rational which has two properties. It is zero for a solution `T` if and only if
 that solution satisfies `inQuadSolProp`. It appears in the definition of `inQuadProj`. -/
 def quadCoeff (T : MSSMACC.Sols) : ℚ :=
-    2 * dot (Y₃.val, B₃.val) ^ 2 *
-    (quadBiLin (Y₃.val, T.val) ^ 2 + quadBiLin (B₃.val, T.val) ^ 2)
+    2 * dot Y₃.val B₃.val ^ 2 *
+    (quadBiLin Y₃.val T.val ^ 2 + quadBiLin B₃.val T.val ^ 2)
 
 lemma inQuadSolProp_iff_quadCoeff_zero (T : MSSMACC.Sols) : inQuadSolProp T ↔ quadCoeff T = 0 := by
   apply Iff.intro
   intro h
   rw [quadCoeff, h.1, h.2]
-  simp only [dot_toFun, Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+  simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
     zero_pow, add_zero, mul_zero]
   intro h
   rw [quadCoeff] at h
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h
+  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
   simp only [ Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
     not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
   apply (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp at h
@@ -123,10 +123,10 @@ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) :
   apply Iff.intro
   intro h
   rw [h.1, h.2]
-  simp only [dot_toFun, Fin.isValue, Fin.reduceFinMk, mul_zero, add_zero, and_self]
+  simp only [Fin.isValue, Fin.reduceFinMk, mul_zero, add_zero, and_self]
   intro h
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h
-  simp only [dot_toFun, Fin.isValue, Fin.reduceFinMk , mul_eq_zero,
+  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
+  simp only [Fin.isValue, Fin.reduceFinMk , mul_eq_zero,
     OfNat.ofNat_ne_zero, or_self, false_or] at h
   rw [h.2.1, h.2.2]
   simp
@@ -149,7 +149,7 @@ def inCubeSolProp (R : MSSMACC.Sols) : Prop :=
 /-- A rational which has two properties. It is zero for a solution `T` if and only if
 that solution satisfies `inCubeSolProp`. It appears in the definition of `inLineEqProj`. -/
 def cubicCoeff (T : MSSMACC.Sols) : ℚ :=
-    3 * dot (Y₃.val, B₃.val) ^ 3 * (cubeTriLin (T.val, T.val, Y₃.val) ^ 2  +
+    3 * (dot Y₃.val B₃.val) ^ 3 * (cubeTriLin (T.val, T.val, Y₃.val) ^ 2  +
     cubeTriLin (T.val, T.val, B₃.val) ^ 2 )
 
 lemma inCubeSolProp_iff_cubicCoeff_zero (T : MSSMACC.Sols) :
@@ -157,11 +157,11 @@ lemma inCubeSolProp_iff_cubicCoeff_zero (T : MSSMACC.Sols) :
   apply Iff.intro
   intro h
   rw [cubicCoeff, h.1, h.2]
-  simp only [dot_toFun, Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+  simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
     zero_pow, add_zero, mul_zero]
   intro h
   rw [cubicCoeff] at h
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h
+  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
   simp only [ Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
     not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
   apply (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp at h
@@ -176,10 +176,10 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) :
   apply Iff.intro
   intro h
   rw [h.1, h.2]
-  simp only [dot_toFun, Fin.isValue, Fin.reduceFinMk, mul_zero, add_zero, and_self]
+  simp only [Fin.isValue, Fin.reduceFinMk, mul_zero, add_zero, and_self]
   intro h
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h
-  simp only [dot_toFun, Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
+  rw [show dot Y₃.val B₃.val = 108 by rfl] at h
+  simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
     not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
   rw [h.2.1, h.2.2]
   simp
@@ -254,7 +254,7 @@ lemma toSolNS_proj (T : notInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
   rw [α₁_proj, α₂_proj]
   ring_nf
   simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add]
-  have h1 : α₃ (proj T.val.toLinSols) * dot (Y₃.val, B₃.val) = lineEqCoeff T.val := by
+  have h1 : α₃ (proj T.val.toLinSols) * dot Y₃.val B₃.val = lineEqCoeff T.val := by
     rw [lineEqCoeff]
     ring
   rw [h1]
@@ -273,12 +273,11 @@ def inLineEqToSol : inLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c
 /-- On elements of `inLineEqSol` a right-inverse to `inLineEqSol`. -/
 def inLineEqProj (T : inLineEqSol) : inLineEq × ℚ × ℚ × ℚ :=
   (⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,
-  (quadCoeff T.val)⁻¹ * quadBiLin (B₃.val, T.val.val),
-  (quadCoeff T.val)⁻¹ * (- quadBiLin (Y₃.val, T.val.val)),
+  (quadCoeff T.val)⁻¹ * quadBiLin B₃.val T.val.val,
+  (quadCoeff T.val)⁻¹ * (- quadBiLin Y₃.val T.val.val),
   (quadCoeff T.val)⁻¹ * (
-  quadBiLin (B₃.val, T.val.val) * (dot (B₃.val, T.val.val) - dot (Y₃.val, T.val.val))
-  - quadBiLin (Y₃.val, T.val.val) * (dot (Y₃.val, T.val.val) - 2 * dot (B₃.val, T.val.val))))
-
+  quadBiLin B₃.val T.val.val * (dot B₃.val T.val.val - dot Y₃.val T.val.val)
+  - quadBiLin Y₃.val T.val.val * (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val)))
 
 lemma inLineEqTo_smul (R : inLineEq) (c₁ c₂ c₃ d : ℚ) :
     inLineEqToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inLineEqToSol (R, c₁, c₂, c₃) := by
@@ -297,8 +296,8 @@ lemma inLineEqToSol_proj (T : inLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
   rw [quad_proj, quad_Y₃_proj, quad_B₃_proj]
   ring_nf
   simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add]
-  have h1 : (quadBiLin (Y₃.val, (T).val.val) ^ 2 * dot (Y₃.val, B₃.val) ^ 2 * 2 +
-      dot (Y₃.val, B₃.val) ^ 2 * quadBiLin (B₃.val, (T).val.val) ^ 2 * 2) = quadCoeff T.val := by
+  have h1 : (quadBiLin Y₃.val T.val.val ^ 2 * dot Y₃.val B₃.val ^ 2 * 2 +
+      dot Y₃.val B₃.val ^ 2 * quadBiLin B₃.val T.val.val ^ 2 * 2) = quadCoeff T.val := by
     rw [quadCoeff]
     ring
   rw [h1]
@@ -329,9 +328,9 @@ def inQuadProj (T : inQuadSol) : inQuad × ℚ × ℚ × ℚ :=
   (cubicCoeff T.val)⁻¹ * (cubeTriLin (T.val.val, T.val.val, B₃.val)),
   (cubicCoeff T.val)⁻¹ * (- cubeTriLin (T.val.val, T.val.val, Y₃.val)),
   (cubicCoeff T.val)⁻¹ *
-  (cubeTriLin (T.val.val, T.val.val, B₃.val) * (dot (B₃.val, T.val.val) - dot (Y₃.val, T.val.val))
+  (cubeTriLin (T.val.val, T.val.val, B₃.val) * (dot B₃.val T.val.val - dot Y₃.val T.val.val)
   - cubeTriLin (T.val.val, T.val.val, Y₃.val)
-    * (dot (Y₃.val, T.val.val) - 2 * dot (B₃.val, T.val.val))))
+    * (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val)))
 
 
 lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := by
@@ -343,8 +342,8 @@ lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
   rw [cube_proj, cube_proj_proj_B₃, cube_proj_proj_Y₃]
   ring_nf
   simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add]
-  have h1 : (cubeTriLin (T.val.val, T.val.val, Y₃.val) ^ 2 * dot (Y₃.val, B₃.val) ^ 3 * 3 +
-      dot (Y₃.val, B₃.val) ^ 3 * cubeTriLin (T.val.val, T.val.val, B₃.val) ^ 2
+  have h1 : (cubeTriLin (T.val.val, T.val.val, Y₃.val) ^ 2 * dot Y₃.val B₃.val ^ 3 * 3 +
+      dot Y₃.val B₃.val ^ 3 * cubeTriLin (T.val.val, T.val.val, B₃.val) ^ 2
        * 3) = cubicCoeff T.val := by
     rw [cubicCoeff]
     ring
@@ -378,9 +377,9 @@ def inQuadCubeProj (T : inQuadCubeSol) : inQuadCube × ℚ × ℚ × ℚ :=
   (⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,
     (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩,
     (inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2⟩,
-  (dot (Y₃.val, B₃.val))⁻¹ * (dot (Y₃.val, T.val.val) - dot (B₃.val, T.val.val)),
-  (dot (Y₃.val, B₃.val))⁻¹ * (2 * dot (B₃.val, T.val.val) - dot (Y₃.val, T.val.val)),
-  (dot (Y₃.val, B₃.val))⁻¹ * 1)
+  (dot Y₃.val B₃.val)⁻¹ * (dot Y₃.val T.val.val - dot B₃.val T.val.val),
+  (dot Y₃.val B₃.val)⁻¹ * (2 * dot B₃.val T.val.val - dot Y₃.val T.val.val),
+  (dot Y₃.val B₃.val)⁻¹ * 1)
 
 lemma inQuadCubeToSol_proj (T : inQuadCubeSol) :
     inQuadCubeToSol (inQuadCubeProj T) = T.val := by
@@ -393,7 +392,7 @@ lemma inQuadCubeToSol_proj (T : inQuadCubeSol) :
   simp only [Fin.isValue, Fin.reduceFinMk, zero_smul, add_zero, zero_add]
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel]
   simp only [one_smul]
-  rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
+  rw [show dot Y₃.val B₃.val = 108 by rfl]
   simp
 
 /-- Given an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` a solution. We will
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index c921969..6f4a118 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -208,21 +208,23 @@ lemma accYY_ext {S T : (SMCharges n).charges}
 
 /-- The quadratic bilinear map. -/
 @[simps!]
-def quadBiLin : BiLinearSymm (SMCharges n).charges where
-  toFun S := ∑ i, (Q S.1 i * Q S.2 i +
+def quadBiLin : BiLinearSymm (SMCharges n).charges := BiLinearSymm.mk₂
+  (fun S => ∑ i, (Q S.1 i * Q S.2 i +
     - 2 * (U S.1 i * U S.2 i) +
     D S.1 i * D S.2 i +
     (- 1) * (L S.1 i * L S.2 i) +
-    E S.1 i * E S.2 i)
-  map_smul₁' a S T := by
+    E S.1 i * E S.2 i))
+  (by
+    intro a S T
     simp only
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
     repeat erw [map_smul]
     simp [HSMul.hSMul, SMul.smul]
-    ring
-  map_add₁' S T R := by
+    ring)
+  (by
+    intro S1 S2 T
     simp only
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
@@ -230,12 +232,13 @@ def quadBiLin : BiLinearSymm (SMCharges n).charges where
     repeat erw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
       one_mul]
-    ring
-  swap' S T := by
+    ring)
+  (by
+    intro S T
     simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     apply Fintype.sum_congr
     intro i
-    ring
+    ring)
 
 /-- The quadratic anomaly cancellation condition. -/
 @[simp]
@@ -247,10 +250,10 @@ lemma accQuad_ext {S T : (SMCharges n).charges}
     (h : ∀ j, ∑ i, ((fun a => a^2) ∘ toSpecies j S) i =
     ∑ i, ((fun a => a^2) ∘ toSpecies j T) i) :
     accQuad S = accQuad T := by
-  simp only [accQuad, BiLinearSymm.toHomogeneousQuad_toFun, Fin.isValue]
+  simp only [HomogeneousQuadratic, accQuad, BiLinearSymm.toHomogeneousQuad_apply]
   erw [← quadBiLin.toFun_eq_coe]
   rw [quadBiLin]
-  simp only
+  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]
   ring_nf
@@ -301,7 +304,7 @@ lemma accCube_ext {S T : (SMCharges 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
-  simp only [accCube, TriLinearSymm.toCubic_toFun, Fin.isValue]
+  simp only [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply]
   erw [← cubeTriLin.toFun_eq_coe]
   rw [cubeTriLin]
   simp only
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index a51df59..3c338ec 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -84,9 +84,7 @@ lemma asLinear_val (S : linearParameters) : S.asLinear.val = S.asCharges := by
 
 lemma cubic (S : linearParameters) :
     accCube (S.asCharges) = - 54 * S.Q'^3 - 18 * S.Q' * S.Y ^ 2 + S.E'^3 := by
-  simp only [accCube, TriLinearSymm.toCubic_toFun, Finset.univ_unique,
-    Fin.default_eq_zero, Fin.isValue, asCharges, SMNoGrav_numberCharges, neg_add_rev, neg_mul,
-    Finset.sum_singleton]
+  simp only [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, neg_mul]
   erw [← TriLinearSymm.toFun_eq_coe]
   rw [cubeTriLin]
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index 9d06fc7..3209846 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@@ -230,21 +230,23 @@ lemma accYY_ext {S T : (SMνCharges n).charges}
 
 /-- The quadratic bilinear map. -/
 @[simps!]
-def quadBiLin : BiLinearSymm (SMνCharges n).charges where
-  toFun S := ∑ i, (Q S.1 i * Q S.2 i +
+def quadBiLin : BiLinearSymm (SMνCharges n).charges := BiLinearSymm.mk₂
+  (fun S => ∑ i, (Q S.1 i * Q S.2 i +
     - 2 * (U S.1 i * U S.2 i) +
     D S.1 i * D S.2 i +
     (- 1) * (L S.1 i * L S.2 i) +
-    E S.1 i * E S.2 i)
-  map_smul₁' a S T := by
+    E S.1 i * E S.2 i))
+  (by
+    intro a S T
     simp only
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
     repeat erw [map_smul]
     simp [HSMul.hSMul, SMul.smul]
-    ring
-  map_add₁' S T R := by
+    ring)
+  (by
+    intro S T R
     simp only
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
@@ -252,19 +254,20 @@ def quadBiLin : BiLinearSymm (SMνCharges n).charges where
     repeat erw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
       one_mul]
-    ring
-  swap' S T := by
+    ring)
+  (by
+    intro S T
     simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     apply Fintype.sum_congr
     intro i
-    ring
+    ring)
 
 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 +
+    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
+  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 [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul, add_left_inj]
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index 91786d7..33ffc7a 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -190,7 +190,7 @@ lemma familyUniversal_accYY (S : (SMνCharges 1).charges) :
   ring
 
 lemma familyUniversal_quadBiLin (S : (SMνCharges 1).charges) (T : (SMνCharges n).charges) :
-    quadBiLin (familyUniversal n S, T) =
+    quadBiLin (familyUniversal n S) T =
     S (0 : Fin 6) * ∑ i, Q T i - 2 * S (1 : Fin 6) * ∑ i, U T i + S (2 : Fin 6) *∑ i, D T i -
     S (3 : Fin 6) * ∑ i, L T i + S (4 : Fin 6) * ∑ i, E T i  := by
   rw [quadBiLin_decomp]
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
index fc7ef5b..c483dcc 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@@ -58,14 +58,14 @@ namespace BL
 variable {n : ℕ}
 
 lemma on_quadBiLin (S : (PlusU1 n).charges) :
-    quadBiLin ((BL n).val, S) = 1/2 * accYY S + 3/2 * accSU2 S - 2 * accSU3 S := by
+    quadBiLin (BL n).val S = 1/2 * accYY S + 3/2 * accSU2 S - 2 * accSU3 S := by
   erw [familyUniversal_quadBiLin]
   rw [accYY_decomp, accSU2_decomp, accSU3_decomp]
   simp only [Fin.isValue, BL₁_val, SMνSpecies_numberCharges, toSpecies_apply, one_mul, mul_neg,
     mul_one, neg_mul, sub_neg_eq_add, one_div]
   ring
 
-lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin ((BL n).val, S.val) = 0 := by
+lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (BL n).val S.val = 0 := by
   rw [on_quadBiLin]
   rw [YYsol S, SU2Sol S, SU3Sol S]
   simp
@@ -110,8 +110,8 @@ lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
   erw [TriLinearSymm.toCubic_add, cubeSol (b • (BL n)), accCube.map_smul]
   repeat rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
   rw [on_cubeTriLin_AFL]
-  simp only [accCube, TriLinearSymm.toCubic_toFun, cubeTriLin_toFun, Fin.isValue, add_zero, BL_val,
-    mul_zero]
+  simp only [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, cubeTriLin_toFun, Fin.isValue,
+    add_zero, BL_val, mul_zero]
   ring
 
 
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
index 9c3ef17..6270cfd 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -56,7 +56,7 @@ namespace Y
 variable {n : ℕ}
 
 lemma on_quadBiLin (S : (PlusU1 n).charges) :
-    quadBiLin ((Y n).val, S) = accYY S := by
+    quadBiLin (Y n).val S = accYY S := by
   erw [familyUniversal_quadBiLin]
   rw [accYY_decomp]
   simp only [Fin.isValue, Y₁_val, SMνSpecies_numberCharges, toSpecies_apply, one_mul, mul_neg,
@@ -64,7 +64,7 @@ lemma on_quadBiLin (S : (PlusU1 n).charges) :
   ring_nf
   simp
 
-lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin ((Y n).val, S.val) = 0 := by
+lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (Y n).val S.val = 0 := by
   rw [on_quadBiLin]
   rw [YYsol S]
 
@@ -123,8 +123,8 @@ lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
   erw [TriLinearSymm.toCubic_add, cubeSol (b • (Y n)), accCube.map_smul]
   repeat rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
   rw [on_cubeTriLin_AFL]
-  simp only [accCube, TriLinearSymm.toCubic_toFun, cubeTriLin_toFun, Fin.isValue, add_zero, Y_val,
-    mul_zero]
+  simp only [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, cubeTriLin_toFun, Fin.isValue,
+    add_zero, Y_val, mul_zero]
   ring
 
 lemma add_AFQ_cube (S : (PlusU1 n).QuadSols) (a b : ℚ) :
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index 98e74a0..8141d90 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -74,13 +74,13 @@ def B : Fin 11 → (PlusU1 3).charges := fun i =>
   | 9 => B₉
   | 10 => B₁₀
 
-lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i, B j) = 0 := by
+lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i) (B j) = 0 := by
   fin_cases i <;> fin_cases j
   any_goals rfl
   all_goals simp at hi
 
 lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
-    quadBiLin (B i, ∑ k, f k • B k) = f i * quadBiLin (B i, B i)  := by
+    quadBiLin (B i) (∑ k, f k • B k) = f i * quadBiLin (B i) (B i)  := by
   rw [quadBiLin.map_sum₂]
   rw [Fintype.sum_eq_single i]
   rw [quadBiLin.map_smul₂]
@@ -92,13 +92,13 @@ lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
 @[simp]
 def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]
 
-lemma quadCoeff_eq_bilinear (i : Fin 11) : quadCoeff i = quadBiLin (B i, B i) := by
+lemma quadCoeff_eq_bilinear (i : Fin 11) : quadCoeff i = quadBiLin (B i) (B i) := by
   fin_cases i
   all_goals rfl
 
 lemma on_accQuad (f : Fin 11 → ℚ) :
     accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * (f i)^2  := by
-  change quadBiLin _ = _
+  change quadBiLin _ _ = _
   rw [quadBiLin.map_sum₁]
   apply Fintype.sum_congr
   intro i
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
index 36c528d..c49d76e 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
@@ -33,14 +33,14 @@ variable (C : (PlusU1 n).QuadSols)
 
 lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accQuad (a • S.val + b • C.val) =
-    a * (a * accQuad S.val + 2 * b * quadBiLin (S.val, C.val)) := by
+    a * (a * accQuad S.val + 2 * b * quadBiLin S.val C.val) := by
   erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • C)]
   rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
   erw [accQuad.map_smul]
   ring
 
 /-- A helper function for what comes later. -/
-def α₁ (S : (PlusU1 n).LinSols) : ℚ := - 2 * quadBiLin (S.val, C.val)
+def α₁ (S : (PlusU1 n).LinSols) : ℚ := - 2 * quadBiLin S.val C.val
 
 /-- A helper function for what comes later. -/
 def α₂ (S : (PlusU1 n).LinSols) : ℚ := accQuad S.val