Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.AnomalyCancellation.Basic

The MSSM with 3 families and RHNs

We define the system of ACCs for the MSSM with 3 families and RHNs. We define the system of charges for 1-species. We prove some basic lemmas about them.

@[expose] public section

The vector space of charges corresponding to the MSSM fermions.

@[simps!]
def MSSMCharges : ACCSystemCharges := ⟨20⟩

The vector spaces of charges of one species of fermions in the MSSM.

@[simps!]
def MSSMSpecies : ACCSystemCharges := ⟨3⟩

lemma sum_MSSMSpecies_numberCharges_eq_expand [AddCommMonoid M]
    (f : Fin MSSMSpecies.numberCharges → M) :
    ∑ i, f i = f ⟨0, byM:Type ?u.3inst✝:AddCommMonoid Mf:Fin MSSMSpecies.numberCharges → M⊢ 0 < MSSMSpecies.numberCharges simpAll goals completed! 🐙⟩ + f ⟨1, byM:Type ?u.3inst✝:AddCommMonoid Mf:Fin MSSMSpecies.numberCharges → M⊢ 1 < MSSMSpecies.numberCharges simpAll goals completed! 🐙⟩ + f ⟨2, byM:Type ?u.3inst✝:AddCommMonoid Mf:Fin MSSMSpecies.numberCharges → M⊢ 2 < MSSMSpecies.numberCharges simpAll goals completed! 🐙⟩ := Fin.sum_univ_three f

An equivalence between MSSMCharges.charges and the space of maps (Fin 18 ⊕ Fin 2 → ℚ). The first 18 factors corresponds to the SM fermions, while the last two are the higgsions.

@[simps!]
def toSMPlusH : MSSMCharges.Charges ≃ (Fin 18 ⊕ Fin 2 → ℚ) :=
  ((@finSumFinEquiv 18 2).arrowCongr (Equiv.refl ℚ)).symm

An equivalence between Fin 18 ⊕ Fin 2 → ℚ and (Fin 18 → ℚ) × (Fin 2 → ℚ).

@[simps!]
def splitSMPlusH : (Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) where
  toFun f := (f ∘ Sum.inl, f ∘ Sum.inr)
  invFun f := Sum.elim f.1 f.2
  left_inv f := Sum.elim_comp_inl_inr f
  right_inv _ := rfl

An equivalence between MSSMCharges.charges and (Fin 18 → ℚ) × (Fin 2 → ℚ). This splits the charges up into the SM and the additional ones for the MSSM.

@[simps!]
def toSplitSMPlusH : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) :=
  toSMPlusH.trans splitSMPlusH

An equivalence between (Fin 18 → ℚ) and (Fin 6 → Fin 3 → ℚ).

@[simps!]
def toSpeciesMaps' : (Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ) :=
  ((Equiv.curry _ _ _).symm.trans
    ((@finProdFinEquiv 6 3).arrowCongr (Equiv.refl ℚ))).symm

An equivalence between MSSMCharges.charges and (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)). This splits charges up into the SM and additional fermions, and further splits the SM into species.

@[simps!]
def toSpecies : MSSMCharges.Charges ≃ (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ) :=
  toSplitSMPlusH.trans (Equiv.prodCongr toSpeciesMaps' (Equiv.refl _))

For a given i ∈ Fin 6 the projection of MSSMCharges.charges down to the corresponding SM species of charges.

@[simps!]
def toSMSpecies (i : Fin 6) : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges where
  toFun S := (Prod.fst ∘ toSpecies) S i
  map_add' _ _ := byi:Fin 6x✝¹:MSSMCharges.Chargesx✝:MSSMCharges.Charges⊢ (Prod.fst ∘ ⇑toSpecies) (x✝¹ + x✝) i = (Prod.fst ∘ ⇑toSpecies) x✝¹ i + (Prod.fst ∘ ⇑toSpecies) x✝ i rflAll goals completed! 🐙
  map_smul' _ _ := byi:Fin 6x✝¹:ℚx✝:MSSMCharges.Charges⊢ (Prod.fst ∘ ⇑toSpecies) (x✝¹ • x✝) i = (RingHom.id ℚ) x✝¹ • (Prod.fst ∘ ⇑toSpecies) x✝ i rflAll goals completed! 🐙

lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) :
    (toSMSpecies i) (toSpecies.symm f) = f.1 i :=
  congrFun (congrArg Prod.fst (toSpecies.apply_symm_apply f)) i

The Q charges as a map Fin 3 → ℚ.

abbrev Q := toSMSpecies 0

The U charges as a map Fin 3 → ℚ.

abbrev U := toSMSpecies 1

The D charges as a map Fin 3 → ℚ.

abbrev D := toSMSpecies 2

The L charges as a map Fin 3 → ℚ.

abbrev L := toSMSpecies 3

The E charges as a map Fin 3 → ℚ.

abbrev E := toSMSpecies 4

The N charges as a map Fin 3 → ℚ.

abbrev N := toSMSpecies 5

The charge Hd.

@[simps!]
def Hd : MSSMCharges.Charges →ₗ[ℚ] ℚ where
  toFun S := S ⟨18, Nat.lt_of_sub_eq_succ rfl⟩
  map_add' _ _ := byx✝¹:MSSMCharges.Chargesx✝:MSSMCharges.Charges⊢ (x✝¹ + x✝) ⟨18, ⋯⟩ = x✝¹ ⟨18, ⋯⟩ + x✝ ⟨18, ⋯⟩ rflAll goals completed! 🐙
  map_smul' _ _ := byx✝¹:ℚx✝:MSSMCharges.Charges⊢ (x✝¹ • x✝) ⟨18, ⋯⟩ = (RingHom.id ℚ) x✝¹ • x✝ ⟨18, ⋯⟩ rflAll goals completed! 🐙

The charge Hu.

@[simps!]
def Hu : MSSMCharges.Charges →ₗ[ℚ] ℚ where
  toFun S := S ⟨19, Nat.lt_of_sub_eq_succ rfl⟩
  map_add' _ _ := byx✝¹:MSSMCharges.Chargesx✝:MSSMCharges.Charges⊢ (x✝¹ + x✝) ⟨19, ⋯⟩ = x✝¹ ⟨19, ⋯⟩ + x✝ ⟨19, ⋯⟩ rflAll goals completed! 🐙
  map_smul' _ _ := byx✝¹:ℚx✝:MSSMCharges.Charges⊢ (x✝¹ • x✝) ⟨19, ⋯⟩ = (RingHom.id ℚ) x✝¹ • x✝ ⟨19, ⋯⟩ rflAll goals completed! 🐙

              lemma charges_eq_toSpecies_eq (S T : MSSMCharges.Charges) :
    S = T ↔ (∀ i, toSMSpecies i S = toSMSpecies i T) ∧ Hd S = Hd T ∧ Hu S = Hu T := byS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ S = T ↔ (∀ (i : Fin 6), (toSMSpecies i) S = (toSMSpecies i) T) ∧ Hd S = Hd T ∧ Hu S = Hu T
  refine ⟨fun h => h ▸ ⟨fun _ => rfl, rfl, rfl⟩, fun h => toSpecies.injective ?_⟩S:MSSMCharges.ChargesT:MSSMCharges.Chargesh:(∀ (i : Fin 6), (toSMSpecies i) S = (toSMSpecies i) T) ∧ Hd S = Hd T ∧ Hu S = Hu T⊢ toSpecies S = toSpecies T
  exact Prod.ext (funext h.1) (funext fun | 0 => h.2.1 | 1 => h.2.2)All goals completed! 🐙lemma Hd_toSpecies_inv (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) :
    Hd (toSpecies.symm f) = f.2 0 := byf:(Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)⊢ Hd (toSpecies.symm f) = f.2 0
  rflAll goals completed! 🐙lemma Hu_toSpecies_inv (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) :
    Hu (toSpecies.symm f) = f.2 1 := byf:(Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)⊢ Hu (toSpecies.symm f) = f.2 1
  rflAll goals completed! 🐙

The gravitational anomaly equation.

def accGrav : MSSMCharges.Charges →ₗ[ℚ] ℚ where
  toFun S := ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i
    + 2 * L S i + E S i + N S i) + 2 * (Hd S + Hu S)
  map_add' S T := byS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i, (6 * Q (S + T) i + 3 * U (S + T) i + 3 * D (S + T) i + 2 * L (S + T) i + E (S + T) i + N (S + T) i) +
    2 * (Hd (S + T) + Hu (S + T)) =
  ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i + N S i) + 2 * (Hd S + Hu S) +
    (∑ i, (6 * Q T i + 3 * U T i + 3 * D T i + 2 * L T i + E T i + N T i) + 2 * (Hd T + Hu T))
    simp only [map_add, ACCSystemCharges.chargesAddCommMonoid_add,
      sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ 6 * (Q S ⟨0, ⋯⟩ + Q T ⟨0, ⋯⟩) + 3 * (U S ⟨0, ⋯⟩ + U T ⟨0, ⋯⟩) + 3 * (D S ⟨0, ⋯⟩ + D T ⟨0, ⋯⟩) +
              2 * (L S ⟨0, ⋯⟩ + L T ⟨0, ⋯⟩) +
            (E S ⟨0, ⋯⟩ + E T ⟨0, ⋯⟩) +
          (N S ⟨0, ⋯⟩ + N T ⟨0, ⋯⟩) +
        (6 * (Q S ⟨1, ⋯⟩ + Q T ⟨1, ⋯⟩) + 3 * (U S ⟨1, ⋯⟩ + U T ⟨1, ⋯⟩) + 3 * (D S ⟨1, ⋯⟩ + D T ⟨1, ⋯⟩) +
              2 * (L S ⟨1, ⋯⟩ + L T ⟨1, ⋯⟩) +
            (E S ⟨1, ⋯⟩ + E T ⟨1, ⋯⟩) +
          (N S ⟨1, ⋯⟩ + N T ⟨1, ⋯⟩)) +
      (6 * (Q S ⟨2, ⋯⟩ + Q T ⟨2, ⋯⟩) + 3 * (U S ⟨2, ⋯⟩ + U T ⟨2, ⋯⟩) + 3 * (D S ⟨2, ⋯⟩ + D T ⟨2, ⋯⟩) +
            2 * (L S ⟨2, ⋯⟩ + L T ⟨2, ⋯⟩) +
          (E S ⟨2, ⋯⟩ + E T ⟨2, ⋯⟩) +
        (N S ⟨2, ⋯⟩ + N T ⟨2, ⋯⟩)) +
    2 * (Hd S + Hd T + (Hu S + Hu T)) =
  6 * Q S ⟨0, ⋯⟩ + 3 * U S ⟨0, ⋯⟩ + 3 * D S ⟨0, ⋯⟩ + 2 * L S ⟨0, ⋯⟩ + E S ⟨0, ⋯⟩ + N S ⟨0, ⋯⟩ +
          (6 * Q S ⟨1, ⋯⟩ + 3 * U S ⟨1, ⋯⟩ + 3 * D S ⟨1, ⋯⟩ + 2 * L S ⟨1, ⋯⟩ + E S ⟨1, ⋯⟩ + N S ⟨1, ⋯⟩) +
        (6 * Q S ⟨2, ⋯⟩ + 3 * U S ⟨2, ⋯⟩ + 3 * D S ⟨2, ⋯⟩ + 2 * L S ⟨2, ⋯⟩ + E S ⟨2, ⋯⟩ + N S ⟨2, ⋯⟩) +
      2 * (Hd S + Hu S) +
    (6 * Q T ⟨0, ⋯⟩ + 3 * U T ⟨0, ⋯⟩ + 3 * D T ⟨0, ⋯⟩ + 2 * L T ⟨0, ⋯⟩ + E T ⟨0, ⋯⟩ + N T ⟨0, ⋯⟩ +
          (6 * Q T ⟨1, ⋯⟩ + 3 * U T ⟨1, ⋯⟩ + 3 * D T ⟨1, ⋯⟩ + 2 * L T ⟨1, ⋯⟩ + E T ⟨1, ⋯⟩ + N T ⟨1, ⋯⟩) +
        (6 * Q T ⟨2, ⋯⟩ + 3 * U T ⟨2, ⋯⟩ + 3 * D T ⟨2, ⋯⟩ + 2 * L T ⟨2, ⋯⟩ + E T ⟨2, ⋯⟩ + N T ⟨2, ⋯⟩) +
      2 * (Hd T + Hu T))
    ringAll goals completed! 🐙
  map_smul' a S := bya:ℚS:MSSMCharges.Charges⊢ ∑ i, (6 * Q (a • S) i + 3 * U (a • S) i + 3 * D (a • S) i + 2 * L (a • S) i + E (a • S) i + N (a • S) i) +
    2 * (Hd (a • S) + Hu (a • S)) =
  (RingHom.id ℚ) a • (∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i + N S i) + 2 * (Hd S + Hu S))
    simp only [map_smul, smul_eq_mul, RingHom.id_apply]a:ℚS:MSSMCharges.Charges⊢ ∑ x, (6 * (a • Q S) x + 3 * (a • U S) x + 3 * (a • D S) x + 2 * (a • L S) x + (a • E S) x + (a • N S) x) +
    2 * (a * Hd S + a * Hu S) =
  a * (∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i + N S i) + 2 * (Hd S + Hu S))
    simp only [HSMul.hSMul, SMul.smul, sum_MSSMSpecies_numberCharges_eq_expand]a:ℚS:MSSMCharges.Charges⊢ 6 * (a * Q S ⟨0, ⋯⟩) + 3 * (a * U S ⟨0, ⋯⟩) + 3 * (a * D S ⟨0, ⋯⟩) + 2 * (a * L S ⟨0, ⋯⟩) + a * E S ⟨0, ⋯⟩ +
          a * N S ⟨0, ⋯⟩ +
        (6 * (a * Q S ⟨1, ⋯⟩) + 3 * (a * U S ⟨1, ⋯⟩) + 3 * (a * D S ⟨1, ⋯⟩) + 2 * (a * L S ⟨1, ⋯⟩) + a * E S ⟨1, ⋯⟩ +
          a * N S ⟨1, ⋯⟩) +
      (6 * (a * Q S ⟨2, ⋯⟩) + 3 * (a * U S ⟨2, ⋯⟩) + 3 * (a * D S ⟨2, ⋯⟩) + 2 * (a * L S ⟨2, ⋯⟩) + a * E S ⟨2, ⋯⟩ +
        a * N S ⟨2, ⋯⟩) +
    2 * (a * Hd S + a * Hu S) =
  a *
    (6 * Q S ⟨0, ⋯⟩ + 3 * U S ⟨0, ⋯⟩ + 3 * D S ⟨0, ⋯⟩ + 2 * L S ⟨0, ⋯⟩ + E S ⟨0, ⋯⟩ + N S ⟨0, ⋯⟩ +
          (6 * Q S ⟨1, ⋯⟩ + 3 * U S ⟨1, ⋯⟩ + 3 * D S ⟨1, ⋯⟩ + 2 * L S ⟨1, ⋯⟩ + E S ⟨1, ⋯⟩ + N S ⟨1, ⋯⟩) +
        (6 * Q S ⟨2, ⋯⟩ + 3 * U S ⟨2, ⋯⟩ + 3 * D S ⟨2, ⋯⟩ + 2 * L S ⟨2, ⋯⟩ + E S ⟨2, ⋯⟩ + N S ⟨2, ⋯⟩) +
      2 * (Hd S + Hu S))
    ringAll goals completed! 🐙

