diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
index bcb17fa..f917b4c 100644
--- a/HepLean/AnomalyCancellation/LinearMaps.lean
+++ b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -55,7 +55,7 @@ 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
@@ -180,92 +180,119 @@ lemma map_smul (f : HomogeneousCubic V) (a : ℚ) (S : V) : f (a • S) = a ^ 3
 end HomogeneousCubic
 
 /-- The structure of a symmetric trilinear function. -/
-structure TriLinearSymm' (V : Type) [AddCommMonoid V] [Module ℚ V] extends
+structure TriLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends
     V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
-  swap₁' : ∀ S T L, toFun S T L = toFun T S L
+  swap₁' : ∀ S T L, toFun S T L  = toFun T S L
   swap₂' : ∀ S T L, toFun S T L = toFun S L T
 
-/-- The structure of a symmetric trilinear function. -/
-structure TriLinearSymm (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_add₁' : ∀ S1 S2 T L, toFun (S1 + S2, T, L) = toFun (S1, T, L) + toFun (S2, T, L)
-  swap₁' : ∀ S T L, toFun (S, T, L) = toFun (T, S, L)
-  swap₂' : ∀ S T L, toFun (S, T, L) = toFun (S, L, T)
-
 namespace TriLinearSymm
 open BigOperators
 variable {V : Type} [AddCommMonoid V] [Module ℚ V]
 
-instance instFun : FunLike (TriLinearSymm V) (V × V × V) ℚ where
+instance instFun : FunLike (TriLinearSymm V) V (V →ₗ[ℚ] V →ₗ[ℚ] ℚ )  where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
     cases g
     simp_all
 
-lemma toFun_eq_coe (f : TriLinearSymm V) : f.toFun = f := rfl
+/-- The construction of a symmetric trilinear map from smul and map_add in the first factor,
+and two swap. -/
+@[simps!]
+def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) = a * f (S, T, L))
+    (map_add : ∀ S1 S2 T L, f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L))
+    (swap₁ : ∀ S T L, f (S, T, L) = f (T, S, L))
+    (swap₂ : ∀ S T L, f (S, T, L) = f (S, L, T)) : TriLinearSymm V where
+  toFun := fun S => (BiLinearSymm.mk₂ (fun T => f (S, T))
+    (by
+      intro a T L
+      simp only
+      rw [swap₁, map_smul, swap₁])
+    (by
+      intro S1 S2 T
+      simp only
+      rw [swap₁, map_add, swap₁, swap₁ S2 S T])
+    (by
+      intro L T
+      simp only
+      rw [swap₂])).toLinearMap
+  map_add' S1 S2 := by
+    apply LinearMap.ext
+    intro T
+    apply LinearMap.ext
+    intro S
+    simp [BiLinearSymm.mk₂, map_add]
+  map_smul' a S := by
+    apply LinearMap.ext
+    intro T
+    apply LinearMap.ext
+    intro L
+    simp [BiLinearSymm.mk₂, map_smul]
+  swap₁' := swap₁
+  swap₂' := swap₂
 
-lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f (S, T, L) = f (T, S, L) :=
+
+lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f S T L = f T S L :=
   f.swap₁' S T L
 
-lemma swap₂ (f : TriLinearSymm V) (S T L : V) : f (S, T, L) = f (S, L, T) :=
+lemma swap₂ (f : TriLinearSymm V) (S T L : V) : f S T L = f S L T :=
   f.swap₂' S T L
 
-lemma swap₃ (f : TriLinearSymm V) (S T L : V) : f (S, T, L) = f (L, T, S) := by
+lemma swap₃ (f : TriLinearSymm V) (S T L : V) : f S T L = f L T S := by
   rw [f.swap₁, f.swap₂, f.swap₁]
 
 lemma map_smul₁ (f : TriLinearSymm V) (a : ℚ) (S T L : V) :
-    f (a • S, T, L) = a * f (S, T, L) :=
-  f.map_smul₁' a S T L
+    f (a • S) T L = a * f S T L := by
+  erw [f.map_smul a S]
+  rfl
 
 lemma map_smul₂ (f : TriLinearSymm V) (S : V) (a : ℚ) (T L : V) :
-    f (S, a • T, L) = a * f (S, T, L) := by
+    f S (a • T) L = a * f S T L := by
   rw [f.swap₁, f.map_smul₁, f.swap₁]
 
 lemma map_smul₃ (f : TriLinearSymm V) (S T : V) (a : ℚ) (L : V) :
-    f (S, T, a • L) = a * f (S, T, L) := by
+    f S T (a • L) = a * f S T L := by
   rw [f.swap₃, f.map_smul₁, f.swap₃]
 
 lemma map_add₁ (f : TriLinearSymm V) (S1 S2 T L : V) :
-    f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L) :=
-  f.map_add₁' S1 S2 T L
+    f (S1 + S2) T L = f S1 T L + f S2 T L := by
+  erw [f.map_add]
+  rfl
 
 lemma map_add₂ (f : TriLinearSymm V) (S T1 T2 L : V) :
-    f (S, T1 + T2, L) = f (S, T1, L) + f (S, T2, L) := by
+    f S (T1 + T2) L = f S T1 L + f S T2 L := by
   rw [f.swap₁, f.map_add₁, f.swap₁ S T1, f.swap₁ S T2]
 
 lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
-    f (S, T, L1 + L2) = f (S, T, L1) + f (S, T, L2) := by
+    f S T (L1 + L2) = f S T L1 + f S T L2 := by
   rw [f.swap₃, f.map_add₁, f.swap₃, f.swap₃ L2 T S]
 
 /-- Fixing the second and third input vectors, the resulting linear map. -/
 def toLinear₁  (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
-  toFun S := f (S, T, L)
+  toFun S := f S T L
   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 : TriLinearSymm V) (S T L : V) : f (S, T, L) = f.toLinear₁ T L S := rfl
+lemma toLinear₁_apply (f : TriLinearSymm V) (S T L : V) : f S T L = f.toLinear₁ T L S := rfl
 
 lemma map_sum₁ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
-    f (∑ i, S i, T, L) = ∑ i, f (S i, T, L) := by
+    f (∑ i, S i) T L = ∑ i, f (S i) T L := by
   rw [f.toLinear₁_apply]
   rw [map_sum]
   rfl
 
 lemma map_sum₂ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
-    f ( T, ∑ i, S i, L) = ∑ i, f (T, S i, L) := by
+    f T (∑ i, S i) L = ∑ i, f T (S i) L := by
   rw [swap₁, map_sum₁]
   apply Fintype.sum_congr
   intro i
   rw [swap₁]
 
 lemma map_sum₃ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