Extensionality lemma for accGrav.

lemma accGrav_ext {S T : MSSMCharges.Charges}
    (hj : ∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T i)
    (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
    accGrav S = accGrav T := byS:MSSMCharges.ChargesT:MSSMCharges.Chargeshj:∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T ihd:Hd S = Hd Thu:Hu S = Hu T⊢ accGrav S = accGrav T
  simp only [accGrav, LinearMap.coe_mk, AddHom.coe_mk, Finset.sum_add_distrib, ← Finset.mul_sum,
    hj, hd, hu]All goals completed! 🐙

The anomaly cancellation condition for SU(2) anomaly.

def accSU2 : MSSMCharges.Charges →ₗ[ℚ] ℚ where
  toFun S := ∑ i, (3 * Q S i + L S i) + Hd S + Hu S
  map_add' S T := byS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i, (3 * Q (S + T) i + L (S + T) i) + Hd (S + T) + Hu (S + T) =
  ∑ i, (3 * Q S i + L S i) + Hd S + Hu S + (∑ i, (3 * Q T i + L T i) + Hd T + Hu T)
    simp only [map_add, ACCSystemCharges.chargesAddCommMonoid_add,
      sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ 3 * (Q S ⟨0, ⋯⟩ + Q T ⟨0, ⋯⟩) + (L S ⟨0, ⋯⟩ + L T ⟨0, ⋯⟩) +
          (3 * (Q S ⟨1, ⋯⟩ + Q T ⟨1, ⋯⟩) + (L S ⟨1, ⋯⟩ + L T ⟨1, ⋯⟩)) +
        (3 * (Q S ⟨2, ⋯⟩ + Q T ⟨2, ⋯⟩) + (L S ⟨2, ⋯⟩ + L T ⟨2, ⋯⟩)) +
      (Hd S + Hd T) +
    (Hu S + Hu T) =
  3 * Q S ⟨0, ⋯⟩ + L S ⟨0, ⋯⟩ + (3 * Q S ⟨1, ⋯⟩ + L S ⟨1, ⋯⟩) + (3 * Q S ⟨2, ⋯⟩ + L S ⟨2, ⋯⟩) + Hd S + Hu S +
    (3 * Q T ⟨0, ⋯⟩ + L T ⟨0, ⋯⟩ + (3 * Q T ⟨1, ⋯⟩ + L T ⟨1, ⋯⟩) + (3 * Q T ⟨2, ⋯⟩ + L T ⟨2, ⋯⟩) + Hd T + Hu T)
    ringAll goals completed! 🐙
  map_smul' a S := bya:ℚS:MSSMCharges.Charges⊢ ∑ i, (3 * Q (a • S) i + L (a • S) i) + Hd (a • S) + Hu (a • S) =
  (RingHom.id ℚ) a • (∑ i, (3 * Q S i + L S i) + Hd S + Hu S)
    simp only [map_smul, smul_eq_mul, RingHom.id_apply]a:ℚS:MSSMCharges.Charges⊢ ∑ x, (3 * (a • Q S) x + (a • L S) x) + a * Hd S + a * Hu S = a * (∑ i, (3 * Q S i + L S i) + Hd S + Hu S)
    simp only [HSMul.hSMul, SMul.smul, sum_MSSMSpecies_numberCharges_eq_expand]a:ℚS:MSSMCharges.Charges⊢ 3 * (a * Q S ⟨0, ⋯⟩) + a * L S ⟨0, ⋯⟩ + (3 * (a * Q S ⟨1, ⋯⟩) + a * L S ⟨1, ⋯⟩) +
        (3 * (a * Q S ⟨2, ⋯⟩) + a * L S ⟨2, ⋯⟩) +
      a * Hd S +
    a * Hu S =
  a * (3 * Q S ⟨0, ⋯⟩ + L S ⟨0, ⋯⟩ + (3 * Q S ⟨1, ⋯⟩ + L S ⟨1, ⋯⟩) + (3 * Q S ⟨2, ⋯⟩ + L S ⟨2, ⋯⟩) + Hd S + Hu S)
    ringAll goals completed! 🐙

Extensionality lemma for accSU2.

lemma accSU2_ext {S T : MSSMCharges.Charges}
    (hj : ∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T i)
    (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
    accSU2 S = accSU2 T := byS:MSSMCharges.ChargesT:MSSMCharges.Chargeshj:∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T ihd:Hd S = Hd Thu:Hu S = Hu T⊢ accSU2 S = accSU2 T
  simp only [accSU2, LinearMap.coe_mk, AddHom.coe_mk, Finset.sum_add_distrib, ← Finset.mul_sum,
    hj, hd, hu]All goals completed! 🐙

The anomaly cancellation condition for SU(3) anomaly.

def accSU3 : MSSMCharges.Charges →ₗ[ℚ] ℚ where
  toFun S := ∑ i, (2 * (Q S i) + (U S i) + (D S i))
  map_add' S T := byS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i, (2 * Q (S + T) i + U (S + T) i + D (S + T) i) = ∑ i, (2 * Q S i + U S i + D S i) + ∑ i, (2 * Q T i + U T i + D T i)
    simp only [map_add, ACCSystemCharges.chargesAddCommMonoid_add,
      sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ 2 * (Q S ⟨0, ⋯⟩ + Q T ⟨0, ⋯⟩) + (U S ⟨0, ⋯⟩ + U T ⟨0, ⋯⟩) + (D S ⟨0, ⋯⟩ + D T ⟨0, ⋯⟩) +
      (2 * (Q S ⟨1, ⋯⟩ + Q T ⟨1, ⋯⟩) + (U S ⟨1, ⋯⟩ + U T ⟨1, ⋯⟩) + (D S ⟨1, ⋯⟩ + D T ⟨1, ⋯⟩)) +
    (2 * (Q S ⟨2, ⋯⟩ + Q T ⟨2, ⋯⟩) + (U S ⟨2, ⋯⟩ + U T ⟨2, ⋯⟩) + (D S ⟨2, ⋯⟩ + D T ⟨2, ⋯⟩)) =
  2 * Q S ⟨0, ⋯⟩ + U S ⟨0, ⋯⟩ + D S ⟨0, ⋯⟩ + (2 * Q S ⟨1, ⋯⟩ + U S ⟨1, ⋯⟩ + D S ⟨1, ⋯⟩) +
      (2 * Q S ⟨2, ⋯⟩ + U S ⟨2, ⋯⟩ + D S ⟨2, ⋯⟩) +
    (2 * Q T ⟨0, ⋯⟩ + U T ⟨0, ⋯⟩ + D T ⟨0, ⋯⟩ + (2 * Q T ⟨1, ⋯⟩ + U T ⟨1, ⋯⟩ + D T ⟨1, ⋯⟩) +
      (2 * Q T ⟨2, ⋯⟩ + U T ⟨2, ⋯⟩ + D T ⟨2, ⋯⟩))
    ringAll goals completed! 🐙
  map_smul' a S := bya:ℚS:MSSMCharges.Charges⊢ ∑ i, (2 * Q (a • S) i + U (a • S) i + D (a • S) i) = (RingHom.id ℚ) a • ∑ i, (2 * Q S i + U S i + D S i)
    simp only [map_smul, smul_eq_mul, RingHom.id_apply]a:ℚS:MSSMCharges.Charges⊢ ∑ x, (2 * (a • Q S) x + (a • U S) x + (a • D S) x) = a * ∑ i, (2 * Q S i + U S i + D S i)
    simp only [HSMul.hSMul, SMul.smul, sum_MSSMSpecies_numberCharges_eq_expand]a:ℚS:MSSMCharges.Charges⊢ 2 * (a * Q S ⟨0, ⋯⟩) + a * U S ⟨0, ⋯⟩ + a * D S ⟨0, ⋯⟩ + (2 * (a * Q S ⟨1, ⋯⟩) + a * U S ⟨1, ⋯⟩ + a * D S ⟨1, ⋯⟩) +
    (2 * (a * Q S ⟨2, ⋯⟩) + a * U S ⟨2, ⋯⟩ + a * D S ⟨2, ⋯⟩) =
  a *
    (2 * Q S ⟨0, ⋯⟩ + U S ⟨0, ⋯⟩ + D S ⟨0, ⋯⟩ + (2 * Q S ⟨1, ⋯⟩ + U S ⟨1, ⋯⟩ + D S ⟨1, ⋯⟩) +
      (2 * Q S ⟨2, ⋯⟩ + U S ⟨2, ⋯⟩ + D S ⟨2, ⋯⟩))
    ringAll goals completed! 🐙

Extensionality lemma for accSU3.

lemma accSU3_ext {S T : MSSMCharges.Charges}
    (hj : ∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T i) :
    accSU3 S = accSU3 T := byS:MSSMCharges.ChargesT:MSSMCharges.Chargeshj:∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T i⊢ accSU3 S = accSU3 T
  simp only [accSU3, LinearMap.coe_mk, AddHom.coe_mk, Finset.sum_add_distrib, ← Finset.mul_sum,
    hj]All goals completed! 🐙

The ACC for Y².

def accYY : MSSMCharges.Charges →ₗ[ℚ] ℚ where
  toFun S := ∑ i, ((Q S) i + 8 * (U S) i + 2 * (D S) i + 3 * (L S) i
    + 6 * (E S) i) + 3 * (Hd S + Hu S)
  map_add' S T := byS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i, (Q (S + T) i + 8 * U (S + T) i + 2 * D (S + T) i + 3 * L (S + T) i + 6 * E (S + T) i) +
    3 * (Hd (S + T) + Hu (S + T)) =
  ∑ i, (Q S i + 8 * U S i + 2 * D S i + 3 * L S i + 6 * E S i) + 3 * (Hd S + Hu S) +
    (∑ i, (Q T i + 8 * U T i + 2 * D T i + 3 * L T i + 6 * E T i) + 3 * (Hd T + Hu T))
    simp only [map_add, ACCSystemCharges.chargesAddCommMonoid_add,
      sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ Q S ⟨0, ⋯⟩ + Q T ⟨0, ⋯⟩ + 8 * (U S ⟨0, ⋯⟩ + U T ⟨0, ⋯⟩) + 2 * (D S ⟨0, ⋯⟩ + D T ⟨0, ⋯⟩) +
            3 * (L S ⟨0, ⋯⟩ + L T ⟨0, ⋯⟩) +
          6 * (E S ⟨0, ⋯⟩ + E T ⟨0, ⋯⟩) +
        (Q S ⟨1, ⋯⟩ + Q T ⟨1, ⋯⟩ + 8 * (U S ⟨1, ⋯⟩ + U T ⟨1, ⋯⟩) + 2 * (D S ⟨1, ⋯⟩ + D T ⟨1, ⋯⟩) +
            3 * (L S ⟨1, ⋯⟩ + L T ⟨1, ⋯⟩) +
          6 * (E S ⟨1, ⋯⟩ + E T ⟨1, ⋯⟩)) +
      (Q S ⟨2, ⋯⟩ + Q T ⟨2, ⋯⟩ + 8 * (U S ⟨2, ⋯⟩ + U T ⟨2, ⋯⟩) + 2 * (D S ⟨2, ⋯⟩ + D T ⟨2, ⋯⟩) +
          3 * (L S ⟨2, ⋯⟩ + L T ⟨2, ⋯⟩) +
        6 * (E S ⟨2, ⋯⟩ + E T ⟨2, ⋯⟩)) +
    3 * (Hd S + Hd T + (Hu S + Hu T)) =
  Q S ⟨0, ⋯⟩ + 8 * U S ⟨0, ⋯⟩ + 2 * D S ⟨0, ⋯⟩ + 3 * L S ⟨0, ⋯⟩ + 6 * E S ⟨0, ⋯⟩ +
          (Q S ⟨1, ⋯⟩ + 8 * U S ⟨1, ⋯⟩ + 2 * D S ⟨1, ⋯⟩ + 3 * L S ⟨1, ⋯⟩ + 6 * E S ⟨1, ⋯⟩) +
        (Q S ⟨2, ⋯⟩ + 8 * U S ⟨2, ⋯⟩ + 2 * D S ⟨2, ⋯⟩ + 3 * L S ⟨2, ⋯⟩ + 6 * E S ⟨2, ⋯⟩) +
      3 * (Hd S + Hu S) +
    (Q T ⟨0, ⋯⟩ + 8 * U T ⟨0, ⋯⟩ + 2 * D T ⟨0, ⋯⟩ + 3 * L T ⟨0, ⋯⟩ + 6 * E T ⟨0, ⋯⟩ +
          (Q T ⟨1, ⋯⟩ + 8 * U T ⟨1, ⋯⟩ + 2 * D T ⟨1, ⋯⟩ + 3 * L T ⟨1, ⋯⟩ + 6 * E T ⟨1, ⋯⟩) +
        (Q T ⟨2, ⋯⟩ + 8 * U T ⟨2, ⋯⟩ + 2 * D T ⟨2, ⋯⟩ + 3 * L T ⟨2, ⋯⟩ + 6 * E T ⟨2, ⋯⟩) +
      3 * (Hd T + Hu T))
    ringAll goals completed! 🐙
  map_smul' a S := bya:ℚS:MSSMCharges.Charges⊢ ∑ i, (Q (a • S) i + 8 * U (a • S) i + 2 * D (a • S) i + 3 * L (a • S) i + 6 * E (a • S) i) +
    3 * (Hd (a • S) + Hu (a • S)) =
  (RingHom.id ℚ) a • (∑ i, (Q S i + 8 * U S i + 2 * D S i + 3 * L S i + 6 * E S i) + 3 * (Hd S + Hu S))
    simp only [map_smul, smul_eq_mul, RingHom.id_apply]a:ℚS:MSSMCharges.Charges⊢ ∑ x, ((a • Q S) x + 8 * (a • U S) x + 2 * (a • D S) x + 3 * (a • L S) x + 6 * (a • E S) x) + 3 * (a * Hd S + a * Hu S) =
  a * (∑ i, (Q S i + 8 * U S i + 2 * D S i + 3 * L S i + 6 * E S i) + 3 * (Hd S + Hu S))
    simp only [HSMul.hSMul, SMul.smul, sum_MSSMSpecies_numberCharges_eq_expand]a:ℚS:MSSMCharges.Charges⊢ a * Q S ⟨0, ⋯⟩ + 8 * (a * U S ⟨0, ⋯⟩) + 2 * (a * D S ⟨0, ⋯⟩) + 3 * (a * L S ⟨0, ⋯⟩) + 6 * (a * E S ⟨0, ⋯⟩) +
        (a * Q S ⟨1, ⋯⟩ + 8 * (a * U S ⟨1, ⋯⟩) + 2 * (a * D S ⟨1, ⋯⟩) + 3 * (a * L S ⟨1, ⋯⟩) + 6 * (a * E S ⟨1, ⋯⟩)) +
      (a * Q S ⟨2, ⋯⟩ + 8 * (a * U S ⟨2, ⋯⟩) + 2 * (a * D S ⟨2, ⋯⟩) + 3 * (a * L S ⟨2, ⋯⟩) + 6 * (a * E S ⟨2, ⋯⟩)) +
    3 * (a * Hd S + a * Hu S) =
  a *
    (Q S ⟨0, ⋯⟩ + 8 * U S ⟨0, ⋯⟩ + 2 * D S ⟨0, ⋯⟩ + 3 * L S ⟨0, ⋯⟩ + 6 * E S ⟨0, ⋯⟩ +
          (Q S ⟨1, ⋯⟩ + 8 * U S ⟨1, ⋯⟩ + 2 * D S ⟨1, ⋯⟩ + 3 * L S ⟨1, ⋯⟩ + 6 * E S ⟨1, ⋯⟩) +
        (Q S ⟨2, ⋯⟩ + 8 * U S ⟨2, ⋯⟩ + 2 * D S ⟨2, ⋯⟩ + 3 * L S ⟨2, ⋯⟩ + 6 * E S ⟨2, ⋯⟩) +
      3 * (Hd S + Hu S))
    ringAll goals completed! 🐙

Extensionality lemma for accGrav.

lemma accYY_ext {S T : MSSMCharges.Charges}
    (hj : ∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T i)
    (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
    accYY S = accYY T := byS:MSSMCharges.ChargesT:MSSMCharges.Chargeshj:∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i = ∑ i, (toSMSpecies j) T ihd:Hd S = Hd Thu:Hu S = Hu T⊢ accYY S = accYY T
  simp only [accYY, LinearMap.coe_mk, AddHom.coe_mk, Finset.sum_add_distrib, ← Finset.mul_sum,
    hj, hd, hu]All goals completed! 🐙

The symmetric bilinear function used to define the quadratic ACC.


@[simps!]
def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂
  (fun (S, T) => ∑ i, (Q S i * Q T i + (- 2) * (U S i * U T i) +
    D S i * D T i + (- 1) * (L S i * L T i) + E S i * E T i) +
    (- Hd S * Hd T + Hu S * Hu T))
  (by⊢ ∀ (a : ℚ) (S T : MSSMCharges.Charges),
  (match (a • S, T) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)) =
    a *
      match (S, T) with
      | (S, T) =>
        ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
          (-Hd S * Hd T + Hu S * Hu T)
    intro a S Ta:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (match (a • S, T) with
  | (S, T) =>
    ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
      (-Hd S * Hd T + Hu S * Hu T)) =
  a *
    match (S, T) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)
    simp onlya:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
      (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
        E (a • S) i * E T i) +
    (-Hd (a • S) * Hd T + Hu (a • S) * Hu T) =
  a *
    (∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
      (-Hd S * Hd T + Hu S * Hu T))
    rw [mul_adda:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
      (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
        E (a • S) i * E T i) +
    (-Hd (a • S) * Hd T + Hu (a • S) * Hu T) =
  a * ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
    a * (-Hd S * Hd T + Hu S * Hu T)a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
      (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
        E (a • S) i * E T i) +
    (-Hd (a • S) * Hd T + Hu (a • S) * Hu T) =
  a * ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
    a * (-Hd S * Hd T + Hu S * Hu T)]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
      (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
        E (a • S) i * E T i) +
    (-Hd (a • S) * Hd T + Hu (a • S) * Hu T) =
  a * ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
    a * (-Hd S * Hd T + Hu S * Hu T)
    congr 1e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
    (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
      E (a • S) i * E T i) =
  a * ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ -Hd (a • S) * Hd T + Hu (a • S) * Hu T = a * (-Hd S * Hd T + Hu S * Hu T)
    ·e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
    (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
      E (a • S) i * E T i) =
  a * ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) rw [Finset.mul_sume_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
    (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
      E (a • S) i * E T i) =
  ∑ i, a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
    (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
      E (a • S) i * E T i) =
  ∑ i, a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)]e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
    (Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
      E (a • S) i * E T i) =
  ∑ i, a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)
      apply Fintype.sum_congre_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∀ (a_1 : Fin MSSMSpecies.numberCharges),
  Q (a • S) a_1 * Q T a_1 + -2 * (U (a • S) a_1 * U T a_1) + D (a • S) a_1 * D T a_1 + -1 * (L (a • S) a_1 * L T a_1) +
      E (a • S) a_1 * E T a_1 =
    a *
      (Q S a_1 * Q T a_1 + -2 * (U S a_1 * U T a_1) + D S a_1 * D T a_1 + -1 * (L S a_1 * L T a_1) + E S a_1 * E T a_1)
      intro ie_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ Q (a • S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
    E (a • S) i * E T i =
  a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)
      repeat rw [map_smule_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (a • Q S) i * Q T i + -2 * (U (a • S) i * U T i) + D (a • S) i * D T i + -1 * (L (a • S) i * L T i) +
    E (a • S) i * E T i =
  a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (a • Q S) i * Q T i + -2 * ((a • U S) i * U T i) + (a • D S) i * D T i + -1 * ((a • L S) i * L T i) +
    (a • E S) i * E T i =
  a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)]e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (a • Q S) i * Q T i + -2 * ((a • U S) i * U T i) + (a • D S) i * D T i + -1 * ((a • L S) i * L T i) +
    E (a • S) i * E T i =
  a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (a • Q S) i * Q T i + -2 * ((a • U S) i * U T i) + (a • D S) i * D T i + -1 * ((a • L S) i * L T i) +
    (a • E S) i * E T i =
  a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (a • Q S) i * Q T i + -2 * ((a • U S) i * U T i) + (a • D S) i * D T i + -1 * ((a • L S) i * L T i) +
    (a • E S) i * E T i =
  a * (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i)
      simp only [HSMul.hSMul, SMul.smul, toSMSpecies_apply, Fin.isValue, neg_mul, one_mul]e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ a * S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * T (Fin.castAdd 2 (finProdFinEquiv (0, i))) +
          -(2 * (a * S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * T (Fin.castAdd 2 (finProdFinEquiv (1, i))))) +
        a * S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * T (Fin.castAdd 2 (finProdFinEquiv (2, i))) +
      -(a * S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * T (Fin.castAdd 2 (finProdFinEquiv (3, i)))) +
    a * S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * T (Fin.castAdd 2 (finProdFinEquiv (4, i))) =
  a *
    (S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * T (Fin.castAdd 2 (finProdFinEquiv (0, i))) +
            -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * T (Fin.castAdd 2 (finProdFinEquiv (1, i))))) +
          S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * T (Fin.castAdd 2 (finProdFinEquiv (2, i))) +
        -(S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * T (Fin.castAdd 2 (finProdFinEquiv (3, i)))) +
      S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * T (Fin.castAdd 2 (finProdFinEquiv (4, i))))
      ringAll goals completed! 🐙
    ·e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ -Hd (a • S) * Hd T + Hu (a • S) * Hu T = a * (-Hd S * Hd T + Hu S * Hu T) simp only [map_smul, Hd_apply, Fin.reduceFinMk, Fin.isValue, smul_eq_mul, neg_mul, Hu_apply]e_aa:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ -(a * S 18 * T 18) + a * S 19 * T 19 = a * (-(S 18 * T 18) + S 19 * T 19)
      ringAll goals completed! 🐙)
  (by⊢ ∀ (S1 S2 T : MSSMCharges.Charges),
  (match (S1 + S2, T) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)) =
    (match (S1, T) with
      | (S, T) =>
        ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
          (-Hd S * Hd T + Hu S * Hu T)) +
      match (S2, T) with
      | (S, T) =>
        ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
          (-Hd S * Hd T + Hu S * Hu T)
    intro S T RS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ (match (S + T, R) with
  | (S, T) =>
    ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
      (-Hd S * Hd T + Hu S * Hu T)) =
  (match (S, R) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)) +
    match (T, R) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)
    simp onlyS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
      (-Hd S * Hd R + Hu S * Hu R) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd T * Hd R + Hu T * Hu R))
    rw [add_assoc,S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R +
      (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
        (-Hd T * Hd R + Hu T * Hu R)))S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R +
        ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd T * Hd R + Hu T * Hu R)) ← add_assoc (-Hd S * Hd R + Hu S * Hu R) _ _S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R +
        ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd T * Hd R + Hu T * Hu R))S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R +
        ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd T * Hd R + Hu T * Hu R))]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R +
        ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd T * Hd R + Hu T * Hu R))
    rw [add_comm (-Hd S * Hd R + Hu S * Hu R) _S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
        (-Hd S * Hd R + Hu S * Hu R) +
      (-Hd T * Hd R + Hu T * Hu R))S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
        (-Hd S * Hd R + Hu S * Hu R) +
      (-Hd T * Hd R + Hu T * Hu R))]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
        (-Hd S * Hd R + Hu S * Hu R) +
      (-Hd T * Hd R + Hu T * Hu R))
    rw [add_assocS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)))S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)))]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    (∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
      (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)))
    rw [← add_assoc _ _ (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R))S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
      ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R))S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
      ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R))]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
      (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
        E (S + T) i * E R i) +
    (-Hd (S + T) * Hd R + Hu (S + T) * Hu R) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
      ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) +
    (-Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R))
    congr 1e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
    (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
      E (S + T) i * E R i) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -Hd (S + T) * Hd R + Hu (S + T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)
    ·e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
    (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
      E (S + T) i * E R i) =
  ∑ i, (Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i) +
    ∑ i, (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i) rw [← Finset.sum_add_distribe_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
    (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
      E (S + T) i * E R i) =
  ∑ x,
    (Q S x * Q R x + -2 * (U S x * U R x) + D S x * D R x + -1 * (L S x * L R x) + E S x * E R x +
      (Q T x * Q R x + -2 * (U T x * U R x) + D T x * D R x + -1 * (L T x * L R x) + E T x * E R x))e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
    (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
      E (S + T) i * E R i) =
  ∑ x,
    (Q S x * Q R x + -2 * (U S x * U R x) + D S x * D R x + -1 * (L S x * L R x) + E S x * E R x +
      (Q T x * Q R x + -2 * (U T x * U R x) + D T x * D R x + -1 * (L T x * L R x) + E T x * E R x))]e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ i,
    (Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
      E (S + T) i * E R i) =
  ∑ x,
    (Q S x * Q R x + -2 * (U S x * U R x) + D S x * D R x + -1 * (L S x * L R x) + E S x * E R x +
      (Q T x * Q R x + -2 * (U T x * U R x) + D T x * D R x + -1 * (L T x * L R x) + E T x * E R x))
      apply Fintype.sum_congre_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∀ (a : Fin MSSMSpecies.numberCharges),
  Q (S + T) a * Q R a + -2 * (U (S + T) a * U R a) + D (S + T) a * D R a + -1 * (L (S + T) a * L R a) +
      E (S + T) a * E R a =
    Q S a * Q R a + -2 * (U S a * U R a) + D S a * D R a + -1 * (L S a * L R a) + E S a * E R a +
      (Q T a * Q R a + -2 * (U T a * U R a) + D T a * D R a + -1 * (L T a * L R a) + E T a * E R a)
      intro ie_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ Q (S + T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
    E (S + T) i * E R i =
  Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
    (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)
      repeat rw [map_adde_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (Q S + Q T) i * Q R i + -2 * (U (S + T) i * U R i) + D (S + T) i * D R i + -1 * (L (S + T) i * L R i) +
    E (S + T) i * E R i =
  Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
    (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (Q S + Q T) i * Q R i + -2 * ((U S + U T) i * U R i) + (D S + D T) i * D R i + -1 * ((L S + L T) i * L R i) +
    (E S + E T) i * E R i =
  Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
    (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)]e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (Q S + Q T) i * Q R i + -2 * ((U S + U T) i * U R i) + (D S + D T) i * D R i + -1 * ((L S + L T) i * L R i) +
    E (S + T) i * E R i =
  Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
    (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (Q S + Q T) i * Q R i + -2 * ((U S + U T) i * U R i) + (D S + D T) i * D R i + -1 * ((L S + L T) i * L R i) +
    (E S + E T) i * E R i =
  Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
    (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (Q S + Q T) i * Q R i + -2 * ((U S + U T) i * U R i) + (D S + D T) i * D R i + -1 * ((L S + L T) i * L R i) +
    (E S + E T) i * E R i =
  Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
    (Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)
      simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSMSpecies_apply, Fin.isValue, neg_mul,
        one_mul]e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Chargesi:Fin MSSMSpecies.numberCharges⊢ (S (Fin.castAdd 2 (finProdFinEquiv (0, i))) + T (Fin.castAdd 2 (finProdFinEquiv (0, i)))) *
            R (Fin.castAdd 2 (finProdFinEquiv (0, i))) +
          -(2 *
              ((S (Fin.castAdd 2 (finProdFinEquiv (1, i))) + T (Fin.castAdd 2 (finProdFinEquiv (1, i)))) *
                R (Fin.castAdd 2 (finProdFinEquiv (1, i))))) +
        (S (Fin.castAdd 2 (finProdFinEquiv (2, i))) + T (Fin.castAdd 2 (finProdFinEquiv (2, i)))) *
          R (Fin.castAdd 2 (finProdFinEquiv (2, i))) +
      -((S (Fin.castAdd 2 (finProdFinEquiv (3, i))) + T (Fin.castAdd 2 (finProdFinEquiv (3, i)))) *
          R (Fin.castAdd 2 (finProdFinEquiv (3, i)))) +
    (S (Fin.castAdd 2 (finProdFinEquiv (4, i))) + T (Fin.castAdd 2 (finProdFinEquiv (4, i)))) *
      R (Fin.castAdd 2 (finProdFinEquiv (4, i))) =
  S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * R (Fin.castAdd 2 (finProdFinEquiv (0, i))) +
            -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * R (Fin.castAdd 2 (finProdFinEquiv (1, i))))) +
          S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * R (Fin.castAdd 2 (finProdFinEquiv (2, i))) +
        -(S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * R (Fin.castAdd 2 (finProdFinEquiv (3, i)))) +
      S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * R (Fin.castAdd 2 (finProdFinEquiv (4, i))) +
    (T (Fin.castAdd 2 (finProdFinEquiv (0, i))) * R (Fin.castAdd 2 (finProdFinEquiv (0, i))) +
            -(2 * (T (Fin.castAdd 2 (finProdFinEquiv (1, i))) * R (Fin.castAdd 2 (finProdFinEquiv (1, i))))) +
          T (Fin.castAdd 2 (finProdFinEquiv (2, i))) * R (Fin.castAdd 2 (finProdFinEquiv (2, i))) +
        -(T (Fin.castAdd 2 (finProdFinEquiv (3, i))) * R (Fin.castAdd 2 (finProdFinEquiv (3, i)))) +
      T (Fin.castAdd 2 (finProdFinEquiv (4, i))) * R (Fin.castAdd 2 (finProdFinEquiv (4, i))))
      ringAll goals completed! 🐙
    ·e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -Hd (S + T) * Hd R + Hu (S + T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R) rw [Hd.map_add,e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -(Hd S + Hd T) * Hd R + Hu (S + T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -(Hd S + Hd T) * Hd R + (Hu S + Hu T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R) Hu.map_adde_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -(Hd S + Hd T) * Hd R + (Hu S + Hu T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -(Hd S + Hd T) * Hd R + (Hu S + Hu T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)]e_aS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ -(Hd S + Hd T) * Hd R + (Hu S + Hu T) * Hu R = -Hd S * Hd R + Hu S * Hu R + (-Hd T * Hd R + Hu T * Hu R)
      ringAll goals completed! 🐙)
  (by⊢ ∀ (S T : MSSMCharges.Charges),
  (match (S, T) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)) =
    match (T, S) with
    | (S, T) =>
      ∑ i, (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (L S i * L T i) + E S i * E T i) +
        (-Hd S * Hd T + Hu S * Hu T)
    intro S LS:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ (match (S, L) with
  | (S, T) =>
    ∑ i,
        (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (MSSMCharges.L S i * MSSMCharges.L T i) +
          E S i * E T i) +
      (-Hd S * Hd T + Hu S * Hu T)) =
  match (L, S) with
  | (S, T) =>
    ∑ i,
        (Q S i * Q T i + -2 * (U S i * U T i) + D S i * D T i + -1 * (MSSMCharges.L S i * MSSMCharges.L T i) +
          E S i * E T i) +
      (-Hd S * Hd T + Hu S * Hu T)
    simp only [toSMSpecies_apply, Fin.isValue, neg_mul, one_mul, Hd_apply, Fin.reduceFinMk,
      Hu_apply]S:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ ∑ x,
      (S (Fin.castAdd 2 (finProdFinEquiv (0, x))) * L (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
              -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, x))) * L (Fin.castAdd 2 (finProdFinEquiv (1, x))))) +
            S (Fin.castAdd 2 (finProdFinEquiv (2, x))) * L (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
          -(S (Fin.castAdd 2 (finProdFinEquiv (3, x))) * L (Fin.castAdd 2 (finProdFinEquiv (3, x)))) +
        S (Fin.castAdd 2 (finProdFinEquiv (4, x))) * L (Fin.castAdd 2 (finProdFinEquiv (4, x)))) +
    (-(S 18 * L 18) + S 19 * L 19) =
  ∑ x,
      (L (Fin.castAdd 2 (finProdFinEquiv (0, x))) * S (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
              -(2 * (L (Fin.castAdd 2 (finProdFinEquiv (1, x))) * S (Fin.castAdd 2 (finProdFinEquiv (1, x))))) +
            L (Fin.castAdd 2 (finProdFinEquiv (2, x))) * S (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
          -(L (Fin.castAdd 2 (finProdFinEquiv (3, x))) * S (Fin.castAdd 2 (finProdFinEquiv (3, x)))) +
        L (Fin.castAdd 2 (finProdFinEquiv (4, x))) * S (Fin.castAdd 2 (finProdFinEquiv (4, x)))) +
    (-(L 18 * S 18) + L 19 * S 19)
    congr 1e_aS:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ ∑ x,
    (S (Fin.castAdd 2 (finProdFinEquiv (0, x))) * L (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
            -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, x))) * L (Fin.castAdd 2 (finProdFinEquiv (1, x))))) +
          S (Fin.castAdd 2 (finProdFinEquiv (2, x))) * L (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
        -(S (Fin.castAdd 2 (finProdFinEquiv (3, x))) * L (Fin.castAdd 2 (finProdFinEquiv (3, x)))) +
      S (Fin.castAdd 2 (finProdFinEquiv (4, x))) * L (Fin.castAdd 2 (finProdFinEquiv (4, x)))) =
  ∑ x,
    (L (Fin.castAdd 2 (finProdFinEquiv (0, x))) * S (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
            -(2 * (L (Fin.castAdd 2 (finProdFinEquiv (1, x))) * S (Fin.castAdd 2 (finProdFinEquiv (1, x))))) +
          L (Fin.castAdd 2 (finProdFinEquiv (2, x))) * S (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
        -(L (Fin.castAdd 2 (finProdFinEquiv (3, x))) * S (Fin.castAdd 2 (finProdFinEquiv (3, x)))) +
      L (Fin.castAdd 2 (finProdFinEquiv (4, x))) * S (Fin.castAdd 2 (finProdFinEquiv (4, x))))e_aS:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ -(S 18 * L 18) + S 19 * L 19 = -(L 18 * S 18) + L 19 * S 19
    ·e_aS:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ ∑ x,
    (S (Fin.castAdd 2 (finProdFinEquiv (0, x))) * L (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
            -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, x))) * L (Fin.castAdd 2 (finProdFinEquiv (1, x))))) +
          S (Fin.castAdd 2 (finProdFinEquiv (2, x))) * L (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
        -(S (Fin.castAdd 2 (finProdFinEquiv (3, x))) * L (Fin.castAdd 2 (finProdFinEquiv (3, x)))) +
      S (Fin.castAdd 2 (finProdFinEquiv (4, x))) * L (Fin.castAdd 2 (finProdFinEquiv (4, x)))) =
  ∑ x,
    (L (Fin.castAdd 2 (finProdFinEquiv (0, x))) * S (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
            -(2 * (L (Fin.castAdd 2 (finProdFinEquiv (1, x))) * S (Fin.castAdd 2 (finProdFinEquiv (1, x))))) +
          L (Fin.castAdd 2 (finProdFinEquiv (2, x))) * S (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
        -(L (Fin.castAdd 2 (finProdFinEquiv (3, x))) * S (Fin.castAdd 2 (finProdFinEquiv (3, x)))) +
      L (Fin.castAdd 2 (finProdFinEquiv (4, x))) * S (Fin.castAdd 2 (finProdFinEquiv (4, x)))) simp only [reduceMul, Fin.isValue, sum_MSSMSpecies_numberCharges_eq_expand]e_aS:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨0, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (0, ⟨0, ⋯⟩))) +
              -(2 *
                  (S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨0, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (1, ⟨0, ⋯⟩))))) +
            S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨0, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (2, ⟨0, ⋯⟩))) +
          -(S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨0, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (3, ⟨0, ⋯⟩)))) +
        S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨0, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (4, ⟨0, ⋯⟩))) +
      (S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨1, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (0, ⟨1, ⋯⟩))) +
              -(2 *
                  (S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨1, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (1, ⟨1, ⋯⟩))))) +
            S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨1, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (2, ⟨1, ⋯⟩))) +
          -(S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨1, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (3, ⟨1, ⋯⟩)))) +
        S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨1, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (4, ⟨1, ⋯⟩)))) +
    (S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
            -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))))) +
          S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
        -(S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩)))) +
      S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * L (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩)))) =
  L (Fin.castAdd 2 (finProdFinEquiv (0, ⟨0, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨0, ⋯⟩))) +
              -(2 *
                  (L (Fin.castAdd 2 (finProdFinEquiv (1, ⟨0, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨0, ⋯⟩))))) +
            L (Fin.castAdd 2 (finProdFinEquiv (2, ⟨0, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨0, ⋯⟩))) +
          -(L (Fin.castAdd 2 (finProdFinEquiv (3, ⟨0, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨0, ⋯⟩)))) +
        L (Fin.castAdd 2 (finProdFinEquiv (4, ⟨0, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨0, ⋯⟩))) +
      (L (Fin.castAdd 2 (finProdFinEquiv (0, ⟨1, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨1, ⋯⟩))) +
              -(2 *
                  (L (Fin.castAdd 2 (finProdFinEquiv (1, ⟨1, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨1, ⋯⟩))))) +
            L (Fin.castAdd 2 (finProdFinEquiv (2, ⟨1, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨1, ⋯⟩))) +
          -(L (Fin.castAdd 2 (finProdFinEquiv (3, ⟨1, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨1, ⋯⟩)))) +
        L (Fin.castAdd 2 (finProdFinEquiv (4, ⟨1, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨1, ⋯⟩)))) +
    (L (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
            -(2 * (L (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))))) +
          L (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
        -(L (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩)))) +
      L (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))))
      ringAll goals completed! 🐙
    ·e_aS:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ -(S 18 * L 18) + S 19 * L 19 = -(L 18 * S 18) + L 19 * S 19 ringAll goals completed! 🐙)