-    f ( T, L, ∑ i, S i) = ∑ i, f (T, L, S i) := by
+    f T L (∑ i, S i) = ∑ i, f T L (S i) := by
   rw [swap₃, map_sum₁]
   apply Fintype.sum_congr
   intro i
@@ -273,7 +300,7 @@ lemma map_sum₃ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L :
 
 lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
     (T : Fin n2 → V) (L : Fin n3 → V) :
-    f (∑ i, S i, ∑ i, T i, ∑ i, L i) = ∑ i, ∑ k, ∑ l, f (S i,  T k,  L l) := by
+    f (∑ i, S i) (∑ i, T i) (∑ i, L i) = ∑ i, ∑ k, ∑ l, f (S i) (T k) (L l) := by
   rw [map_sum₁]
   apply Fintype.sum_congr
   intro i
@@ -287,7 +314,7 @@ lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
 @[simps!]
 def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
     (τ : TriLinearSymm charges) : HomogeneousCubic charges where
-  toFun S := τ (S, S, S)
+  toFun S := τ S S S
   map_smul' a S := by
     simp only [smul_eq_mul]
     rw [τ.map_smul₁, τ.map_smul₂, τ.map_smul₃]
@@ -296,7 +323,7 @@ def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
 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
+    τ.toCubic T + 3 * τ S S T + 3 * τ T T S := by
   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]
diff --git a/HepLean/AnomalyCancellation/MSSMNu/B3.lean b/HepLean/AnomalyCancellation/MSSMNu/B3.lean
index 88ec09c..378cd82 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/B3.lean
@@ -59,9 +59,9 @@ def B₃ : MSSMACC.Sols :=
 lemma B₃_val : B₃.val = B₃AsCharge := by
   rfl
 
-lemma doublePoint_B₃_B₃ (R : MSSMACC.LinSols) : cubeTriLin (B₃.val, B₃.val, R.val) = 0 := by
-  rw [← TriLinearSymm.toFun_eq_coe]
-  simp only [cubeTriLin, cubeTriLinToFun, MSSMSpecies_numberCharges]
+lemma doublePoint_B₃_B₃ (R : MSSMACC.LinSols) : cubeTriLin B₃.val B₃.val R.val = 0 := by
+  simp only [cubeTriLin, TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun,
+    MSSMSpecies_numberCharges, Fin.isValue, Fin.reduceFinMk]
   rw [Fin.sum_univ_three]
   rw [B₃_val]
   rw [B₃AsCharge]
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index dd42a33..839e1d9 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -409,12 +409,13 @@ lemma cubeTriLinToFun_swap2 (S T R : MSSMCharges.charges) :
   ring
 
 /-- The symmetric trilinear form used to define the cubic ACC. -/
-def cubeTriLin : TriLinearSymm MSSMCharges.charges where
-  toFun S := cubeTriLinToFun S
-  map_smul₁' := cubeTriLinToFun_map_smul₁
-  map_add₁' := cubeTriLinToFun_map_add₁
-  swap₁' := cubeTriLinToFun_swap1
-  swap₂' := cubeTriLinToFun_swap2
+@[simps!]
+def cubeTriLin : TriLinearSymm MSSMCharges.charges := TriLinearSymm.mk₃
+  cubeTriLinToFun
+  cubeTriLinToFun_map_smul₁
+  cubeTriLinToFun_map_add₁
+  cubeTriLinToFun_swap1
+  cubeTriLinToFun_swap2
 
 /-- The cubic ACC. -/
 @[simp]
@@ -426,10 +427,8 @@ lemma accCube_ext {S T : MSSMCharges.charges}
     ∑ i, ((fun a => a^3) ∘ toSMSpecies j T) i)
     (hd : Hd S = Hd T) (hu : Hu S = Hu T)  :
     accCube S = accCube T := by
-  simp [cubeTriLin, cubeTriLinToFun]
-  erw [← cubeTriLin.toFun_eq_coe]
-  rw [cubeTriLin]
-  simp only [cubeTriLinToFun]
+  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]
   ring_nf
diff --git a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
index c77df0f..968f8e3 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
@@ -54,8 +54,8 @@ lemma lineY₃B₃Charges_cubic (a b : ℚ) : accCube (lineY₃B₃Charges a b).
   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]
-  rw [show cubeTriLin (Y₃.val, Y₃.val, B₃.val) = 0 by rfl]
-  rw [show cubeTriLin (B₃.val, B₃.val, Y₃.val) = 0 by rfl]
+  rw [show cubeTriLin Y₃.val Y₃.val B₃.val = 0 by rfl]
+  rw [show cubeTriLin B₃.val B₃.val Y₃.val = 0 by rfl]
   simp
 
 /-- The line through $Y_3$ and $B_3$ as `Sols`. -/
@@ -63,9 +63,9 @@ 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 doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
-    cubeTriLin (Y₃.val, B₃.val, R.val) = 0 := by
-  rw [← TriLinearSymm.toFun_eq_coe]
-  simp only [cubeTriLin, cubeTriLinToFun, MSSMSpecies_numberCharges]
+    cubeTriLin Y₃.val B₃.val R.val = 0 := by
+  simp only [cubeTriLin, TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun,
+    MSSMSpecies_numberCharges, Fin.isValue, Fin.reduceFinMk]
   rw [Fin.sum_univ_three]
   rw [B₃_val, Y₃_val]
   rw [B₃AsCharge, Y₃AsCharge]
@@ -83,8 +83,8 @@ lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
   linear_combination -(12 * h2) + 9 * h1 + 3 * h3
 
 lemma lineY₃B₃_doublePoint (R : MSSMACC.LinSols) (a b : ℚ) :
-    cubeTriLin ((lineY₃B₃ a b).val, (lineY₃B₃ a b).val, R.val) = 0 := by
-  change cubeTriLin (a • Y₃.val + b • B₃.val , a • Y₃.val + b • B₃.val, R.val ) = 0
+    cubeTriLin (lineY₃B₃ a b).val (lineY₃B₃ a b).val R.val = 0 := by
+  change cubeTriLin (a • Y₃.val + b • B₃.val) (a • Y₃.val + b • B₃.val) R.val = 0
   rw [cubeTriLin.map_add₂, cubeTriLin.map_add₁, cubeTriLin.map_add₁]
   repeat rw [cubeTriLin.map_smul₂, cubeTriLin.map_smul₁]
   rw [doublePoint_B₃_B₃, doublePoint_Y₃_Y₃, doublePoint_Y₃_B₃]
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
index cd3a157..7442533 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
@@ -121,8 +121,8 @@ 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
+    cubeTriLin (proj T).val (proj T).val Y₃.val =
+    (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]
@@ -143,8 +143,8 @@ lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
   ring
 
 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