The quadratic ACC.

@[simp]
def accQuad : HomogeneousQuadratic MSSMCharges.Charges := quadBiLin.toHomogeneousQuad

Extensionality lemma for accQuad.

set_option backward.isDefEq.respectTransparency false in

lemma accQuad_ext {S T : (MSSMCharges).Charges}
    (h : ∀ j, ∑ i, ((fun a => a^2) ∘ toSMSpecies j S) i =
    ∑ i, ((fun a => a^2) ∘ toSMSpecies j T) i)
    (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
    accQuad S = accQuad T := byS:MSSMCharges.ChargesT:MSSMCharges.Chargesh:∀ (j : Fin 6), ∑ i, ((fun a => a ^ 2) ∘ (toSMSpecies j) S) i = ∑ i, ((fun a => a ^ 2) ∘ (toSMSpecies j) T) ihd:Hd S = Hd Thu:Hu S = Hu T⊢ accQuad S = accQuad T
  have h1 : ∀ j, ∑ i, (toSMSpecies j S i)^2 = ∑ i, (toSMSpecies j T i)^2 := hS:MSSMCharges.ChargesT:MSSMCharges.Chargesh:∀ (j : Fin 6), ∑ i, ((fun a => a ^ 2) ∘ (toSMSpecies j) S) i = ∑ i, ((fun a => a ^ 2) ∘ (toSMSpecies j) T) ihd:Hd S = Hd Thu:Hu S = Hu Th1:∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i ^ 2 = ∑ i, (toSMSpecies j) T i ^ 2⊢ accQuad S = accQuad T
  simp only [HomogeneousQuadratic, accQuad, BiLinearSymm.toHomogeneousQuad_apply, quadBiLin,
    BiLinearSymm.mk₂_toFun_apply, ← pow_two, Finset.sum_add_distrib, ← Finset.mul_sum, h1, hd, hu]All goals completed! 🐙

The function underlying the symmetric trilinear form used to define the cubic ACC.

def cubeTriLinToFun
    (S : MSSMCharges.Charges × MSSMCharges.Charges × MSSMCharges.Charges) : ℚ :=
  ∑ 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)
    + (2 * Hd S.1 * Hd S.2.1 * Hd S.2.2
    + 2 * Hu S.1 * Hu S.2.1 * Hu S.2.2)

              lemma cubeTriLinToFun_map_smul₁ (a : ℚ) (S T R : MSSMCharges.Charges) :
    cubeTriLinToFun (a • S, T, R) = a * cubeTriLinToFun (S, T, R) := bya:ℚS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ cubeTriLinToFun (a • S, T, R) = a * cubeTriLinToFun (S, T, R)
  simp only [cubeTriLinToFun, map_smul, smul_eq_mul]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ ∑ x,
      (6 * ((a • Q S) x * Q T x * Q R x) + 3 * ((a • U S) x * U T x * U R x) + 3 * ((a • D S) x * D T x * D R x) +
            2 * ((a • L S) x * L T x * L R x) +
          (a • E S) x * E T x * E R x +
        (a • N S) x * N T x * N R x) +
    (2 * (a * Hd S) * Hd T * Hd R + 2 * (a * Hu S) * Hu T * Hu R) =
  a *
    (∑ x,
        (6 * (Q S x * Q T x * Q R x) + 3 * (U S x * U T x * U R x) + 3 * (D S x * D T x * D R x) +
              2 * (L S x * L T x * L R x) +
            E S x * E T x * E R x +
          N S x * N T x * N R x) +
      (2 * Hd S * Hd T * Hd R + 2 * Hu S * Hu T * Hu R))
  simp only [HSMul.hSMul, SMul.smul, sum_MSSMSpecies_numberCharges_eq_expand]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ 6 * (a * Q S ⟨0, ⋯⟩ * Q T ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩) + 3 * (a * U S ⟨0, ⋯⟩ * U T ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩) +
                3 * (a * D S ⟨0, ⋯⟩ * D T ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩) +
              2 * (a * L S ⟨0, ⋯⟩ * L T ⟨0, ⋯⟩ * L R ⟨0, ⋯⟩) +
            a * E S ⟨0, ⋯⟩ * E T ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ +
          a * N S ⟨0, ⋯⟩ * N T ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ +
        (6 * (a * Q S ⟨1, ⋯⟩ * Q T ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩) + 3 * (a * U S ⟨1, ⋯⟩ * U T ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩) +
                3 * (a * D S ⟨1, ⋯⟩ * D T ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩) +
              2 * (a * L S ⟨1, ⋯⟩ * L T ⟨1, ⋯⟩ * L R ⟨1, ⋯⟩) +
            a * E S ⟨1, ⋯⟩ * E T ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ +
          a * N S ⟨1, ⋯⟩ * N T ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩) +
      (6 * (a * Q S ⟨2, ⋯⟩ * Q T ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩) + 3 * (a * U S ⟨2, ⋯⟩ * U T ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩) +
              3 * (a * D S ⟨2, ⋯⟩ * D T ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩) +
            2 * (a * L S ⟨2, ⋯⟩ * L T ⟨2, ⋯⟩ * L R ⟨2, ⋯⟩) +
          a * E S ⟨2, ⋯⟩ * E T ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ +
        a * N S ⟨2, ⋯⟩ * N T ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩) +
    (2 * (a * Hd S) * Hd T * Hd R + 2 * (a * Hu S) * Hu T * Hu R) =
  a *
    (6 * (Q S ⟨0, ⋯⟩ * Q T ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩) + 3 * (U S ⟨0, ⋯⟩ * U T ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩) +
                  3 * (D S ⟨0, ⋯⟩ * D T ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩) +
                2 * (L S ⟨0, ⋯⟩ * L T ⟨0, ⋯⟩ * L R ⟨0, ⋯⟩) +
              E S ⟨0, ⋯⟩ * E T ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ +
            N S ⟨0, ⋯⟩ * N T ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ +
          (6 * (Q S ⟨1, ⋯⟩ * Q T ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩) + 3 * (U S ⟨1, ⋯⟩ * U T ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩) +
                  3 * (D S ⟨1, ⋯⟩ * D T ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩) +
                2 * (L S ⟨1, ⋯⟩ * L T ⟨1, ⋯⟩ * L R ⟨1, ⋯⟩) +
              E S ⟨1, ⋯⟩ * E T ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ +
            N S ⟨1, ⋯⟩ * N T ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩) +
        (6 * (Q S ⟨2, ⋯⟩ * Q T ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩) + 3 * (U S ⟨2, ⋯⟩ * U T ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩) +
                3 * (D S ⟨2, ⋯⟩ * D T ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩) +
              2 * (L S ⟨2, ⋯⟩ * L T ⟨2, ⋯⟩ * L R ⟨2, ⋯⟩) +
            E S ⟨2, ⋯⟩ * E T ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ +
          N S ⟨2, ⋯⟩ * N T ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩) +
      (2 * Hd S * Hd T * Hd R + 2 * Hu S * Hu T * Hu R))
  ringAll goals completed! 🐙lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
    cubeTriLinToFun (S + T, R, L) = cubeTriLinToFun (S, R, L) + cubeTriLinToFun (T, R, L) := byS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ cubeTriLinToFun (S + T, R, L) = cubeTriLinToFun (S, R, L) + cubeTriLinToFun (T, R, L)
  simp only [cubeTriLinToFun, map_add, ACCSystemCharges.chargesAddCommMonoid_add,
    sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.ChargesL:MSSMCharges.Charges⊢ 6 * ((Q S ⟨0, ⋯⟩ + Q T ⟨0, ⋯⟩) * Q R ⟨0, ⋯⟩ * Q L ⟨0, ⋯⟩) + 3 * ((U S ⟨0, ⋯⟩ + U T ⟨0, ⋯⟩) * U R ⟨0, ⋯⟩ * U L ⟨0, ⋯⟩) +
                3 * ((D S ⟨0, ⋯⟩ + D T ⟨0, ⋯⟩) * D R ⟨0, ⋯⟩ * D L ⟨0, ⋯⟩) +
              2 *
                ((MSSMCharges.L S ⟨0, ⋯⟩ + MSSMCharges.L T ⟨0, ⋯⟩) * MSSMCharges.L R ⟨0, ⋯⟩ * MSSMCharges.L L ⟨0, ⋯⟩) +
            (E S ⟨0, ⋯⟩ + E T ⟨0, ⋯⟩) * E R ⟨0, ⋯⟩ * E L ⟨0, ⋯⟩ +
          (N S ⟨0, ⋯⟩ + N T ⟨0, ⋯⟩) * N R ⟨0, ⋯⟩ * N L ⟨0, ⋯⟩ +
        (6 * ((Q S ⟨1, ⋯⟩ + Q T ⟨1, ⋯⟩) * Q R ⟨1, ⋯⟩ * Q L ⟨1, ⋯⟩) +
                  3 * ((U S ⟨1, ⋯⟩ + U T ⟨1, ⋯⟩) * U R ⟨1, ⋯⟩ * U L ⟨1, ⋯⟩) +
                3 * ((D S ⟨1, ⋯⟩ + D T ⟨1, ⋯⟩) * D R ⟨1, ⋯⟩ * D L ⟨1, ⋯⟩) +
              2 *
                ((MSSMCharges.L S ⟨1, ⋯⟩ + MSSMCharges.L T ⟨1, ⋯⟩) * MSSMCharges.L R ⟨1, ⋯⟩ * MSSMCharges.L L ⟨1, ⋯⟩) +
            (E S ⟨1, ⋯⟩ + E T ⟨1, ⋯⟩) * E R ⟨1, ⋯⟩ * E L ⟨1, ⋯⟩ +
          (N S ⟨1, ⋯⟩ + N T ⟨1, ⋯⟩) * N R ⟨1, ⋯⟩ * N L ⟨1, ⋯⟩) +
      (6 * ((Q S ⟨2, ⋯⟩ + Q T ⟨2, ⋯⟩) * Q R ⟨2, ⋯⟩ * Q L ⟨2, ⋯⟩) +
                3 * ((U S ⟨2, ⋯⟩ + U T ⟨2, ⋯⟩) * U R ⟨2, ⋯⟩ * U L ⟨2, ⋯⟩) +
              3 * ((D S ⟨2, ⋯⟩ + D T ⟨2, ⋯⟩) * D R ⟨2, ⋯⟩ * D L ⟨2, ⋯⟩) +
            2 * ((MSSMCharges.L S ⟨2, ⋯⟩ + MSSMCharges.L T ⟨2, ⋯⟩) * MSSMCharges.L R ⟨2, ⋯⟩ * MSSMCharges.L L ⟨2, ⋯⟩) +
          (E S ⟨2, ⋯⟩ + E T ⟨2, ⋯⟩) * E R ⟨2, ⋯⟩ * E L ⟨2, ⋯⟩ +
        (N S ⟨2, ⋯⟩ + N T ⟨2, ⋯⟩) * N R ⟨2, ⋯⟩ * N L ⟨2, ⋯⟩) +
    (2 * (Hd S + Hd T) * Hd R * Hd L + 2 * (Hu S + Hu T) * Hu R * Hu L) =
  6 * (Q S ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩ * Q L ⟨0, ⋯⟩) + 3 * (U S ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩ * U L ⟨0, ⋯⟩) +
                  3 * (D S ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩ * D L ⟨0, ⋯⟩) +
                2 * (MSSMCharges.L S ⟨0, ⋯⟩ * MSSMCharges.L R ⟨0, ⋯⟩ * MSSMCharges.L L ⟨0, ⋯⟩) +
              E S ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ * E L ⟨0, ⋯⟩ +
            N S ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ * N L ⟨0, ⋯⟩ +
          (6 * (Q S ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩ * Q L ⟨1, ⋯⟩) + 3 * (U S ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩ * U L ⟨1, ⋯⟩) +
                  3 * (D S ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩ * D L ⟨1, ⋯⟩) +
                2 * (MSSMCharges.L S ⟨1, ⋯⟩ * MSSMCharges.L R ⟨1, ⋯⟩ * MSSMCharges.L L ⟨1, ⋯⟩) +
              E S ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ * E L ⟨1, ⋯⟩ +
            N S ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩ * N L ⟨1, ⋯⟩) +
        (6 * (Q S ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩ * Q L ⟨2, ⋯⟩) + 3 * (U S ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩ * U L ⟨2, ⋯⟩) +
                3 * (D S ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩ * D L ⟨2, ⋯⟩) +
              2 * (MSSMCharges.L S ⟨2, ⋯⟩ * MSSMCharges.L R ⟨2, ⋯⟩ * MSSMCharges.L L ⟨2, ⋯⟩) +
            E S ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ * E L ⟨2, ⋯⟩ +
          N S ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩ * N L ⟨2, ⋯⟩) +
      (2 * Hd S * Hd R * Hd L + 2 * Hu S * Hu R * Hu L) +
    (6 * (Q T ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩ * Q L ⟨0, ⋯⟩) + 3 * (U T ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩ * U L ⟨0, ⋯⟩) +
                  3 * (D T ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩ * D L ⟨0, ⋯⟩) +
                2 * (MSSMCharges.L T ⟨0, ⋯⟩ * MSSMCharges.L R ⟨0, ⋯⟩ * MSSMCharges.L L ⟨0, ⋯⟩) +
              E T ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ * E L ⟨0, ⋯⟩ +
            N T ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ * N L ⟨0, ⋯⟩ +
          (6 * (Q T ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩ * Q L ⟨1, ⋯⟩) + 3 * (U T ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩ * U L ⟨1, ⋯⟩) +
                  3 * (D T ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩ * D L ⟨1, ⋯⟩) +
                2 * (MSSMCharges.L T ⟨1, ⋯⟩ * MSSMCharges.L R ⟨1, ⋯⟩ * MSSMCharges.L L ⟨1, ⋯⟩) +
              E T ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ * E L ⟨1, ⋯⟩ +
            N T ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩ * N L ⟨1, ⋯⟩) +
        (6 * (Q T ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩ * Q L ⟨2, ⋯⟩) + 3 * (U T ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩ * U L ⟨2, ⋯⟩) +
                3 * (D T ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩ * D L ⟨2, ⋯⟩) +
              2 * (MSSMCharges.L T ⟨2, ⋯⟩ * MSSMCharges.L R ⟨2, ⋯⟩ * MSSMCharges.L L ⟨2, ⋯⟩) +
            E T ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ * E L ⟨2, ⋯⟩ +
          N T ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩ * N L ⟨2, ⋯⟩) +
      (2 * Hd T * Hd R * Hd L + 2 * Hu T * Hu R * Hu L))
  ringAll goals completed! 🐙lemma cubeTriLinToFun_swap1 (S T R : MSSMCharges.Charges) :
    cubeTriLinToFun (S, T, R) = cubeTriLinToFun (T, S, R) := byS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ cubeTriLinToFun (S, T, R) = cubeTriLinToFun (T, S, R)
  simp only [cubeTriLinToFun, sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ 6 * (Q S ⟨0, ⋯⟩ * Q T ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩) + 3 * (U S ⟨0, ⋯⟩ * U T ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩) +
                3 * (D S ⟨0, ⋯⟩ * D T ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩) +
              2 * (L S ⟨0, ⋯⟩ * L T ⟨0, ⋯⟩ * L R ⟨0, ⋯⟩) +
            E S ⟨0, ⋯⟩ * E T ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ +
          N S ⟨0, ⋯⟩ * N T ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ +
        (6 * (Q S ⟨1, ⋯⟩ * Q T ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩) + 3 * (U S ⟨1, ⋯⟩ * U T ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩) +
                3 * (D S ⟨1, ⋯⟩ * D T ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩) +
              2 * (L S ⟨1, ⋯⟩ * L T ⟨1, ⋯⟩ * L R ⟨1, ⋯⟩) +
            E S ⟨1, ⋯⟩ * E T ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ +
          N S ⟨1, ⋯⟩ * N T ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩) +
      (6 * (Q S ⟨2, ⋯⟩ * Q T ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩) + 3 * (U S ⟨2, ⋯⟩ * U T ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩) +
              3 * (D S ⟨2, ⋯⟩ * D T ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩) +
            2 * (L S ⟨2, ⋯⟩ * L T ⟨2, ⋯⟩ * L R ⟨2, ⋯⟩) +
          E S ⟨2, ⋯⟩ * E T ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ +
        N S ⟨2, ⋯⟩ * N T ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩) +
    (2 * Hd S * Hd T * Hd R + 2 * Hu S * Hu T * Hu R) =
  6 * (Q T ⟨0, ⋯⟩ * Q S ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩) + 3 * (U T ⟨0, ⋯⟩ * U S ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩) +
                3 * (D T ⟨0, ⋯⟩ * D S ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩) +
              2 * (L T ⟨0, ⋯⟩ * L S ⟨0, ⋯⟩ * L R ⟨0, ⋯⟩) +
            E T ⟨0, ⋯⟩ * E S ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ +
          N T ⟨0, ⋯⟩ * N S ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ +
        (6 * (Q T ⟨1, ⋯⟩ * Q S ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩) + 3 * (U T ⟨1, ⋯⟩ * U S ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩) +
                3 * (D T ⟨1, ⋯⟩ * D S ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩) +
              2 * (L T ⟨1, ⋯⟩ * L S ⟨1, ⋯⟩ * L R ⟨1, ⋯⟩) +
            E T ⟨1, ⋯⟩ * E S ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ +
          N T ⟨1, ⋯⟩ * N S ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩) +
      (6 * (Q T ⟨2, ⋯⟩ * Q S ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩) + 3 * (U T ⟨2, ⋯⟩ * U S ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩) +
              3 * (D T ⟨2, ⋯⟩ * D S ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩) +
            2 * (L T ⟨2, ⋯⟩ * L S ⟨2, ⋯⟩ * L R ⟨2, ⋯⟩) +
          E T ⟨2, ⋯⟩ * E S ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ +
        N T ⟨2, ⋯⟩ * N S ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩) +
    (2 * Hd T * Hd S * Hd R + 2 * Hu T * Hu S * Hu R)
  ringAll goals completed! 🐙lemma cubeTriLinToFun_swap2 (S T R : MSSMCharges.Charges) :
    cubeTriLinToFun (S, T, R) = cubeTriLinToFun (S, R, T) := byS:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ cubeTriLinToFun (S, T, R) = cubeTriLinToFun (S, R, T)
  simp only [cubeTriLinToFun, sum_MSSMSpecies_numberCharges_eq_expand]S:MSSMCharges.ChargesT:MSSMCharges.ChargesR:MSSMCharges.Charges⊢ 6 * (Q S ⟨0, ⋯⟩ * Q T ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩) + 3 * (U S ⟨0, ⋯⟩ * U T ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩) +
                3 * (D S ⟨0, ⋯⟩ * D T ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩) +
              2 * (L S ⟨0, ⋯⟩ * L T ⟨0, ⋯⟩ * L R ⟨0, ⋯⟩) +
            E S ⟨0, ⋯⟩ * E T ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ +
          N S ⟨0, ⋯⟩ * N T ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ +
        (6 * (Q S ⟨1, ⋯⟩ * Q T ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩) + 3 * (U S ⟨1, ⋯⟩ * U T ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩) +
                3 * (D S ⟨1, ⋯⟩ * D T ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩) +
              2 * (L S ⟨1, ⋯⟩ * L T ⟨1, ⋯⟩ * L R ⟨1, ⋯⟩) +
            E S ⟨1, ⋯⟩ * E T ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ +
          N S ⟨1, ⋯⟩ * N T ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩) +
      (6 * (Q S ⟨2, ⋯⟩ * Q T ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩) + 3 * (U S ⟨2, ⋯⟩ * U T ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩) +
              3 * (D S ⟨2, ⋯⟩ * D T ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩) +
            2 * (L S ⟨2, ⋯⟩ * L T ⟨2, ⋯⟩ * L R ⟨2, ⋯⟩) +
          E S ⟨2, ⋯⟩ * E T ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ +
        N S ⟨2, ⋯⟩ * N T ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩) +
    (2 * Hd S * Hd T * Hd R + 2 * Hu S * Hu T * Hu R) =
  6 * (Q S ⟨0, ⋯⟩ * Q R ⟨0, ⋯⟩ * Q T ⟨0, ⋯⟩) + 3 * (U S ⟨0, ⋯⟩ * U R ⟨0, ⋯⟩ * U T ⟨0, ⋯⟩) +
                3 * (D S ⟨0, ⋯⟩ * D R ⟨0, ⋯⟩ * D T ⟨0, ⋯⟩) +
              2 * (L S ⟨0, ⋯⟩ * L R ⟨0, ⋯⟩ * L T ⟨0, ⋯⟩) +
            E S ⟨0, ⋯⟩ * E R ⟨0, ⋯⟩ * E T ⟨0, ⋯⟩ +
          N S ⟨0, ⋯⟩ * N R ⟨0, ⋯⟩ * N T ⟨0, ⋯⟩ +
        (6 * (Q S ⟨1, ⋯⟩ * Q R ⟨1, ⋯⟩ * Q T ⟨1, ⋯⟩) + 3 * (U S ⟨1, ⋯⟩ * U R ⟨1, ⋯⟩ * U T ⟨1, ⋯⟩) +
                3 * (D S ⟨1, ⋯⟩ * D R ⟨1, ⋯⟩ * D T ⟨1, ⋯⟩) +
              2 * (L S ⟨1, ⋯⟩ * L R ⟨1, ⋯⟩ * L T ⟨1, ⋯⟩) +
            E S ⟨1, ⋯⟩ * E R ⟨1, ⋯⟩ * E T ⟨1, ⋯⟩ +
          N S ⟨1, ⋯⟩ * N R ⟨1, ⋯⟩ * N T ⟨1, ⋯⟩) +
      (6 * (Q S ⟨2, ⋯⟩ * Q R ⟨2, ⋯⟩ * Q T ⟨2, ⋯⟩) + 3 * (U S ⟨2, ⋯⟩ * U R ⟨2, ⋯⟩ * U T ⟨2, ⋯⟩) +
              3 * (D S ⟨2, ⋯⟩ * D R ⟨2, ⋯⟩ * D T ⟨2, ⋯⟩) +
            2 * (L S ⟨2, ⋯⟩ * L R ⟨2, ⋯⟩ * L T ⟨2, ⋯⟩) +
          E S ⟨2, ⋯⟩ * E R ⟨2, ⋯⟩ * E T ⟨2, ⋯⟩ +
        N S ⟨2, ⋯⟩ * N R ⟨2, ⋯⟩ * N T ⟨2, ⋯⟩) +
    (2 * Hd S * Hd R * Hd T + 2 * Hu S * Hu R * Hu T)
  ringAll goals completed! 🐙

The symmetric trilinear form used to define the cubic ACC.

@[simps!]
def cubeTriLin : TriLinearSymm MSSMCharges.Charges := TriLinearSymm.mk₃
  cubeTriLinToFun
  cubeTriLinToFun_map_smul₁
  cubeTriLinToFun_map_add₁
  cubeTriLinToFun_swap1
  cubeTriLinToFun_swap2

The cubic ACC.

@[simp]
def accCube : HomogeneousCubic MSSMCharges.Charges := cubeTriLin.toCubic

Extensionality lemma for accCube.

set_option backward.isDefEq.respectTransparency false in

lemma accCube_ext {S T : MSSMCharges.Charges}
    (h : ∀ j, ∑ i, ((fun a => a^3) ∘ toSMSpecies j S) i =
    ∑ i, ((fun a => a^3) ∘ toSMSpecies j T) i)
    (hd : Hd S = Hd T) (hu : Hu S = Hu T) :
    accCube S = accCube T := byS:MSSMCharges.ChargesT:MSSMCharges.Chargesh:∀ (j : Fin 6), ∑ i, ((fun a => a ^ 3) ∘ (toSMSpecies j) S) i = ∑ i, ((fun a => a ^ 3) ∘ (toSMSpecies j) T) ihd:Hd S = Hd Thu:Hu S = Hu T⊢ accCube S = accCube T
  have h1 : ∀ j, ∑ i, (toSMSpecies j S i)^3 = ∑ i, (toSMSpecies j T i)^3 := hS:MSSMCharges.ChargesT:MSSMCharges.Chargesh:∀ (j : Fin 6), ∑ i, ((fun a => a ^ 3) ∘ (toSMSpecies j) S) i = ∑ i, ((fun a => a ^ 3) ∘ (toSMSpecies j) T) ihd:Hd S = Hd Thu:Hu S = Hu Th1:∀ (j : Fin 6), ∑ i, (toSMSpecies j) S i ^ 3 = ∑ i, (toSMSpecies j) T i ^ 3⊢ accCube S = accCube T
  simp only [HomogeneousCubic, accCube, cubeTriLin, TriLinearSymm.toCubic_apply,
    TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun, ← pow_three', Finset.sum_add_distrib,
    ← Finset.mul_sum, h1, hd, hu]All goals completed! 🐙

The ACCSystem for the MSSM without RHN.

@[simps!]
def MSSMACC : ACCSystem where
  toACCSystemCharges := MSSMCharges
  numberLinear := 4
  linearACCs := fun i =>
    match i with
    | 0 => accGrav
    | 1 => accSU2
    | 2 => accSU3
    | 3 => accYY
  numberQuadratic := 1
  quadraticACCs := fun i =>
    match i with
    | 0 => accQuad
  cubicACC := accCube

lemma cubicACC_apply (S : MSSMACC.Charges) : MSSMACC.cubicACC S = cubeTriLin.toCubic S := rfl

lemma quadSol (S : MSSMACC.QuadSols) : accQuad S.val = 0 := S.quadSol ⟨0, byS:MSSMACC.QuadSols⊢ 0 < MSSMACC.numberQuadratic simpAll goals completed! 🐙⟩

A solution from a charge satisfying the ACCs.

@[simp]
def AnomalyFreeMk (S : MSSMACC.Charges) (hg : accGrav S = 0)
    (hsu2 : accSU2 S = 0) (hsu3 : accSU3 S = 0) (hyy : accYY S = 0)
    (hquad : accQuad S = 0) (hcube : accCube S = 0) : MSSMACC.Sols :=
  ⟨⟨⟨S, byS:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0⊢ ∀ (i : Fin MSSMACC.numberLinear), (MSSMACC.linearACCs i) S = 0
    intro iS:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberLinear⊢ (MSSMACC.linearACCs i) S = 0
    match i with
    | ⟨0, _⟩ =>S:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberLinearisLt✝:0 < MSSMACC.numberLinear⊢ (MSSMACC.linearACCs ⟨0, isLt✝⟩) S = 0 exact hgAll goals completed! 🐙
    | ⟨1, _⟩ =>S:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberLinearisLt✝:1 < MSSMACC.numberLinear⊢ (MSSMACC.linearACCs ⟨1, isLt✝⟩) S = 0 exact hsu2All goals completed! 🐙
    | ⟨2, _⟩ =>S:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberLinearisLt✝:2 < MSSMACC.numberLinear⊢ (MSSMACC.linearACCs ⟨2, isLt✝⟩) S = 0 exact hsu3All goals completed! 🐙
    | ⟨3, _⟩ =>S:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberLinearisLt✝:3 < MSSMACC.numberLinear⊢ (MSSMACC.linearACCs ⟨3, isLt✝⟩) S = 0 exact hyyAll goals completed! 🐙⟩, byS:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0⊢ ∀ (i : Fin MSSMACC.numberQuadratic), (MSSMACC.quadraticACCs i) { val := S, linearSol := ⋯ }.val = 0
    intro iS:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberQuadratic⊢ (MSSMACC.quadraticACCs i) { val := S, linearSol := ⋯ }.val = 0
    match i with
    | ⟨0, _⟩ =>S:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0i:Fin MSSMACC.numberQuadraticisLt✝:0 < MSSMACC.numberQuadratic⊢ (MSSMACC.quadraticACCs ⟨0, isLt✝⟩) { val := S, linearSol := ⋯ }.val = 0 exact hquadAll goals completed! 🐙⟩, hcube⟩

lemma AnomalyFreeMk_val (S : MSSMACC.Charges) (hg : accGrav S = 0)
    (hsu2 : accSU2 S = 0) (hsu3 : accSU3 S = 0) (hyy : accYY S = 0)
    (hquad : accQuad S = 0) (hcube : accCube S = 0) :
    (AnomalyFreeMk S hg hsu2 hsu3 hyy hquad hcube).val = S := byS:MSSMACC.Chargeshg:accGrav S = 0hsu2:accSU2 S = 0hsu3:accSU3 S = 0hyy:accYY S = 0hquad:accQuad S = 0hcube:accCube S = 0⊢ (AnomalyFreeMk S hg hsu2 hsu3 hyy hquad hcube).val = S
  rflAll goals completed! 🐙

A QuadSol from a LinSol satisfying the quadratic ACC.

@[simp]
def AnomalyFreeQuadMk' (S : MSSMACC.LinSols) (hquad : accQuad S.val = 0) :
    MSSMACC.QuadSols :=
  ⟨S, byS:MSSMACC.LinSolshquad:accQuad S.val = 0⊢ ∀ (i : Fin MSSMACC.numberQuadratic), (MSSMACC.quadraticACCs i) S.val = 0
    intro iS:MSSMACC.LinSolshquad:accQuad S.val = 0i:Fin MSSMACC.numberQuadratic⊢ (MSSMACC.quadraticACCs i) S.val = 0
    match i with
    | ⟨0, _⟩ =>S:MSSMACC.LinSolshquad:accQuad S.val = 0i:Fin MSSMACC.numberQuadraticisLt✝:0 < MSSMACC.numberQuadratic⊢ (MSSMACC.quadraticACCs ⟨0, isLt✝⟩) S.val = 0 exact hquadAll goals completed! 🐙⟩

A Sol from a LinSol satisfying the quadratic and cubic ACCs.

@[simp]
def AnomalyFreeMk' (S : MSSMACC.LinSols) (hquad : accQuad S.val = 0)
    (hcube : accCube S.val = 0) : MSSMACC.Sols :=
  ⟨⟨S, byS:MSSMACC.LinSolshquad:accQuad S.val = 0hcube:accCube S.val = 0⊢ ∀ (i : Fin MSSMACC.numberQuadratic), (MSSMACC.quadraticACCs i) S.val = 0
    intro iS:MSSMACC.LinSolshquad:accQuad S.val = 0hcube:accCube S.val = 0i:Fin MSSMACC.numberQuadratic⊢ (MSSMACC.quadraticACCs i) S.val = 0
    match i with
    | ⟨0, _⟩ =>S:MSSMACC.LinSolshquad:accQuad S.val = 0hcube:accCube S.val = 0i:Fin MSSMACC.numberQuadraticisLt✝:0 < MSSMACC.numberQuadratic⊢ (MSSMACC.quadraticACCs ⟨0, isLt✝⟩) S.val = 0 exact hquadAll goals completed! 🐙⟩, hcube⟩

A Sol from a QuadSol satisfying the cubic ACCs.

@[simp]
def AnomalyFreeMk'' (S : MSSMACC.QuadSols) (hcube : accCube S.val = 0) : MSSMACC.Sols :=
  ⟨S, hcube⟩

lemma AnomalyFreeMk''_val (S : MSSMACC.QuadSols)
    (hcube : accCube S.val = 0) :
    (AnomalyFreeMk'' S hcube).val = S.val := byS:MSSMACC.QuadSolshcube:accCube S.val = 0⊢ (AnomalyFreeMk'' S hcube).val = S.val
  rflAll goals completed! 🐙

The dot product on the vector space of charges.

set_option backward.isDefEq.respectTransparency false in


@[simps!]
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)
  (by⊢ ∀ (a : ℚ) (S T : MSSMCharges.Charges),
  ∑ i,
          (Q (a • S, T).1 i * Q (a • S, T).2 i + U (a • S, T).1 i * U (a • S, T).2 i +
                  D (a • S, T).1 i * D (a • S, T).2 i +
                L (a • S, T).1 i * L (a • S, T).2 i +
              E (a • S, T).1 i * E (a • S, T).2 i +
            N (a • S, T).1 i * N (a • S, T).2 i) +
        Hd (a • S, T).1 * Hd (a • S, T).2 +
      Hu (a • S, T).1 * Hu (a • S, T).2 =
    a *
      (∑ i,
            (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                  L (S, T).1 i * L (S, T).2 i +
                E (S, T).1 i * E (S, T).2 i +
              N (S, T).1 i * N (S, T).2 i) +
          Hd (S, T).1 * Hd (S, T).2 +
        Hu (S, T).1 * Hu (S, T).2)
    intro a S Ta:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        (Q (a • S, T).1 i * Q (a • S, T).2 i + U (a • S, T).1 i * U (a • S, T).2 i +
                D (a • S, T).1 i * D (a • S, T).2 i +
              L (a • S, T).1 i * L (a • S, T).2 i +
            E (a • S, T).1 i * E (a • S, T).2 i +
          N (a • S, T).1 i * N (a • S, T).2 i) +
      Hd (a • S, T).1 * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)
    repeat rw [(toSMSpecies _).map_smula:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + U (a • S, T).1 i * U (a • S, T).2 i +
                D (a • S, T).1 i * D (a • S, T).2 i +
              L (a • S, T).1 i * L (a • S, T).2 i +
            E (a • S, T).1 i * E (a • S, T).2 i +
          N (a • S, T).1 i * N (a • S, T).2 i) +
      Hd (a • S, T).1 * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      Hd (a • S, T).1 * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          N (a • S, T).1 i * N (a • S, T).2 i) +
      Hd (a • S, T).1 * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      Hd (a • S, T).1 * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      Hd (a • S, T).1 * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)
    rw [Hd.map_smul,a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      a • Hd S * Hd (a • S, T).2 +
    Hu (a • S, T).1 * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      a • Hd S * Hd (a • S, T).2 +
    a • Hu S * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2) Hu.map_smula:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      a • Hd S * Hd (a • S, T).2 +
    a • Hu S * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      a • Hd S * Hd (a • S, T).2 +
    a • Hu S * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        ((a • (toSMSpecies 0) S) i * Q (a • S, T).2 i + (a • (toSMSpecies 1) S) i * U (a • S, T).2 i +
                (a • (toSMSpecies 2) S) i * D (a • S, T).2 i +
              (a • (toSMSpecies 3) S) i * L (a • S, T).2 i +
            (a • (toSMSpecies 4) S) i * E (a • S, T).2 i +
          (a • (toSMSpecies 5) S) i * N (a • S, T).2 i) +
      a • Hd S * Hd (a • S, T).2 +
    a • Hu S * Hu (a • S, T).2 =
  a *
    (∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2)
    simp only [Fin.isValue, toSMSpecies_apply, reduceMul, sum_MSSMSpecies_numberCharges_eq_expand,
      Fin.zero_eta, Fin.mk_one, Hd_apply, Fin.reduceFinMk, smul_eq_mul, Hu_apply]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (a • (toSMSpecies 0) S) 0 * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                    (a • (toSMSpecies 1) S) 0 * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  (a • (toSMSpecies 2) S) 0 * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                (a • (toSMSpecies 3) S) 0 * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              (a • (toSMSpecies 4) S) 0 * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            (a • (toSMSpecies 5) S) 0 * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          ((a • (toSMSpecies 0) S) 1 * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    (a • (toSMSpecies 1) S) 1 * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                  (a • (toSMSpecies 2) S) 1 * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                (a • (toSMSpecies 3) S) 1 * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              (a • (toSMSpecies 4) S) 1 * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            (a • (toSMSpecies 5) S) 1 * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        ((a • (toSMSpecies 0) S) ⟨2, ⋯⟩ * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  (a • (toSMSpecies 1) S) ⟨2, ⋯⟩ * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                (a • (toSMSpecies 2) S) ⟨2, ⋯⟩ * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              (a • (toSMSpecies 3) S) ⟨2, ⋯⟩ * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            (a • (toSMSpecies 4) S) ⟨2, ⋯⟩ * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          (a • (toSMSpecies 5) S) ⟨2, ⋯⟩ * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      a * S 18 * T 18 +
    a * S 19 * T 19 =
  a *
    (S (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                      S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
                S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
              S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
            (S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                      S (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
                S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
              S (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
          (S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
                S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
              S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
            S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
        S 18 * T 18 +
      S 19 * T 19)
    simp only [HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply]a:ℚS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ a * S (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                    a * S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  a * S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                a * S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              a * S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            a * S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          (a * S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    a * S (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                  a * S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                a * S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              a * S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            a * S (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        (a * S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  a * S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                a * S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              a * S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            a * S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          a * S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      a * S 18 * T 18 +
    a * S 19 * T 19 =
  a *
    (S (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                      S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
                S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
              S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
            (S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                      S (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
                S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
              S (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
          (S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
                S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
              S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
            S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
        S 18 * T 18 +
      S 19 * T 19)
    ringAll goals completed! 🐙)
  (by⊢ ∀ (S1 S2 T : MSSMCharges.Charges),
  ∑ i,
          (Q (S1 + S2, T).1 i * Q (S1 + S2, T).2 i + U (S1 + S2, T).1 i * U (S1 + S2, T).2 i +
                  D (S1 + S2, T).1 i * D (S1 + S2, T).2 i +
                L (S1 + S2, T).1 i * L (S1 + S2, T).2 i +
              E (S1 + S2, T).1 i * E (S1 + S2, T).2 i +
            N (S1 + S2, T).1 i * N (S1 + S2, T).2 i) +
        Hd (S1 + S2, T).1 * Hd (S1 + S2, T).2 +
      Hu (S1 + S2, T).1 * Hu (S1 + S2, T).2 =
    ∑ i,
            (Q (S1, T).1 i * Q (S1, T).2 i + U (S1, T).1 i * U (S1, T).2 i + D (S1, T).1 i * D (S1, T).2 i +
                  L (S1, T).1 i * L (S1, T).2 i +
                E (S1, T).1 i * E (S1, T).2 i +
              N (S1, T).1 i * N (S1, T).2 i) +
          Hd (S1, T).1 * Hd (S1, T).2 +
        Hu (S1, T).1 * Hu (S1, T).2 +
      (∑ i,
            (Q (S2, T).1 i * Q (S2, T).2 i + U (S2, T).1 i * U (S2, T).2 i + D (S2, T).1 i * D (S2, T).2 i +
                  L (S2, T).1 i * L (S2, T).2 i +
                E (S2, T).1 i * E (S2, T).2 i +
              N (S2, T).1 i * N (S2, T).2 i) +
          Hd (S2, T).1 * Hd (S2, T).2 +
        Hu (S2, T).1 * Hu (S2, T).2)
    intro S1 S2 TS1:MSSMCharges.ChargesS2:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        (Q (S1 + S2, T).1 i * Q (S1 + S2, T).2 i + U (S1 + S2, T).1 i * U (S1 + S2, T).2 i +
                D (S1 + S2, T).1 i * D (S1 + S2, T).2 i +
              L (S1 + S2, T).1 i * L (S1 + S2, T).2 i +
            E (S1 + S2, T).1 i * E (S1 + S2, T).2 i +
          N (S1 + S2, T).1 i * N (S1 + S2, T).2 i) +
      Hd (S1 + S2, T).1 * Hd (S1 + S2, T).2 +
    Hu (S1 + S2, T).1 * Hu (S1 + S2, T).2 =
  ∑ i,
          (Q (S1, T).1 i * Q (S1, T).2 i + U (S1, T).1 i * U (S1, T).2 i + D (S1, T).1 i * D (S1, T).2 i +
                L (S1, T).1 i * L (S1, T).2 i +
              E (S1, T).1 i * E (S1, T).2 i +
            N (S1, T).1 i * N (S1, T).2 i) +
        Hd (S1, T).1 * Hd (S1, T).2 +
      Hu (S1, T).1 * Hu (S1, T).2 +
    (∑ i,
          (Q (S2, T).1 i * Q (S2, T).2 i + U (S2, T).1 i * U (S2, T).2 i + D (S2, T).1 i * D (S2, T).2 i +
                L (S2, T).1 i * L (S2, T).2 i +
              E (S2, T).1 i * E (S2, T).2 i +
            N (S2, T).1 i * N (S2, T).2 i) +
        Hd (S2, T).1 * Hd (S2, T).2 +
      Hu (S2, T).1 * Hu (S2, T).2)
    simp only [toSMSpecies_apply, Fin.isValue,
      ACCSystemCharges.chargesAddCommMonoid_add, map_add, Hd_apply, Fin.reduceFinMk, Hu_apply]S1:MSSMCharges.ChargesS2:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ x,
        ((S1 (Fin.castAdd 2 (finProdFinEquiv (0, x))) + S2 (Fin.castAdd 2 (finProdFinEquiv (0, x)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (1, x))) + S2 (Fin.castAdd 2 (finProdFinEquiv (1, x)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (1, x))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (2, x))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, x)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (3, x))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, x)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (3, x))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (4, x))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, x)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (4, x))) +
          (S1 (Fin.castAdd 2 (finProdFinEquiv (5, x))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, x)))) *
            T (Fin.castAdd 2 (finProdFinEquiv (5, x)))) +
      (S1 18 + S2 18) * T 18 +
    (S1 19 + S2 19) * T 19 =
  ∑ x,
          (S1 (Fin.castAdd 2 (finProdFinEquiv (0, x))) * T (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (1, x))) * T (Fin.castAdd 2 (finProdFinEquiv (1, x))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (2, x))) * T (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (3, x))) * T (Fin.castAdd 2 (finProdFinEquiv (3, x))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (4, x))) * T (Fin.castAdd 2 (finProdFinEquiv (4, x))) +
            S1 (Fin.castAdd 2 (finProdFinEquiv (5, x))) * T (Fin.castAdd 2 (finProdFinEquiv (5, x)))) +
        S1 18 * T 18 +
      S1 19 * T 19 +
    (∑ x,
          (S2 (Fin.castAdd 2 (finProdFinEquiv (0, x))) * T (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (1, x))) * T (Fin.castAdd 2 (finProdFinEquiv (1, x))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (2, x))) * T (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (3, x))) * T (Fin.castAdd 2 (finProdFinEquiv (3, x))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (4, x))) * T (Fin.castAdd 2 (finProdFinEquiv (4, x))) +
            S2 (Fin.castAdd 2 (finProdFinEquiv (5, x))) * T (Fin.castAdd 2 (finProdFinEquiv (5, x)))) +
        S2 18 * T 18 +
      S2 19 * T 19)
    simp only [reduceMul, Fin.isValue, sum_MSSMSpecies_numberCharges_eq_expand, Fin.zero_eta,
      Fin.mk_one]S1:MSSMCharges.ChargesS2:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (S1 (Fin.castAdd 2 (finProdFinEquiv (0, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (0, 0)))) *
                      T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                    (S1 (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) *
                      T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (3, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, 0)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, 0)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          ((S1 (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (0, 1)))) *
                      T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    (S1 (Fin.castAdd 2 (finProdFinEquiv (1, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (1, 1)))) *
                      T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (3, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (5, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        ((S1 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                      S2 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          (S1 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) *
            T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      (S1 18 + S2 18) * T 18 +
    (S1 19 + S2 19) * T 19 =
  S1 (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                      S1 (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                      S1 (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
          (S1 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
            S1 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
        S1 18 * T 18 +
      S1 19 * T 19 +
    (S2 (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                      S2 (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
            (S2 (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                      S2 (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
          (S2 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
            S2 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
        S2 18 * T 18 +
      S2 19 * T 19)
    simp only [Fin.isValue, Prod.mk_zero_zero, Prod.mk_one_one]S1:MSSMCharges.ChargesS2:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (S1 (Fin.castAdd 2 (finProdFinEquiv 0)) + S2 (Fin.castAdd 2 (finProdFinEquiv 0))) *
                      T (Fin.castAdd 2 (finProdFinEquiv 0)) +
                    (S1 (Fin.castAdd 2 (finProdFinEquiv (1, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (1, 0)))) *
                      T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (2, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, 0)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (3, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, 0)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (4, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, 0)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (5, 0))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, 0)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          ((S1 (Fin.castAdd 2 (finProdFinEquiv (0, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (0, 1)))) *
                      T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    (S1 (Fin.castAdd 2 (finProdFinEquiv 1)) + S2 (Fin.castAdd 2 (finProdFinEquiv 1))) *
                      T (Fin.castAdd 2 (finProdFinEquiv 1)) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (2, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, 1)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (3, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, 1)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (4, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, 1)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (5, 1))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        ((S1 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  (S1 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                      S2 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩)))) *
                    T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                (S1 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩)))) *
                  T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              (S1 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩)))) *
                T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩)))) *
              T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          (S1 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) + S2 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) *
            T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      (S1 18 + S2 18) * T 18 +
    (S1 19 + S2 19) * T 19 =
  S1 (Fin.castAdd 2 (finProdFinEquiv 0)) * T (Fin.castAdd 2 (finProdFinEquiv 0)) +
                      S1 (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
            (S1 (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                      S1 (Fin.castAdd 2 (finProdFinEquiv 1)) * T (Fin.castAdd 2 (finProdFinEquiv 1)) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
          (S1 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                    S1 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                  S1 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
                S1 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
              S1 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
            S1 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
        S1 18 * T 18 +
      S1 19 * T 19 +
    (S2 (Fin.castAdd 2 (finProdFinEquiv 0)) * T (Fin.castAdd 2 (finProdFinEquiv 0)) +
                      S2 (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
            (S2 (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                      S2 (Fin.castAdd 2 (finProdFinEquiv 1)) * T (Fin.castAdd 2 (finProdFinEquiv 1)) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
          (S2 (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                    S2 (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                  S2 (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
                S2 (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
              S2 (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
            S2 (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
        S2 18 * T 18 +
      S2 19 * T 19)
    ringAll goals completed! 🐙)
  (by⊢ ∀ (S T : MSSMCharges.Charges),
  ∑ i,
          (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
                L (S, T).1 i * L (S, T).2 i +
              E (S, T).1 i * E (S, T).2 i +
            N (S, T).1 i * N (S, T).2 i) +
        Hd (S, T).1 * Hd (S, T).2 +
      Hu (S, T).1 * Hu (S, T).2 =
    ∑ i,
          (Q (T, S).1 i * Q (T, S).2 i + U (T, S).1 i * U (T, S).2 i + D (T, S).1 i * D (T, S).2 i +
                L (T, S).1 i * L (T, S).2 i +
              E (T, S).1 i * E (T, S).2 i +
            N (T, S).1 i * N (T, S).2 i) +
        Hd (T, S).1 * Hd (T, S).2 +
      Hu (T, S).1 * Hu (T, S).2
    intro S TS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ i,
        (Q (S, T).1 i * Q (S, T).2 i + U (S, T).1 i * U (S, T).2 i + D (S, T).1 i * D (S, T).2 i +
              L (S, T).1 i * L (S, T).2 i +
            E (S, T).1 i * E (S, T).2 i +
          N (S, T).1 i * N (S, T).2 i) +
      Hd (S, T).1 * Hd (S, T).2 +
    Hu (S, T).1 * Hu (S, T).2 =
  ∑ i,
        (Q (T, S).1 i * Q (T, S).2 i + U (T, S).1 i * U (T, S).2 i + D (T, S).1 i * D (T, S).2 i +
              L (T, S).1 i * L (T, S).2 i +
            E (T, S).1 i * E (T, S).2 i +
          N (T, S).1 i * N (T, S).2 i) +
      Hd (T, S).1 * Hd (T, S).2 +
    Hu (T, S).1 * Hu (T, S).2
    simp only [toSMSpecies_apply, Fin.isValue, Hd_apply, Fin.reduceFinMk, Hu_apply]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∑ x,
        (S (Fin.castAdd 2 (finProdFinEquiv (0, x))) * T (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (1, x))) * T (Fin.castAdd 2 (finProdFinEquiv (1, x))) +
                S (Fin.castAdd 2 (finProdFinEquiv (2, x))) * T (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
              S (Fin.castAdd 2 (finProdFinEquiv (3, x))) * T (Fin.castAdd 2 (finProdFinEquiv (3, x))) +
            S (Fin.castAdd 2 (finProdFinEquiv (4, x))) * T (Fin.castAdd 2 (finProdFinEquiv (4, x))) +
          S (Fin.castAdd 2 (finProdFinEquiv (5, x))) * T (Fin.castAdd 2 (finProdFinEquiv (5, x)))) +
      S 18 * T 18 +
    S 19 * T 19 =
  ∑ x,
        (T (Fin.castAdd 2 (finProdFinEquiv (0, x))) * S (Fin.castAdd 2 (finProdFinEquiv (0, x))) +
                  T (Fin.castAdd 2 (finProdFinEquiv (1, x))) * S (Fin.castAdd 2 (finProdFinEquiv (1, x))) +
                T (Fin.castAdd 2 (finProdFinEquiv (2, x))) * S (Fin.castAdd 2 (finProdFinEquiv (2, x))) +
              T (Fin.castAdd 2 (finProdFinEquiv (3, x))) * S (Fin.castAdd 2 (finProdFinEquiv (3, x))) +
            T (Fin.castAdd 2 (finProdFinEquiv (4, x))) * S (Fin.castAdd 2 (finProdFinEquiv (4, x))) +
          T (Fin.castAdd 2 (finProdFinEquiv (5, x))) * S (Fin.castAdd 2 (finProdFinEquiv (5, x)))) +
      T 18 * S 18 +
    T 19 * S 19
    simp only [reduceMul, Fin.isValue, sum_MSSMSpecies_numberCharges_eq_expand, Fin.zero_eta,
      Fin.mk_one]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ S (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          (S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    S (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            S (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        (S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      S 18 * T 18 +
    S 19 * T 19 =
  T (Fin.castAdd 2 (finProdFinEquiv (0, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (0, 0))) +
                    T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          (T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    T (Fin.castAdd 2 (finProdFinEquiv (1, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (1, 1))) +
                  T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            T (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        (T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      T 18 * S 18 +
    T 19 * S 19
    simp only [Fin.isValue, Prod.mk_zero_zero, Prod.mk_one_one]S:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ S (Fin.castAdd 2 (finProdFinEquiv 0)) * T (Fin.castAdd 2 (finProdFinEquiv 0)) +
                    S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          (S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    S (Fin.castAdd 2 (finProdFinEquiv 1)) * T (Fin.castAdd 2 (finProdFinEquiv 1)) +
                  S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            S (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * T (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        (S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      S 18 * T 18 +
    S 19 * T 19 =
  T (Fin.castAdd 2 (finProdFinEquiv 0)) * S (Fin.castAdd 2 (finProdFinEquiv 0)) +
                    T (Fin.castAdd 2 (finProdFinEquiv (1, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (1, 0))) +
                  T (Fin.castAdd 2 (finProdFinEquiv (2, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (2, 0))) +
                T (Fin.castAdd 2 (finProdFinEquiv (3, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (3, 0))) +
              T (Fin.castAdd 2 (finProdFinEquiv (4, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (4, 0))) +
            T (Fin.castAdd 2 (finProdFinEquiv (5, 0))) * S (Fin.castAdd 2 (finProdFinEquiv (5, 0))) +
          (T (Fin.castAdd 2 (finProdFinEquiv (0, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (0, 1))) +
                    T (Fin.castAdd 2 (finProdFinEquiv 1)) * S (Fin.castAdd 2 (finProdFinEquiv 1)) +
                  T (Fin.castAdd 2 (finProdFinEquiv (2, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (2, 1))) +
                T (Fin.castAdd 2 (finProdFinEquiv (3, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (3, 1))) +
              T (Fin.castAdd 2 (finProdFinEquiv (4, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (4, 1))) +
            T (Fin.castAdd 2 (finProdFinEquiv (5, 1))) * S (Fin.castAdd 2 (finProdFinEquiv (5, 1)))) +
        (T (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (0, ⟨2, ⋯⟩))) +
                  T (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (1, ⟨2, ⋯⟩))) +
                T (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (2, ⟨2, ⋯⟩))) +
              T (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (3, ⟨2, ⋯⟩))) +
            T (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (4, ⟨2, ⋯⟩))) +
          T (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩))) * S (Fin.castAdd 2 (finProdFinEquiv (5, ⟨2, ⋯⟩)))) +
      T 18 * S 18 +
    T 19 * S 19
    ringAll goals completed! 🐙)