+    cubeTriLin (proj T).val (proj T).val B₃.val =
+    (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]
@@ -159,10 +159,10 @@ lemma cube_proj_proj_B₃ (T : MSSMACC.LinSols) :
   ring
 
 lemma cube_proj_proj_self (T : MSSMACC.Sols) :
-    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, T.val) =
+    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
+    ((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]
@@ -176,10 +176,10 @@ lemma cube_proj_proj_self (T : MSSMACC.Sols) :
   ring
 
 lemma cube_proj (T : MSSMACC.Sols) :
-    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, (proj T.1.1).val) =
+    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
+    ((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 4918d14..85a5443 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@@ -115,8 +115,8 @@ lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
 
 lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
     accCube (planeY₃B₃ R a b c).val = c ^ 2 *
-    (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
+    (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]
   erw [TriLinearSymm.toCubic_add]
   erw [lineY₃B₃Charges_cubic]
@@ -124,7 +124,7 @@ lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
   rw [cubeTriLin.toCubic.map_smul]
   rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
   rw [cubeTriLin.map_add₃, cubeTriLin.map_smul₃, cubeTriLin.map_smul₃]
-  rw [show (TriLinearSymm.toCubic cubeTriLin) R.val = cubeTriLin (R.val, R.val, R.val) by rfl]
+  rw [show (TriLinearSymm.toCubic cubeTriLin) R.val = cubeTriLin R.val R.val R.val by rfl]
   ring
 
 /-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic,
@@ -163,18 +163,18 @@ 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)
+    (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)
+    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 =
@@ -188,9 +188,9 @@ def α₁ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
 def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
     MSSMACC.LinSols :=
   planeY₃B₃ R
-    (a₂ * cubeTriLin (R.val, R.val, R.val) - 3 * a₃ * cubeTriLin (R.val, R.val, B₃.val))
-    (3 * a₃ * cubeTriLin (R.val, R.val, Y₃.val) -  a₁ * cubeTriLin (R.val, R.val, R.val))
-    (3 * (a₁ * cubeTriLin (R.val, R.val, B₃.val) - a₂ * cubeTriLin (R.val, R.val, Y₃.val)))
+    (a₂ * cubeTriLin R.val R.val R.val - 3 * a₃ * cubeTriLin R.val R.val B₃.val)
+    (3 * a₃ * cubeTriLin R.val R.val Y₃.val -  a₁ * cubeTriLin R.val R.val R.val)
+    (3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val))
 
 
 lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
@@ -210,7 +210,7 @@ lemma lineCube_cube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
 
 lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
     accQuad (lineCube R a₁ a₂ a₃).val =
-    3 * (a₁ * cubeTriLin (R.val, R.val, B₃.val) - a₂ * cubeTriLin (R.val, R.val, Y₃.val)) *
+    3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val) *
     (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃) := by
   erw [planeY₃B₃_quad]
   rw [α₁, α₂, α₃]
@@ -221,8 +221,8 @@ 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
+    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
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 619cd61..2ab823f 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -46,8 +46,8 @@ 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`. -/
@@ -134,8 +134,8 @@ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) :
 /-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
 entirely in the cubic surface. -/
 def inCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
-    cubeTriLin (R.val, R.val, R.val) = 0 ∧ cubeTriLin (R.val, R.val, B₃.val) = 0 ∧
-    cubeTriLin (R.val, R.val, Y₃.val) = 0
+    cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧
+    cubeTriLin R.val R.val Y₃.val = 0
 
 
 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (inCubeProp R) := by
@@ -144,13 +144,13 @@ instance (R : MSSMACC.AnomalyFreePerp) : Decidable (inCubeProp R) := by
 /-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃`
 lies entirely in the cubic surface. -/
 def inCubeSolProp (R : MSSMACC.Sols) : Prop :=
-    cubeTriLin (R.val, R.val, B₃.val) = 0 ∧ cubeTriLin (R.val, R.val, Y₃.val) = 0
+    cubeTriLin R.val R.val B₃.val = 0 ∧ cubeTriLin R.val R.val Y₃.val = 0
 
 /-- 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  +
-    cubeTriLin (T.val, T.val, B₃.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) :
     inCubeSolProp T ↔ cubicCoeff T = 0 := by
@@ -214,9 +214,9 @@ def inQuadCubeSol : Type :=
 /-- Given a `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
 def toSolNSQuad (R : MSSMACC.AnomalyFreePerp) : MSSMACC.QuadSols :=
   lineQuad R
-    (3 * cubeTriLin (R.val, R.val, Y₃.val))
-    (3 * cubeTriLin (R.val, R.val, B₃.val))
-    (cubeTriLin (R.val, R.val, R.val))
+    (3 * cubeTriLin R.val R.val Y₃.val)
+    (3 * cubeTriLin R.val R.val B₃.val)
+    (cubeTriLin R.val R.val R.val)
 
 lemma toSolNSQuad_cube (R : MSSMACC.AnomalyFreePerp) :
     accCube (toSolNSQuad R).val = 0 := by
@@ -325,11 +325,11 @@ lemma inQuadToSol_smul (R : inQuad) (c₁ c₂ c₃ d : ℚ) :
 def inQuadProj (T : inQuadSol) : inQuad × ℚ × ℚ × ℚ :=
   (⟨⟨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⟩,
-  (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),
+  (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, Y₃.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)))
 
 
@@ -342,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
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Y3.lean b/HepLean/AnomalyCancellation/MSSMNu/Y3.lean
index f065a0b..d7f2b16 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Y3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Y3.lean
@@ -60,9 +60,9 @@ lemma Y₃_val : Y₃.val = Y₃AsCharge := by
   rfl
 
 lemma doublePoint_Y₃_Y₃ (R : MSSMACC.LinSols) :
-    cubeTriLin (Y₃.val, Y₃.val, R.val) = 0 := by
-  rw [← TriLinearSymm.toFun_eq_coe]
-  simp only [cubeTriLin, cubeTriLinToFun, MSSMSpecies_numberCharges]
+    cubeTriLin Y₃.val Y₃.val R.val = 0 := by
+  simp only [cubeTriLin, TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun,
+    MSSMSpecies_numberCharges, Fin.isValue, Fin.reduceFinMk]
   rw [Fin.sum_univ_three]
   rw [Y₃_val]
   rw [Y₃AsCharge]
diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index 1482a39..b9f04a3 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -38,42 +38,39 @@ def accGrav (n : ℕ) : ((PureU1Charges n).charges →ₗ[ℚ] ℚ) where
 
 /-- The symmetric trilinear form used to define the cubic anomaly. -/
 @[simps!]
-def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).charges where
-  toFun S := ∑ i, S.1 i * S.2.1 i * S.2.2 i
-  map_smul₁' a S L T := by
+def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).charges := TriLinearSymm.mk₃
+  (fun  S =>  ∑ i, S.1 i * S.2.1 i * S.2.2 i)
+  (by
+    intro a S L T
     simp [HSMul.hSMul]
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
-    ring
-  map_add₁' S L T R := by
+    ring)
+  (by
+    intro S L T R
     simp only [PureU1Charges_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
     intro i
     ring
-  swap₁' S L T := by
+    )
+  (by
+    intro S L T
     simp only [PureU1Charges_numberCharges]
     apply Fintype.sum_congr
     intro i
     ring
-  swap₂' S L T := by
+  )
+  (by
+    intro S L T
     simp only [PureU1Charges_numberCharges]
     apply Fintype.sum_congr
     intro i
     ring
+  )
+
 
-lemma accCubeTriLinSymm_cast {n m : ℕ} (h : m = n)
-    (S :  (PureU1Charges n).charges × (PureU1Charges n).charges × (PureU1Charges n).charges) :
-    accCubeTriLinSymm S = ∑ i : Fin m,
-      S.1 (Fin.cast h i) * S.2.1 (Fin.cast h i) * S.2.2 (Fin.cast h i) := by
-  rw [← accCubeTriLinSymm.toFun_eq_coe, accCubeTriLinSymm]
-  simp only [PureU1Charges_numberCharges]
-  rw [Finset.sum_equiv (Fin.castIso h).symm.toEquiv]
-  intro i
-  simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
-  intro i
-  simp
 
 /-- The cubic anomaly equation. -/
 @[simp]
@@ -84,9 +81,9 @@ def accCube (n : ℕ)  : HomogeneousCubic ((PureU1Charges n).charges) :=
 lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).charges) :
     accCube n S = ∑ i : Fin n, S i ^ 3:= by
   rw [accCube, TriLinearSymm.toCubic]
-  change  accCubeTriLinSymm.toFun (S, S, S) = _
+  change  accCubeTriLinSymm S S S = _
   rw [accCubeTriLinSymm]
-  simp only [PureU1Charges_numberCharges]
+  simp only [PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply]
   apply Finset.sum_congr
   simp only
   ring_nf
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index 1963a5f..63b1ee5 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -470,7 +470,7 @@ lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by
   ring
 
 lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
-    accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j)
+    accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
     = g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by
   simp [accCubeTriLinSymm]
   rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
@@ -485,7 +485,7 @@ lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
   simp
 
 lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) :
-    accCubeTriLinSymm.toFun (P! g, P! g, basisAsCharges j)
+    accCubeTriLinSymm (P! g) (P! g) (basisAsCharges j)
     =  (P! g (δ₁ j))^2 -  (P! g (δ₂ j))^2 := by
   simp [accCubeTriLinSymm]
   rw [sum_δ₁_δ₂]
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index d439440..834dc5b 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -42,8 +42,8 @@ def lineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
 
 lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) :
     ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
-    3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f)
-    + b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by
+    3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f)
+    + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := by
   intro g f hS a b
   have h1 := h g f hS a b
   change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1
@@ -62,7 +62,7 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S)
 -/
 lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) :
     ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val =  P g + P! f),
-    accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+    accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
   intro g f hS
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
    (lineInCubic_expand h g f hS 1 2) / 6
@@ -92,7 +92,7 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
     (LIC : lineInCubicPerm S) :
     ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) ,
       (S.val (δ!₂ j) - S.val (δ!₁ j))
-      * accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by
+      * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
   intro j g f h
   let S' :=  (FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j)) S
   have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
@@ -106,7 +106,7 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
 
 lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ )).LinSols}
     (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) :
-    accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges  (Fin.last n)) =
+    accCubeTriLinSymm (P f) (P f) (basis!AsCharges  (Fin.last n)) =
     - (S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) * (2 * S.val δ!₄ +
     S.val (δ!₂ (Fin.last n))  + S.val (δ!₁ (Fin.last n))) := by
   rw [P_P_P!_accCube f  (Fin.last n)]
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
index 359465a..fd6a18e 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -38,13 +38,13 @@ point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show ext
 free point. -/
 def parameterizationAsLinear (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
     (PureU1 (2 * n.succ)).LinSols :=
-  a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
-  (- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
+  a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P' g +
+  (- accCubeTriLinSymm (P g) (P g) (P! f)) • P!' f)
 
 lemma parameterizationAsLinear_val (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
     (parameterizationAsLinear g f a).val =
-    a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
-    (- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
+    a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P g +
+    (- accCubeTriLinSymm (P g) (P g) (P! f)) • P! f) := by
   rw [parameterizationAsLinear]
   change a • (_ • (P' g).val + _ • (P!' f).val) = _
   rw [P'_val, P!'_val]
@@ -68,7 +68,7 @@ def parameterization (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
 
 lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols}
     (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (hS : S.val = P g + P! f) :
-    accCubeTriLinSymm (P g, P g, P! f) = - accCubeTriLinSymm (P! f, P! f, P g) := by
+    accCubeTriLinSymm (P g) (P g) (P! f) = - accCubeTriLinSymm (P! f) (P! f) (P g) := by
   have hC := S.cubicSol
   rw [hS] at hC
   change (accCube (2 * n.succ)) (P g + P! f) = 0 at hC
@@ -81,11 +81,11 @@ lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols}
 In this case our parameterization above will be able to recover this point. -/
 def genericCase (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
   ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
-  accCubeTriLinSymm (P g, P g, P! f) ≠  0
+  accCubeTriLinSymm (P g) (P g) (P! f) ≠  0
 
 lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols)
     (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧
-    accCubeTriLinSymm (P g, P g, P! f) ≠  0) : genericCase S := by
+    accCubeTriLinSymm (P g) (P g) (P! f) ≠  0) : genericCase S := by
   intro g f hS hC
   obtain ⟨g', f', hS', hC'⟩ := hs
   rw [hS] at hS'
@@ -96,11 +96,11 @@ lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols)
 /-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) = 0`.-/
 def specialCase  (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
   ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
-  accCubeTriLinSymm (P g, P g, P! f) = 0
+  accCubeTriLinSymm (P g) (P g) (P! f) = 0
 
 lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols)
     (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧
-    accCubeTriLinSymm (P g, P g, P! f) =  0) : specialCase S := by
+    accCubeTriLinSymm (P g) (P g) (P! f) =  0) : specialCase S := by
   intro g f hS
   obtain ⟨g', f', hS', hC'⟩ := hs
   rw [hS] at hS'
@@ -111,8 +111,8 @@ lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols)
 lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) :
     genericCase S ∨ specialCase S := by
   obtain ⟨g, f, h⟩ := span_basis S.1.1
-  have h1 :  accCubeTriLinSymm (P g, P g, P! f) ≠  0 ∨
-     accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+  have h1 :  accCubeTriLinSymm (P g) (P g) (P! f) ≠  0 ∨
+     accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
     exact ne_or_eq _ _
   cases h1 <;> rename_i h1
   exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
@@ -121,7 +121,7 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) :
 theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : genericCase S) :
     ∃ g f a,  S = parameterization g f a := by
   obtain ⟨g, f, hS⟩ := span_basis S.1.1
-  use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
+  use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹
   rw [parameterization]
   apply ACCSystem.Sols.ext
   rw [parameterizationAsLinear_val]
@@ -148,7 +148,7 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
   rw [h]
   rw [anomalyFree_param _ _ hS] at h
   simp at h
-  change accCubeTriLinSymm (P! f, P! f, P g) = 0 at h
+  change accCubeTriLinSymm (P! f) (P! f) (P g) = 0 at h
   erw [h]
   simp
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index 903d788..ef0361d 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -471,7 +471,7 @@ lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by
   ring
 
 lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
-    accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j)
+    accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
     = (P g (δ!₁ j))^2 - (g j)^2 := by
   simp [accCubeTriLinSymm]
   rw [sum_δ!, basis!_on_δ!₃]
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index 8ee978e..d7a9000 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -42,8 +42,8 @@ def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
 
 lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) :
     ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ) ,
-    3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f)
-    + b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by
+    3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f)
+    + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := by
   intro g f hS a b
   have h1 := h g f hS a b
   change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1
@@ -57,7 +57,7 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S)
 
 lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) :
     ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val =  P g + P! f),
-    accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+    accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
   intro g f hS
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) -
      (lineInCubic_expand h g f hS 1 2 ) / 6
@@ -91,7 +91,7 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
     (LIC : lineInCubicPerm S) :
     ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) ,
       (S.val (δ!₂ j) - S.val (δ!₁ j))
-      * accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by
+      * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
   intro j g f h
   let S' :=  (FamilyPermutations (2 * n.succ + 1)).linSolRep
     (pairSwap (δ!₁ j) (δ!₂ j)) S
@@ -107,7 +107,7 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
 
 lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
     (f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) :
-    accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges 0) =
+    accCubeTriLinSymm (P f) (P f) (basis!AsCharges 0) =
     (S.val (δ!₁ 0) + S.val (δ!₂ 0)) * (2 * S.val δ!₃ + S.val (δ!₁ 0) + S.val (δ!₂ 0)) := by
   rw [P_P_P!_accCube f 0]
   rw [← Pa_δa₁ f g]
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
index 02d2d18..f219b8a 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -33,13 +33,13 @@ open VectorLikeOddPlane
 show that this can be extended to a complete solution. -/
 def parameterizationAsLinear (g f : Fin n → ℚ)  (a : ℚ) :
     (PureU1 (2 * n + 1)).LinSols :=
-  a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
-  (- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
+  a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P' g +
+  (- accCubeTriLinSymm (P g) (P g) (P! f)) • P!' f)
 
 lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
     (parameterizationAsLinear g f a).val =
-    a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
-    (- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
+    a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P g +
+    (- accCubeTriLinSymm (P g) (P g) (P! f)) • P! f) := by
   rw [parameterizationAsLinear]
   change a • (_ • (P' g).val + _ • (P!' f).val) = _
   rw [P'_val, P!'_val]
@@ -65,8 +65,8 @@ def parameterization (g f : Fin n → ℚ) (a : ℚ) :
 
 lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
     (g f : Fin n → ℚ)  (hS : S.val = P g + P! f) :
-    accCubeTriLinSymm (P g, P g, P! f) =
-    - accCubeTriLinSymm (P! f, P! f, P g) := by
+    accCubeTriLinSymm (P g) (P g) (P! f) =
+    - accCubeTriLinSymm (P! f) (P! f) (P g) := by
   have hC := S.cubicSol
   rw [hS] at hC
   change (accCube (2 * n + 1)) (P g + P! f) = 0 at hC
@@ -79,11 +79,11 @@ lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
 In this case our parameterization above will be able to recover this point. -/
 def genericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
   ∀ (g f : Fin n.succ → ℚ)  (_ : S.val = P g + P! f) ,
-  accCubeTriLinSymm (P g, P g, P! f) ≠  0
+  accCubeTriLinSymm (P g) (P g) (P! f) ≠  0
 
 lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
     (hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
-    accCubeTriLinSymm (P g, P g, P! f) ≠  0) : genericCase S := by
+    accCubeTriLinSymm (P g) (P g) (P! f) ≠  0) : genericCase S := by
   intro g f hS hC
   obtain ⟨g', f', hS', hC'⟩ := hs
   rw [hS] at hS'
@@ -95,11 +95,11 @@ lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
 In this case we will show that S is zero if it is true for all permutations. -/
 def specialCase  (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
   ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f) ,
-  accCubeTriLinSymm (P g, P g, P! f) = 0
+  accCubeTriLinSymm (P g) (P g) (P! f) = 0
 
 lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
     (hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
-    accCubeTriLinSymm (P g, P g, P! f) =  0) : specialCase S := by
+    accCubeTriLinSymm (P g) (P g) (P! f) =  0) : specialCase S := by
   intro g f hS
   obtain ⟨g', f', hS', hC'⟩ := hs
   rw [hS] at hS'
@@ -110,8 +110,8 @@ lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
 lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
     genericCase S ∨ specialCase S := by
   obtain ⟨g, f, h⟩ := span_basis S.1.1
-  have h1 :  accCubeTriLinSymm (P g, P g, P! f) ≠  0 ∨
-     accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+  have h1 :  accCubeTriLinSymm (P g) (P g) (P! f) ≠  0 ∨
+     accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
     exact ne_or_eq _ _
   cases h1 <;> rename_i h1
   exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
@@ -120,7 +120,7 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
 theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : genericCase S) :
     ∃ g f a,  S = parameterization g f a := by
   obtain ⟨g, f, hS⟩ := span_basis S.1.1
-  use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
+  use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹
   rw [parameterization]
   apply ACCSystem.Sols.ext
   rw [parameterizationAsLinear_val]
@@ -149,7 +149,7 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
   rw [h]
   rw [anomalyFree_param _ _ hS] at h
   simp at h
-  change accCubeTriLinSymm (P! f, P! f, P g) = 0 at h
+  change accCubeTriLinSymm (P! f) (P! f) (P g) = 0 at h
   erw [h]
   simp
 
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index 6f4a118..cd71230 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -262,13 +262,14 @@ lemma accQuad_ext {S T : (SMCharges n).charges}
 
 /-- The trilinear function defining the cubic. -/
 @[simps!]
-def cubeTriLin : TriLinearSymm (SMCharges n).charges where
-  toFun S := ∑ i, (6 * ((Q S.1 i) * (Q S.2.1 i) * (Q S.2.2 i))
+def cubeTriLin : TriLinearSymm (SMCharges n).charges := TriLinearSymm.mk₃
+  (fun S => ∑ i, (6 * ((Q S.1 i) * (Q S.2.1 i) * (Q S.2.2 i))
     + 3 * ((U S.1 i) * (U S.2.1 i) * (U S.2.2 i))
     + 3 * ((D S.1 i) * (D S.2.1 i) * (D S.2.2 i))
     + 2 * ((L S.1 i) * (L S.2.1 i) * (L S.2.2 i))
-    +  ((E S.1 i) * (E S.2.1 i) * (E S.2.2 i)))
-  map_smul₁' a S T R := by
+    +  ((E S.1 i) * (E S.2.1 i) * (E S.2.2 i))))
+  (by
+    intro a S T R
     simp only
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
@@ -276,7 +277,9 @@ def cubeTriLin : TriLinearSymm (SMCharges n).charges where
     repeat erw [map_smul]
     simp [HSMul.hSMul, SMul.smul]
     ring
-  map_add₁' S T R L := by
+  )
+  (by
+    intro S T R L
     simp only
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
@@ -284,16 +287,21 @@ def cubeTriLin : TriLinearSymm (SMCharges n).charges where
     repeat erw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
     ring
-  swap₁' S T L := by
+  )
+  (by
+    intro S T L
     simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
     ring
-  swap₂' S T L := by
+  )
+  (by
+    intro S T L
     simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
     ring
+  )
 
 /-- The cubic acc. -/
 @[simp]
@@ -304,10 +312,8 @@ 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 [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply]
-  erw [← cubeTriLin.toFun_eq_coe]
-  rw [cubeTriLin]
-  simp only
+  simp only [HomogeneousCubic, accCube, cubeTriLin, TriLinearSymm.toCubic_apply,
+    TriLinearSymm.mk₃_toFun_apply_apply]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
   ring_nf
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 3c338ec..6b4f240 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -84,9 +84,8 @@ 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 [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, neg_mul]
-  erw [← TriLinearSymm.toFun_eq_coe]
-  rw [cubeTriLin]
+  simp only [HomogeneousCubic, accCube, cubeTriLin, TriLinearSymm.toCubic_apply,
+    TriLinearSymm.mk₃_toFun_apply_apply]
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton]
   repeat erw [speciesVal]
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index 3209846..a38afa2 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@@ -295,47 +295,52 @@ lemma accQuad_ext {S T : (SMνCharges n).charges}
 
 /-- The symmetric trilinear form used to define the cubic acc. -/
 @[simps!]
-def cubeTriLin : TriLinearSymm (SMνCharges n).charges where
-  toFun S := ∑ i, (6 * ((Q S.1 i) * (Q S.2.1 i) * (Q S.2.2 i))
+def cubeTriLin : TriLinearSymm (SMνCharges n).charges := TriLinearSymm.mk₃
+  (fun S => ∑ i, (6 * ((Q S.1 i) * (Q S.2.1 i) * (Q S.2.2 i))
     + 3 * ((U S.1 i) * (U S.2.1 i) * (U S.2.2 i))
     + 3 * ((D S.1 i) * (D S.2.1 i) * (D S.2.2 i))
     + 2 * ((L S.1 i) * (L S.2.1 i) * (L S.2.2 i))
     +  ((E S.1 i) * (E S.2.1 i) * (E S.2.2 i))
-    +  ((N S.1 i) * (N S.2.1 i) * (N S.2.2 i)))
-  map_smul₁' a S T R := by
+    +  ((N S.1 i) * (N S.2.1 i) * (N S.2.2 i))))
+  (by
+    intro a S T R
     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 L := by
+    ring)
+  (by
+    intro S T R L
     simp only
     rw [← Finset.sum_add_distrib]
     apply Fintype.sum_congr
     intro i
     repeat erw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
-    ring
-  swap₁' S T L := by
+    ring)
+  (by
+    intro S T L
     simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
-    ring
-  swap₂' S T L := by
+    ring)
+  (by
+    intro S T L
     simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
-    ring
+    ring)
 
 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) +
+    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
+  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]
 
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index 33ffc7a..8ffd5e8 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -210,7 +210,7 @@ lemma familyUniversal_accQuad (S : (SMνCharges 1).charges) :
   ring
 
 lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharges n).charges) :
-    cubeTriLin (familyUniversal n S, T, R) = 6 * S (0 : Fin 6) * ∑ i, (Q T i * Q R i) +
+    cubeTriLin (familyUniversal n S) T R = 6 * S (0 : Fin 6) * ∑ i, (Q T i * Q R i) +
       3 * S (1 : Fin 6) * ∑ i,  (U T i * U R i) + 3 * S (2 : Fin 6) * ∑ i,  (D T i * D R i)
       + 2 * S (3 : Fin 6) * ∑ i, (L T i * L R i) +
       S (4 : Fin 6) * ∑ i, (E T i * E R i) + S (5 : Fin 6) * ∑ i, (N T i * N R i) := by
@@ -221,7 +221,7 @@ lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharg
   ring
 
 lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).charges) (R : (SMνCharges n).charges) :
-    cubeTriLin (familyUniversal n S, familyUniversal n T, R) =
+    cubeTriLin (familyUniversal n S) (familyUniversal n T) R =
       6 * S (0 : Fin 6) * T (0 : Fin 6) * ∑ i, Q R i +
        3 * S (1 : Fin 6) * T (1 : Fin 6) * ∑ i, U R i
       + 3 * S (2 : Fin 6) * T (2 : Fin 6) * ∑ i, D R i +
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
index d2806a7..03fd5ec 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@@ -31,7 +31,7 @@ def B₀ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₀_cubic (S T : (SM 3).charges) : cubeTriLin (B₀, S, T) =
+lemma B₀_cubic (S T : (SM 3).charges) : cubeTriLin B₀ S T =
     6 * (S (0 : Fin 18) * T  (0 : Fin 18) - S  (1 : Fin 18) * T  (1 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₀, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring
@@ -44,7 +44,7 @@ def B₁ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₁_cubic (S T : (SM 3).charges) : cubeTriLin (B₁, S, T) =
+lemma B₁_cubic (S T : (SM 3).charges) : cubeTriLin B₁ S T =
     3 * (S (3 : Fin 18) * T  (3 : Fin 18) - S  (4 : Fin 18) * T  (4 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₁, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring
@@ -57,7 +57,7 @@ def B₂ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₂_cubic (S T : (SM 3).charges) : cubeTriLin (B₂, S, T) =
+lemma B₂_cubic (S T : (SM 3).charges) : cubeTriLin B₂ S T =
     3 * (S (6 : Fin 18) * T  (6 : Fin 18) - S  (7 : Fin 18) * T  (7 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₂, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring
@@ -70,7 +70,7 @@ def B₃ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₃_cubic (S T : (SM 3).charges) : cubeTriLin (B₃, S, T) =
+lemma B₃_cubic (S T : (SM 3).charges) : cubeTriLin B₃ S T =
     2 * (S (9 : Fin 18) * T  (9 : Fin 18) - S  (10 : Fin 18) * T  (10 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₃, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring_nf
@@ -84,7 +84,7 @@ def B₄ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₄_cubic (S T : (SM 3).charges) : cubeTriLin (B₄, S, T) =
+lemma B₄_cubic (S T : (SM 3).charges) : cubeTriLin B₄ S T =
     (S (12 : Fin 18) * T  (12 : Fin 18) - S  (13 : Fin 18) * T  (13 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₄, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring_nf
@@ -98,7 +98,7 @@ def B₅ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₅_cubic (S T : (SM 3).charges) : cubeTriLin (B₅, S, T) =
+lemma B₅_cubic (S T : (SM 3).charges) : cubeTriLin B₅ S T =
     (S (15 : Fin 18) * T  (15 : Fin 18) - S  (16 : Fin 18) * T  (16 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₅, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring_nf
@@ -112,7 +112,7 @@ def B₆ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   | _, _ => 0
   )
 
-lemma B₆_cubic (S T : (SM 3).charges) : cubeTriLin (B₆, S, T) =
+lemma B₆_cubic (S T : (SM 3).charges) : cubeTriLin B₆ S T =
     3* (S (5 : Fin 18) * T  (5 : Fin 18) - S  (8 : Fin 18) * T  (8 : Fin 18)) := by
   simp [Fin.sum_univ_three, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring_nf
@@ -130,8 +130,8 @@ def B : Fin 7 → (SM 3).charges := fun i =>
   | 6 => B₆
 
 lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 0, B i, S) = 0 := by
-  change cubeTriLin (B₀, B i, S) = 0
+    cubeTriLin (B 0) (B i) S = 0 := by
+  change cubeTriLin B₀ (B i) S = 0
   rw [B₀_cubic]
   fin_cases i <;>
     simp at hi <;>
@@ -139,55 +139,55 @@ lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).charges) :
 
 
 lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 1, B i, S) = 0 := by
-  change cubeTriLin (B₁, B i, S) = 0
+    cubeTriLin (B 1) (B i) S = 0 := by
+  change cubeTriLin B₁ (B i) S = 0
   rw [B₁_cubic]
   fin_cases i <;>
     simp at hi <;>
     simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₂_Bi_cubic {i : Fin 7} (hi : 2 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 2, B i, S) = 0 := by
-  change cubeTriLin (B₂, B i, S) = 0
+    cubeTriLin (B 2) (B i) S = 0 := by
+  change cubeTriLin B₂ (B i) S = 0
   rw [B₂_cubic]
   fin_cases i <;>
     simp at hi <;>
     simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₃_Bi_cubic {i : Fin 7} (hi : 3 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 3, B i, S) = 0 := by
-  change cubeTriLin (B₃, B i, S) = 0
+    cubeTriLin (B 3) (B i) S = 0 := by
+  change cubeTriLin (B₃) (B i) S = 0
   rw [B₃_cubic]
   fin_cases i <;>
-    simp at hi <;>
-    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  simp at hi <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₄_Bi_cubic {i : Fin 7} (hi : 4 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 4, B i, S) = 0 := by
-  change cubeTriLin (B₄, B i, S) = 0
+    cubeTriLin (B 4) (B i) S = 0 := by
+  change cubeTriLin (B₄) (B i) S = 0
   rw [B₄_cubic]
   fin_cases i <;>
-    simp at hi <;>
-    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  simp at hi <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₅_Bi_cubic {i : Fin 7} (hi : 5 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 5, B i, S) = 0 := by
-  change cubeTriLin (B₅, B i, S) = 0
+    cubeTriLin (B 5) (B i) S = 0 := by
+  change cubeTriLin (B₅) (B i) S = 0
   rw [B₅_cubic]
   fin_cases i <;>
-    simp at hi <;>
-    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  simp at hi <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₆_Bi_cubic {i : Fin 7} (hi : 6 ≠ i) (S : (SM 3).charges) :
-    cubeTriLin (B 6, B i, S) = 0 := by
-  change cubeTriLin (B₆, B i, S) = 0
+    cubeTriLin (B 6) (B i) S = 0 := by
+  change cubeTriLin (B₆) (B i) S = 0
   rw [B₆_cubic]
   fin_cases i <;>
-    simp at hi <;>
-    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  simp at hi <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).charges) :
-    cubeTriLin (B i, B j, S) = 0 := by
+    cubeTriLin (B i) (B j) S = 0 := by
   fin_cases i
   exact B₀_Bi_cubic h S
   exact B₁_Bi_cubic h S
@@ -198,57 +198,57 @@ lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).charges) :
   exact B₆_Bi_cubic h S
 
 lemma B₀_B₀_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 0, B 0, B i) = 0 := by
-  change cubeTriLin (B₀, B₀, B i) = 0
+    cubeTriLin (B 0) (B 0) (B i) = 0 := by
+  change cubeTriLin (B₀) (B₀) (B i) = 0
   rw [B₀_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₁_B₁_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 1, B 1, B i) = 0 := by
-  change cubeTriLin (B₁, B₁, B i) = 0
+    cubeTriLin (B 1) (B 1) (B i) = 0 := by
+  change cubeTriLin (B₁) (B₁) (B i) = 0
   rw [B₁_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₂_B₂_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 2, B 2, B i) = 0 := by
-  change cubeTriLin (B₂, B₂, B i) = 0
+    cubeTriLin (B 2) (B 2) (B i) = 0 := by
+  change cubeTriLin (B₂) (B₂) (B i) = 0
   rw [B₂_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₃_B₃_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 3, B 3, B i) = 0 := by
-  change cubeTriLin (B₃, B₃, B i) = 0
+    cubeTriLin (B 3) (B 3) (B i) = 0 := by
+  change cubeTriLin (B₃) (B₃) (B i) = 0
   rw [B₃_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₄_B₄_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 4, B 4, B i) = 0 := by
-  change cubeTriLin (B₄, B₄, B i) = 0
+    cubeTriLin (B 4) (B 4) (B i) = 0 := by
+  change cubeTriLin (B₄) (B₄) (B i) = 0
   rw [B₄_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₅_B₅_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 5, B 5, B i) = 0 := by
-  change cubeTriLin (B₅, B₅, B i) = 0
+    cubeTriLin (B 5) (B 5) (B i) = 0 := by
+  change cubeTriLin (B₅) (B₅) (B i) = 0
   rw [B₅_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₆_B₆_Bi_cubic {i : Fin 7} :
-    cubeTriLin (B 6, B 6, B i) = 0 := by
-  change cubeTriLin (B₆, B₆, B i) = 0
+    cubeTriLin (B 6) (B 6) (B i) = 0 := by
+  change cubeTriLin (B₆) (B₆) (B i) = 0
   rw [B₆_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 
 lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
-    cubeTriLin (B i, B i, B j) = 0 := by
+    cubeTriLin (B i) (B i) (B j) = 0 := by
   fin_cases i
   exact B₀_B₀_Bi_cubic
   exact B₁_B₁_Bi_cubic
@@ -259,7 +259,7 @@ lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
   exact B₆_B₆_Bi_cubic
 
 lemma Bi_Bj_Bk_cubic (i j k : Fin 7) :
-    cubeTriLin (B i, B j, B k) = 0 := by
+    cubeTriLin (B i) (B j) (B k) = 0 := by
   by_cases hij : i ≠ j
   exact Bi_Bj_ne_cubic hij (B k)
   simp at hij
@@ -267,7 +267,7 @@ lemma Bi_Bj_Bk_cubic (i j k : Fin 7) :
   exact Bi_Bi_Bj_cubic j k
 
 theorem B_in_accCube (f : Fin 7 → ℚ) : accCube (∑ i, f i • B i) = 0 := by
-  change cubeTriLin _ = 0
+  change cubeTriLin _ _ _ = 0
   rw [cubeTriLin.map_sum₁₂₃]
   apply Fintype.sum_eq_zero
   intro i
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
index c483dcc..c88f6bc 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@@ -91,7 +91,7 @@ lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S
   rfl
 
 lemma on_cubeTriLin (S : (PlusU1 n).charges) :
-    cubeTriLin ((BL n).val, (BL n).val, S) = 9 * accGrav S - 24 * accSU3 S := by
+    cubeTriLin (BL n).val (BL n).val S = 9 * accGrav S - 24 * accSU3 S := by
   erw [familyUniversal_cubeTriLin']
   rw [accGrav_decomp, accSU3_decomp]
   simp only [Fin.isValue, BL₁_val, mul_one, SMνSpecies_numberCharges, toSpecies_apply, mul_neg,
@@ -99,18 +99,18 @@ lemma on_cubeTriLin (S : (PlusU1 n).charges) :
   ring
 
 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
-    cubeTriLin ((BL n).val, (BL n).val, S.val) = 0 := by
+    cubeTriLin (BL n).val (BL n).val S.val = 0 := by
   rw [on_cubeTriLin]
   rw [gravSol S, SU3Sol S]
   simp
 
 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accCube (a • S.val + b • (BL n).val) =
-    a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin (S.val, S.val, (BL n).val)) := by
+    a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin S.val S.val (BL n).val) := by
   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 [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, cubeTriLin_toFun, Fin.isValue,
+  simp only [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, 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 6270cfd..5bf2164 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -90,7 +90,7 @@ lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S
   rfl
 
 lemma on_cubeTriLin (S : (PlusU1 n).charges) :
-    cubeTriLin ((Y n).val, (Y n).val, S) =  6 * accYY S := by
+    cubeTriLin (Y n).val (Y n).val S =  6 * accYY S := by
   erw [familyUniversal_cubeTriLin']
   rw [accYY_decomp]
   simp only [Fin.isValue, Y₁_val, mul_one, SMνSpecies_numberCharges, toSpecies_apply, mul_neg,
@@ -98,13 +98,13 @@ lemma on_cubeTriLin (S : (PlusU1 n).charges) :
   ring
 
 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
-    cubeTriLin ((Y n).val, (Y n).val, S.val) = 0 := by
+    cubeTriLin (Y n).val (Y n).val S.val = 0 := by
   rw [on_cubeTriLin]
   rw [YYsol S]
   simp
 
 lemma on_cubeTriLin' (S : (PlusU1 n).charges) :
-    cubeTriLin ((Y n).val, S, S) =  6 * accQuad S := by
+    cubeTriLin (Y n).val S S =  6 * accQuad S := by
   erw [familyUniversal_cubeTriLin]
   rw [accQuad_decomp]
   simp only [Fin.isValue, Y₁_val, mul_one, SMνSpecies_numberCharges, toSpecies_apply, mul_neg,
@@ -112,18 +112,18 @@ lemma on_cubeTriLin' (S : (PlusU1 n).charges) :
   ring_nf
 
 lemma on_cubeTriLin'_ALQ (S : (PlusU1 n).QuadSols) :
-    cubeTriLin ((Y n).val, S.val, S.val) = 0 := by
+    cubeTriLin (Y n).val S.val S.val = 0 := by
   rw [on_cubeTriLin']
   rw [quadSol S]
   simp
 
 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accCube (a • S.val + b • (Y n).val) =
-    a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin (S.val, S.val, (Y n).val)) := by
+    a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin S.val S.val (Y n).val) := by
   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 [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, cubeTriLin_toFun, Fin.isValue,
+  simp only [HomogeneousCubic, accCube, TriLinearSymm.toCubic_apply, Fin.isValue,
     add_zero, Y_val, mul_zero]
   ring
 
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index 8141d90..11baafc 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -204,8 +204,8 @@ lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i
     cubeTriLin.map_smul₃, cubeTriLin.map_smul₃] at hc
   rw [show accCube B₉ = 9 by rfl] at hc
   rw [show accCube B₁₀ = 1 by rfl] at hc
-  rw [show cubeTriLin (B₉, B₉, B₁₀) = 0 by rfl] at hc
-  rw [show cubeTriLin (B₁₀, B₁₀, B₉) = 0 by rfl] at hc
+  rw [show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl] at hc
+  rw [show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
   simp at hc
   have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by
     ring
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
index e938e7f..da6f205 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@@ -29,7 +29,7 @@ open BigOperators
 variable {n : ℕ}
 /-- A helper function for what follows. -/
 @[simp]
-def α₁ (S : (PlusU1 n).QuadSols) : ℚ := - 3 * cubeTriLin (S.val, S.val, (BL n).val)
+def α₁ (S : (PlusU1 n).QuadSols) : ℚ := - 3 * cubeTriLin S.val S.val (BL n).val
 
 /-- A helper function for what follows. -/
 @[simp]