Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps

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.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic

Family maps for the Standard Model for RHN ACCs

We define the a series of maps between the charges for different numbers of families.

@[expose] public section

Given a map of for a generic species, the corresponding map for charges.


@[simps!]
def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Charges) :
    (SMνCharges n).Charges →ₗ[ℚ] (SMνCharges m).Charges where
  toFun S := toSpeciesEquiv.symm (fun i => (LinearMap.comp f (toSpecies i)) S)
  map_add' S T := byn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T
    rw [charges_eq_toSpecies_eqn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∀ (i : Fin 6),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
    (toSpecies i)
      ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∀ (i : Fin 6),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
    (toSpecies i)
      ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)]n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∀ (i : Fin 6),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
    (toSpecies i)
      ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)
    intro in:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpecies i)
    ((toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) + toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)
    rw [map_add,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (S + T)) =
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) +
    (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)All goals completed! 🐙 toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin 6⊢ (f ∘ₗ toSpecies i) (S + T) =
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S) +
    (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)All goals completed! 🐙 toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin 6⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) T)All goals completed! 🐙 toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin 6⊢ (f ∘ₗ toSpecies i) (S + T) = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) TAll goals completed! 🐙
      map_addn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).ChargesS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin 6⊢ (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) T = (f ∘ₗ toSpecies i) S + (f ∘ₗ toSpecies i) TAll goals completed! 🐙]All goals completed! 🐙
  map_smul' a S := byn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Charges⊢ (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S
    rw [charges_eq_toSpecies_eqn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
    (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
    (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)]n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6),
  (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
    (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)
    intro in:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (toSpecies i) ((RingHom.id ℚ) a • toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)
    rw [map_smul,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) (a • S)) =
  (RingHom.id ℚ) a • (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (toSpecies i) (toSpeciesEquiv.symm fun i => (f ∘ₗ toSpecies i) S)n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S toSMSpecies_toSpecies_inv,n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ (f ∘ₗ toSpecies i) (a • S) = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) Sn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S map_smuln:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) Sn:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S]n:ℕm:ℕf:(SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Chargesa:ℚS:(SMνCharges n).Chargesi:Fin 6⊢ a • (f ∘ₗ toSpecies i) S = (RingHom.id ℚ) a • (f ∘ₗ toSpecies i) S
    rflAll goals completed! 🐙

lemma chargesMapOfSpeciesMap_toSpecies {n m : ℕ}
    (f : (SMνSpecies n).Charges →ₗ[ℚ] (SMνSpecies m).Charges)
    (S : (SMνCharges n).Charges) (j : Fin 6) :
    toSpecies j (chargesMapOfSpeciesMap f S) = (LinearMap.comp f (toSpecies j)) S :=
  toSMSpecies_toSpecies_inv _ _

The projection of the m-family charges onto the first n-family charges for species.

@[simps!]
def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
    (SMνSpecies m).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
  toFun S := S ∘ Fin.castLE h
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

The projection of the m-family charges onto the first n-family charges.

def familyProjection {m n : ℕ} (h : n ≤ m) : (SMνCharges m).Charges →ₗ[ℚ] (SMνCharges n).Charges :=
  chargesMapOfSpeciesMap (speciesFamilyProj h)

For species, the embedding of the m-family charges onto the n-family charges, with all other charges zero.


@[simps!]
def speciesEmbed (m n : ℕ) :
    (SMνSpecies m).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
  toFun S := fun i =>
    if hi : i.val < m then
      S ⟨i, hi⟩
    else
      0
  map_add' S T := bym:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Charges⊢ (fun i => if hi : ↑i < m then (S + T) ⟨↑i, hi⟩ else 0) =
  (fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + fun i => if hi : ↑i < m then T ⟨↑i, hi⟩ else 0
    funext im:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberCharges⊢ (if hi : ↑i < m then (S + T) ⟨↑i, hi⟩ else 0) =
  ((fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + fun i => if hi : ↑i < m then T ⟨↑i, hi⟩ else 0) i
    simp only [ACCSystemCharges.chargesAddCommMonoid_add]m:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberCharges⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0
    by_cases hi : i.val < mposm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0
    ·posm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0 rw [dif_pos hi,posm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ = (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0All goals completed! 🐙 dif_pos hi,posm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ = S ⟨↑i, hi⟩ + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0All goals completed! 🐙 dif_pos hiposm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ = S ⟨↑i, hi⟩ + T ⟨↑i, hi⟩All goals completed! 🐙]All goals completed! 🐙
    ·negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then S ⟨↑i, ⋯⟩ + T ⟨↑i, ⋯⟩ else 0) =
  (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0 rw [dif_neg hi,negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = (if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0 dif_neg hi,negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + if hi : ↑i < m then T ⟨↑i, hi⟩ else 0negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0 dif_neg hinegm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0]negm:ℕn:ℕS:(SMνSpecies m).ChargesT:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = 0 + 0
      with_unfolding_all rflAll goals completed! 🐙
  map_smul' a S := bym:ℕn:ℕa:ℚS:(SMνSpecies m).Charges⊢ (fun i => if hi : ↑i < m then (a • S) ⟨↑i, hi⟩ else 0) =
  (RingHom.id ℚ) a • fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0
    funext im:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberCharges⊢ (if hi : ↑i < m then (a • S) ⟨↑i, hi⟩ else 0) = ((RingHom.id ℚ) a • fun i => if hi : ↑i < m then S ⟨↑i, hi⟩ else 0) i
    simp only [HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
      eq_ratCast, Rat.cast_eq_id, id_eq]m:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberCharges⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0
    by_cases hi : i.val < mposm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0negm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0
    ·posm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0 rw [dif_pos hi,posm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ a * S ⟨↑i, ⋯⟩ = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0All goals completed! 🐙 dif_pos hiposm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:↑i < m⊢ a * S ⟨↑i, ⋯⟩ = a * S ⟨↑i, hi⟩All goals completed! 🐙]All goals completed! 🐙
    ·negm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ (if h : ↑i < m then a * S ⟨↑i, ⋯⟩ else 0) = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0 rw [dif_neg hi,negm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * if hi : ↑i < m then S ⟨↑i, hi⟩ else 0negm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0 dif_neg hinegm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0negm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0]negm:ℕn:ℕa:ℚS:(SMνSpecies m).Chargesi:Fin (SMνSpecies n).numberChargeshi:¬↑i < m⊢ 0 = a * 0
      exact Eq.symm (Rat.mul_zero a)All goals completed! 🐙

The embedding of the m-family charges onto the n-family charges, with all other charges zero.

def familyEmbedding (m n : ℕ) : (SMνCharges m).Charges →ₗ[ℚ] (SMνCharges n).Charges :=
  chargesMapOfSpeciesMap (speciesEmbed m n)

For species, the embedding of the 1-family charges into the n-family charges in a universal manner.

@[simps!]
def speciesFamilyUniversial (n : ℕ) :
    (SMνSpecies 1).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
  toFun S _ := S ⟨0, Nat.zero_lt_succ 0⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

The embedding of the 1-family charges into the n-family charges in a universal manner.

def familyUniversal (n : ℕ) : (SMνCharges 1).Charges →ₗ[ℚ] (SMνCharges n).Charges :=
  chargesMapOfSpeciesMap (speciesFamilyUniversial n)

              

lemma toSpecies_familyUniversal {n : ℕ} (j : Fin 6) (S : (SMνCharges 1).Charges)
    (i : Fin n) : toSpecies j (familyUniversal n S) i = toSpecies j S ⟨0, byn:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ 0 < (SMνSpecies 1).numberCharges simpAll goals completed! 🐙⟩ := byn:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ (toSpecies j) ((familyUniversal n) S) i = (toSpecies j) S ⟨0, ⋯⟩
  rw [familyUniversal,n:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ (toSpecies j) ((chargesMapOfSpeciesMap (speciesFamilyUniversial n)) S) i = (toSpecies j) S ⟨0, ⋯⟩n:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ (speciesFamilyUniversial n ∘ₗ toSpecies j) S i = (toSpecies j) S ⟨0, ⋯⟩ chargesMapOfSpeciesMap_toSpeciesn:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ (speciesFamilyUniversial n ∘ₗ toSpecies j) S i = (toSpecies j) S ⟨0, ⋯⟩n:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ (speciesFamilyUniversial n ∘ₗ toSpecies j) S i = (toSpecies j) S ⟨0, ⋯⟩]n:ℕj:Fin 6S:(SMνCharges 1).Chargesi:Fin n⊢ (speciesFamilyUniversial n ∘ₗ toSpecies j) S i = (toSpecies j) S ⟨0, ⋯⟩
  rflAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma sum_familyUniversal {n : ℕ} (m : ℕ) (S : (SMνCharges 1).Charges) (j : Fin 6) :
    ∑ i, ((fun a => a ^ m) ∘ toSpecies j (familyUniversal n S)) i =
    n * (toSpecies j S ⟨0, byn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ 0 < (SMνSpecies 1).numberCharges simpAll goals completed! 🐙⟩) ^ m := byn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) ((familyUniversal n) S)) i = ↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m
  simp only [Function.comp_apply, toSpecies_apply, toSpeciesEquiv_apply,
    Fin.zero_eta, Fin.isValue, Nat.reduceMul]n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m
  have h1 : (n : ℚ) * (toSpecies j S ⟨0, byn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ 0 < (SMνSpecies 1).numberChargesn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m simpAll goals completed! 🐙n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m⟩) ^ m =
      ∑ _i : Fin n, (toSpecies j S ⟨0, byn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6_i:Fin n⊢ 0 < (SMνSpecies 1).numberChargesn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m simpAll goals completed! 🐙n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m⟩) ^ m := byn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) ((familyUniversal n) S)) i = ↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ mn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m
    rw [Fin.sum_constn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = n • (toSpecies j) S ⟨0, ⋯⟩ ^ mn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = n • (toSpecies j) S ⟨0, ⋯⟩ ^ mn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m]n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = n • (toSpecies j) S ⟨0, ⋯⟩ ^ mn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m
    simpn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ mn:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ↑n * S (finProdFinEquiv (j, 0)) ^ m
  erw [h1n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m]n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ m
  refine Finset.sum_congr rfl (fun i _ => ?_)n:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ mi:Fin (SMνSpecies n).numberChargesx✝:i ∈ Finset.univ⊢ (familyUniversal n) S (finProdFinEquiv (j, i)) ^ m = (toSpecies j) S ⟨0, ⋯⟩ ^ m
  erw [toSpecies_familyUniversaln:ℕm:ℕS:(SMνCharges 1).Chargesj:Fin 6h1:↑n * (toSpecies j) S ⟨0, ⋯⟩ ^ m = ∑ _i, (toSpecies j) S ⟨0, ⋯⟩ ^ mi:Fin (SMνSpecies n).numberChargesx✝:i ∈ Finset.univ⊢ (toSpecies j) S ⟨0, ⋯⟩ ^ m = (toSpecies j) S ⟨0, ⋯⟩ ^ m]All goals completed! 🐙lemma sum_familyUniversal_one {n : ℕ} (S : (SMνCharges 1).Charges) (j : Fin 6) :
    ∑ i, toSpecies j (familyUniversal n S) i = n * (toSpecies j S ⟨0, byn:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ 0 < (SMνSpecies 1).numberCharges simpAll goals completed! 🐙⟩) := byn:ℕS:(SMνCharges 1).Chargesj:Fin 6⊢ ∑ i, (toSpecies j) ((familyUniversal n) S) i = ↑n * (toSpecies j) S ⟨0, ⋯⟩
  simpa using @sum_familyUniversal n 1 S jAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma sum_familyUniversal_two {n : ℕ} (S : (SMνCharges 1).Charges)
    (T : (SMνCharges n).Charges) (j : Fin 6) :
    ∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i) =
    (toSpecies j S ⟨0, byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6⊢ 0 < (SMνSpecies 1).numberCharges simpAll goals completed! 🐙⟩) * ∑ i, toSpecies j T i := byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6⊢ ∑ i, (toSpecies j) ((familyUniversal n) S) i * (toSpecies j) T i = (toSpecies j) S ⟨0, ⋯⟩ * ∑ i, (toSpecies j) T i
  simp only [toSpecies_apply, toSpeciesEquiv_apply, Fin.zero_eta,
    Fin.isValue, Nat.reduceMul]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) =
  S (finProdFinEquiv (j, 0)) * ∑ x, T (finProdFinEquiv (j, x))
  rw [Finset.mul_sumn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) =
  ∑ i, S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i))n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) =
  ∑ i, S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i))]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) =
  ∑ i, S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i))
  refine Finset.sum_congr rfl (fun i _ => ?_)n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesx✝:i ∈ Finset.univ⊢ (familyUniversal n) S (finProdFinEquiv (j, i)) * T (finProdFinEquiv (j, i)) =
  S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i))
  erw [toSpecies_familyUniversaln:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesx✝:i ∈ Finset.univ⊢ (toSpecies j) S ⟨0, ⋯⟩ * T (finProdFinEquiv (j, i)) = S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i))]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesx✝:i ∈ Finset.univ⊢ (toSpecies j) S ⟨0, ⋯⟩ * T (finProdFinEquiv (j, i)) = S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i))
  rflAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).Charges)
    (T L : (SMνCharges n).Charges) (j : Fin 6) :
    ∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i * toSpecies j L i) =
    (toSpecies j S ⟨0, byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ 0 < (SMνSpecies 1).numberCharges simpAll goals completed! 🐙⟩) * ∑ i, toSpecies j T i * toSpecies j L i := byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∑ i, (toSpecies j) ((familyUniversal n) S) i * (toSpecies j) T i * (toSpecies j) L i =
  (toSpecies j) S ⟨0, ⋯⟩ * ∑ i, (toSpecies j) T i * (toSpecies j) L i
  simp only [toSpecies_apply, toSpeciesEquiv_apply, Fin.zero_eta,
    Fin.isValue, Nat.reduceMul]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)) =
  S (finProdFinEquiv (j, 0)) * ∑ x, T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x))
  rw [Finset.mul_sumn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)) =
  ∑ i, S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)) =
  ∑ i, S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∑ x, (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)) =
  ∑ i, S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))
  apply Finset.sum_congrhn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ Finset.univ = Finset.univan:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∀ x ∈ Finset.univ,
  (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)) =
    S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)))
  ·hn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ Finset.univ = Finset.univ rflAll goals completed! 🐙
  ·an:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6⊢ ∀ x ∈ Finset.univ,
  (familyUniversal n) S (finProdFinEquiv (j, x)) * T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x)) =
    S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, x)) * L (finProdFinEquiv (j, x))) intro i _an:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesa✝:i ∈ Finset.univ⊢ (familyUniversal n) S (finProdFinEquiv (j, i)) * T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)) =
  S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))
    erw [toSpecies_familyUniversalan:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesa✝:i ∈ Finset.univ⊢ (toSpecies j) S ⟨0, ⋯⟩ * T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)) =
  S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))]an:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesa✝:i ∈ Finset.univ⊢ (toSpecies j) S ⟨0, ⋯⟩ * T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)) =
  S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))
    simp only [toSpecies_apply, toSpeciesEquiv_apply, Fin.zero_eta, Fin.isValue, Nat.reduceMul]an:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesj:Fin 6i:Fin (SMνSpecies n).numberChargesa✝:i ∈ Finset.univ⊢ S (finProdFinEquiv (j, 0)) * T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)) =
  S (finProdFinEquiv (j, 0)) * (T (finProdFinEquiv (j, i)) * L (finProdFinEquiv (j, i)))
    ringAll goals completed! 🐙

lemma familyUniversal_accGrav (S : (SMνCharges 1).Charges) :
    accGrav (familyUniversal n S) = n * (accGrav S) := byn:ℕS:(SMνCharges 1).Charges⊢ accGrav ((familyUniversal n) S) = ↑n * accGrav S
  rw [accGrav_decomp,n:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i + 3 * ∑ i, U ((familyUniversal n) S) i + 3 * ∑ i, D ((familyUniversal n) S) i +
        2 * ∑ i, L ((familyUniversal n) S) i +
      ∑ i, E ((familyUniversal n) S) i +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * accGrav Sn:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i + 3 * ∑ i, U ((familyUniversal n) S) i + 3 * ∑ i, D ((familyUniversal n) S) i +
        2 * ∑ i, L ((familyUniversal n) S) i +
      ∑ i, E ((familyUniversal n) S) i +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i) accGrav_decompn:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i + 3 * ∑ i, U ((familyUniversal n) S) i + 3 * ∑ i, D ((familyUniversal n) S) i +
        2 * ∑ i, L ((familyUniversal n) S) i +
      ∑ i, E ((familyUniversal n) S) i +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)n:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i + 3 * ∑ i, U ((familyUniversal n) S) i + 3 * ∑ i, D ((familyUniversal n) S) i +
        2 * ∑ i, L ((familyUniversal n) S) i +
      ∑ i, E ((familyUniversal n) S) i +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)]n:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i + 3 * ∑ i, U ((familyUniversal n) S) i + 3 * ∑ i, D ((familyUniversal n) S) i +
        2 * ∑ i, L ((familyUniversal n) S) i +
      ∑ i, E ((familyUniversal n) S) i +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)
  repeat rw [sum_familyUniversal_onen:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + 3 * ∑ i, U ((familyUniversal n) S) i + 3 * ∑ i, D ((familyUniversal n) S) i +
        2 * ∑ i, L ((familyUniversal n) S) i +
      ∑ i, E ((familyUniversal n) S) i +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)]n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ +
    ∑ i, N ((familyUniversal n) S) i =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ =
  ↑n * (6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + ∑ i, N S i)
  simp only [Fin.isValue, toSpecies_apply, toSpeciesEquiv, Nat.reduceMul, Equiv.symm_trans,
    Equiv.arrowCongr_symm, Equiv.refl_symm, Equiv.symm_symm, sum_one]n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 0 ⟨0, ⋯⟩) +
            3 *
              (↑n *
                ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 1 ⟨0, ⋯⟩) +
          3 *
            (↑n * ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 2 ⟨0, ⋯⟩) +
        2 * (↑n * ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 3 ⟨0, ⋯⟩) +
      ↑n * ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 4 ⟨0, ⋯⟩ +
    ↑n * ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 5 ⟨0, ⋯⟩ =
  ↑n *
    (6 *
                ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 0
                  ⟨0, sum_one._proof_1⟩ +
              3 *
                ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 1
                  ⟨0, sum_one._proof_1⟩ +
            3 *
              ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 2
                ⟨0, sum_one._proof_1⟩ +
          2 *
            ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 3
              ⟨0, sum_one._proof_1⟩ +
        ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 4
          ⟨0, sum_one._proof_1⟩ +
      ((finProdFinEquiv.symm.arrowCongr (Equiv.refl ℚ)).trans (Equiv.curry (Fin 6) (Fin 1) ℚ)) S 5
        ⟨0, sum_one._proof_1⟩)
  ringAll goals completed! 🐙

lemma familyUniversal_accSU2 (S : (SMνCharges 1).Charges) :
    accSU2 (familyUniversal n S) = n * (accSU2 S) := byn:ℕS:(SMνCharges 1).Charges⊢ accSU2 ((familyUniversal n) S) = ↑n * accSU2 S
  rw [accSU2_decomp,n:ℕS:(SMνCharges 1).Charges⊢ 3 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, L ((familyUniversal n) S) i = ↑n * accSU2 Sn:ℕS:(SMνCharges 1).Charges⊢ 3 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, L ((familyUniversal n) S) i = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i) accSU2_decompn:ℕS:(SMνCharges 1).Charges⊢ 3 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, L ((familyUniversal n) S) i = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)n:ℕS:(SMνCharges 1).Charges⊢ 3 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, L ((familyUniversal n) S) i = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)]n:ℕS:(SMνCharges 1).Charges⊢ 3 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, L ((familyUniversal n) S) i = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)
  repeat rw [sum_familyUniversal_onen:ℕS:(SMνCharges 1).Charges⊢ 3 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ∑ i, L ((familyUniversal n) S) i = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)n:ℕS:(SMνCharges 1).Charges⊢ 3 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 3) S ⟨0, ⋯⟩ = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)]n:ℕS:(SMνCharges 1).Charges⊢ 3 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ∑ i, L ((familyUniversal n) S) i = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)n:ℕS:(SMνCharges 1).Charges⊢ 3 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 3) S ⟨0, ⋯⟩ = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)n:ℕS:(SMνCharges 1).Charges⊢ 3 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 3) S ⟨0, ⋯⟩ = ↑n * (3 * ∑ i, Q S i + ∑ i, L S i)
  simp only [Fin.isValue, toSpecies_apply, sum_one]n:ℕS:(SMνCharges 1).Charges⊢ 3 * (↑n * toSpeciesEquiv S 0 ⟨0, ⋯⟩) + ↑n * toSpeciesEquiv S 3 ⟨0, ⋯⟩ =
  ↑n * (3 * toSpeciesEquiv S 0 ⟨0, sum_one._proof_1⟩ + toSpeciesEquiv S 3 ⟨0, sum_one._proof_1⟩)
  ringAll goals completed! 🐙

lemma familyUniversal_accSU3 (S : (SMνCharges 1).Charges) :
    accSU3 (familyUniversal n S) = n * (accSU3 S) := byn:ℕS:(SMνCharges 1).Charges⊢ accSU3 ((familyUniversal n) S) = ↑n * accSU3 S
  rw [accSU3_decomp,n:ℕS:(SMνCharges 1).Charges⊢ 2 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, U ((familyUniversal n) S) i + ∑ i, D ((familyUniversal n) S) i =
  ↑n * accSU3 Sn:ℕS:(SMνCharges 1).Charges⊢ 2 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, U ((familyUniversal n) S) i + ∑ i, D ((familyUniversal n) S) i =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i) accSU3_decompn:ℕS:(SMνCharges 1).Charges⊢ 2 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, U ((familyUniversal n) S) i + ∑ i, D ((familyUniversal n) S) i =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)n:ℕS:(SMνCharges 1).Charges⊢ 2 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, U ((familyUniversal n) S) i + ∑ i, D ((familyUniversal n) S) i =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)]n:ℕS:(SMνCharges 1).Charges⊢ 2 * ∑ i, Q ((familyUniversal n) S) i + ∑ i, U ((familyUniversal n) S) i + ∑ i, D ((familyUniversal n) S) i =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)
  repeat rw [sum_familyUniversal_onen:ℕS:(SMνCharges 1).Charges⊢ 2 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ∑ i, U ((familyUniversal n) S) i + ∑ i, D ((familyUniversal n) S) i =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)n:ℕS:(SMνCharges 1).Charges⊢ 2 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 1) S ⟨0, ⋯⟩ + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)]n:ℕS:(SMνCharges 1).Charges⊢ 2 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 1) S ⟨0, ⋯⟩ + ∑ i, D ((familyUniversal n) S) i =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)n:ℕS:(SMνCharges 1).Charges⊢ 2 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 1) S ⟨0, ⋯⟩ + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)n:ℕS:(SMνCharges 1).Charges⊢ 2 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩) + ↑n * (toSpecies 1) S ⟨0, ⋯⟩ + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ =
  ↑n * (2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i)
  simp only [Fin.isValue, toSpecies_apply, sum_one]n:ℕS:(SMνCharges 1).Charges⊢ 2 * (↑n * toSpeciesEquiv S 0 ⟨0, ⋯⟩) + ↑n * toSpeciesEquiv S 1 ⟨0, ⋯⟩ + ↑n * toSpeciesEquiv S 2 ⟨0, ⋯⟩ =
  ↑n *
    (2 * toSpeciesEquiv S 0 ⟨0, sum_one._proof_1⟩ + toSpeciesEquiv S 1 ⟨0, sum_one._proof_1⟩ +
      toSpeciesEquiv S 2 ⟨0, sum_one._proof_1⟩)
  ringAll goals completed! 🐙

lemma familyUniversal_accYY (S : (SMνCharges 1).Charges) :
    accYY (familyUniversal n S) = n * (accYY S) := byn:ℕS:(SMνCharges 1).Charges⊢ accYY ((familyUniversal n) S) = ↑n * accYY S
  rw [accYY_decomp,n:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i + 8 * ∑ i, U ((familyUniversal n) S) i + 2 * ∑ i, D ((familyUniversal n) S) i +
      3 * ∑ i, L ((familyUniversal n) S) i +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * accYY Sn:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i + 8 * ∑ i, U ((familyUniversal n) S) i + 2 * ∑ i, D ((familyUniversal n) S) i +
      3 * ∑ i, L ((familyUniversal n) S) i +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i) accYY_decompn:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i + 8 * ∑ i, U ((familyUniversal n) S) i + 2 * ∑ i, D ((familyUniversal n) S) i +
      3 * ∑ i, L ((familyUniversal n) S) i +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)n:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i + 8 * ∑ i, U ((familyUniversal n) S) i + 2 * ∑ i, D ((familyUniversal n) S) i +
      3 * ∑ i, L ((familyUniversal n) S) i +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)]n:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i + 8 * ∑ i, U ((familyUniversal n) S) i + 2 * ∑ i, D ((familyUniversal n) S) i +
      3 * ∑ i, L ((familyUniversal n) S) i +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)
  repeat rw [sum_familyUniversal_onen:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ + 8 * ∑ i, U ((familyUniversal n) S) i + 2 * ∑ i, D ((familyUniversal n) S) i +
      3 * ∑ i, L ((familyUniversal n) S) i +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ + 8 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 2 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
      3 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
    6 * (↑n * (toSpecies 4) S ⟨0, ⋯⟩) =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)]n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ + 8 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 2 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
      3 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
    6 * ∑ i, E ((familyUniversal n) S) i =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ + 8 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 2 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
      3 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
    6 * (↑n * (toSpecies 4) S ⟨0, ⋯⟩) =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ + 8 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩) + 2 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩) +
      3 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩) +
    6 * (↑n * (toSpecies 4) S ⟨0, ⋯⟩) =
  ↑n * (∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i)
  simp only [Fin.isValue, toSpecies_apply, sum_one]n:ℕS:(SMνCharges 1).Charges⊢ ↑n * toSpeciesEquiv S 0 ⟨0, ⋯⟩ + 8 * (↑n * toSpeciesEquiv S 1 ⟨0, ⋯⟩) + 2 * (↑n * toSpeciesEquiv S 2 ⟨0, ⋯⟩) +
      3 * (↑n * toSpeciesEquiv S 3 ⟨0, ⋯⟩) +
    6 * (↑n * toSpeciesEquiv S 4 ⟨0, ⋯⟩) =
  ↑n *
    (toSpeciesEquiv S 0 ⟨0, sum_one._proof_1⟩ + 8 * toSpeciesEquiv S 1 ⟨0, sum_one._proof_1⟩ +
          2 * toSpeciesEquiv S 2 ⟨0, sum_one._proof_1⟩ +
        3 * toSpeciesEquiv S 3 ⟨0, sum_one._proof_1⟩ +
      6 * toSpeciesEquiv S 4 ⟨0, sum_one._proof_1⟩)
  ringAll goals completed! 🐙

lemma familyUniversal_quadBiLin (S : (SMνCharges 1).Charges) (T : (SMνCharges n).Charges) :
    quadBiLin (familyUniversal n S) T =
    S (0 : Fin 6) * ∑ i, Q T i - 2 * S (1 : Fin 6) * ∑ i, U T i + S (2 : Fin 6) *∑ i, D T i -
    S (3 : Fin 6) * ∑ i, L T i + S (4 : Fin 6) * ∑ i, E T i := byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ (quadBiLin ((familyUniversal n) S)) T =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i
  rw [quadBiLin_decompn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ ∑ i, Q ((familyUniversal n) S) i * Q T i - 2 * ∑ i, U ((familyUniversal n) S) i * U T i +
        ∑ i, D ((familyUniversal n) S) i * D T i -
      ∑ i, L ((familyUniversal n) S) i * L T i +
    ∑ i, E ((familyUniversal n) S) i * E T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ ∑ i, Q ((familyUniversal n) S) i * Q T i - 2 * ∑ i, U ((familyUniversal n) S) i * U T i +
        ∑ i, D ((familyUniversal n) S) i * D T i -
      ∑ i, L ((familyUniversal n) S) i * L T i +
    ∑ i, E ((familyUniversal n) S) i * E T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ ∑ i, Q ((familyUniversal n) S) i * Q T i - 2 * ∑ i, U ((familyUniversal n) S) i * U T i +
        ∑ i, D ((familyUniversal n) S) i * D T i -
      ∑ i, L ((familyUniversal n) S) i * L T i +
    ∑ i, E ((familyUniversal n) S) i * E T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i
  repeat rw [sum_familyUniversal_twon:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ (toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i - 2 * ∑ i, U ((familyUniversal n) S) i * U T i +
        ∑ i, D ((familyUniversal n) S) i * D T i -
      ∑ i, L ((familyUniversal n) S) i * L T i +
    ∑ i, E ((familyUniversal n) S) i * E T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ (toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i - 2 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i) +
        (toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i -
      (toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i +
    (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ (toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i - 2 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i) +
        (toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i -
      (toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i +
    ∑ i, E ((familyUniversal n) S) i * E T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ (toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i - 2 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i) +
        (toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i -
      (toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i +
    (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ (toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i - 2 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i) +
        (toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i -
      (toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i +
    (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i
  repeat rw [toSpecies_onen:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ S 0 * ∑ i, (toSpecies 0) T i - 2 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i) +
        (toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i -
      (toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i +
    (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ S 0 * ∑ i, (toSpecies 0) T i - 2 * (S 1 * ∑ i, (toSpecies 1) T i) + S 2 * ∑ i, (toSpecies 2) T i -
      S 3 * ∑ i, (toSpecies 3) T i +
    S 4 * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ S 0 * ∑ i, (toSpecies 0) T i - 2 * (S 1 * ∑ i, (toSpecies 1) T i) + S 2 * ∑ i, (toSpecies 2) T i -
      S 3 * ∑ i, (toSpecies 3) T i +
    (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ S 0 * ∑ i, (toSpecies 0) T i - 2 * (S 1 * ∑ i, (toSpecies 1) T i) + S 2 * ∑ i, (toSpecies 2) T i -
      S 3 * ∑ i, (toSpecies 3) T i +
    S 4 * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ S 0 * ∑ i, (toSpecies 0) T i - 2 * (S 1 * ∑ i, (toSpecies 1) T i) + S 2 * ∑ i, (toSpecies 2) T i -
      S 3 * ∑ i, (toSpecies 3) T i +
    S 4 * ∑ i, (toSpecies 4) T i =
  S 0 * ∑ i, Q T i - 2 * S 1 * ∑ i, U T i + S 2 * ∑ i, D T i - S 3 * ∑ i, L T i + S 4 * ∑ i, E T i
  simp only [Fin.isValue, toSpecies_apply, add_left_inj, sub_left_inj, sub_right_inj]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).Charges⊢ 2 * (S 1 * ∑ x, toSpeciesEquiv T 1 x) = 2 * S 1 * ∑ x, toSpeciesEquiv T 1 x
  ringAll goals completed! 🐙

lemma familyUniversal_accQuad (S : (SMνCharges 1).Charges) :
    accQuad (familyUniversal n S) = n * (accQuad S) := byn:ℕS:(SMνCharges 1).Charges⊢ accQuad ((familyUniversal n) S) = ↑n * accQuad S
  rw [accQuad_decompn:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i ^ 2 - 2 * ∑ i, U ((familyUniversal n) S) i ^ 2 + ∑ i, D ((familyUniversal n) S) i ^ 2 -
      ∑ i, L ((familyUniversal n) S) i ^ 2 +
    ∑ i, E ((familyUniversal n) S) i ^ 2 =
  ↑n * accQuad Sn:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i ^ 2 - 2 * ∑ i, U ((familyUniversal n) S) i ^ 2 + ∑ i, D ((familyUniversal n) S) i ^ 2 -
      ∑ i, L ((familyUniversal n) S) i ^ 2 +
    ∑ i, E ((familyUniversal n) S) i ^ 2 =
  ↑n * accQuad S]n:ℕS:(SMνCharges 1).Charges⊢ ∑ i, Q ((familyUniversal n) S) i ^ 2 - 2 * ∑ i, U ((familyUniversal n) S) i ^ 2 + ∑ i, D ((familyUniversal n) S) i ^ 2 -
      ∑ i, L ((familyUniversal n) S) i ^ 2 +
    ∑ i, E ((familyUniversal n) S) i ^ 2 =
  ↑n * accQuad S
  repeat erw [sum_familyUniversaln:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 2 - 2 * ∑ i, U ((familyUniversal n) S) i ^ 2 + ∑ i, D ((familyUniversal n) S) i ^ 2 -
      ∑ i, L ((familyUniversal n) S) i ^ 2 +
    ∑ i, E ((familyUniversal n) S) i ^ 2 =
  ↑n * accQuad S]n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 2 - 2 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 2) + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 2 -
      ↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 2 +
    ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 2 =
  ↑n * accQuad S
  rw [accQuad_decompn:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 2 - 2 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 2) + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 2 -
      ↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 2 +
    ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 2 =
  ↑n * (∑ i, Q S i ^ 2 - 2 * ∑ i, U S i ^ 2 + ∑ i, D S i ^ 2 - ∑ i, L S i ^ 2 + ∑ i, E S i ^ 2)n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 2 - 2 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 2) + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 2 -
      ↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 2 +
    ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 2 =
  ↑n * (∑ i, Q S i ^ 2 - 2 * ∑ i, U S i ^ 2 + ∑ i, D S i ^ 2 - ∑ i, L S i ^ 2 + ∑ i, E S i ^ 2)]n:ℕS:(SMνCharges 1).Charges⊢ ↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 2 - 2 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 2) + ↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 2 -
      ↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 2 +
    ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 2 =
  ↑n * (∑ i, Q S i ^ 2 - 2 * ∑ i, U S i ^ 2 + ∑ i, D S i ^ 2 - ∑ i, L S i ^ 2 + ∑ i, E S i ^ 2)
  simp only [Fin.isValue, toSpecies_apply, sum_one]n:ℕS:(SMνCharges 1).Charges⊢ ↑n * toSpeciesEquiv S 0 ⟨0, ⋯⟩ ^ 2 - 2 * (↑n * toSpeciesEquiv S 1 ⟨0, ⋯⟩ ^ 2) + ↑n * toSpeciesEquiv S 2 ⟨0, ⋯⟩ ^ 2 -
      ↑n * toSpeciesEquiv S 3 ⟨0, ⋯⟩ ^ 2 +
    ↑n * toSpeciesEquiv S 4 ⟨0, ⋯⟩ ^ 2 =
  ↑n *
    (toSpeciesEquiv S 0 ⟨0, sum_one._proof_1⟩ ^ 2 - 2 * toSpeciesEquiv S 1 ⟨0, sum_one._proof_1⟩ ^ 2 +
          toSpeciesEquiv S 2 ⟨0, sum_one._proof_1⟩ ^ 2 -
        toSpeciesEquiv S 3 ⟨0, sum_one._proof_1⟩ ^ 2 +
      toSpeciesEquiv S 4 ⟨0, sum_one._proof_1⟩ ^ 2)
  ringAll goals completed! 🐙

lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).Charges) (T R : (SMνCharges n).Charges) :
    cubeTriLin (familyUniversal n S) T R = 6 * S (0 : Fin 6) * ∑ i, (Q T i * Q R i) +
      3 * S (1 : Fin 6) * ∑ i, (U T i * U R i) + 3 * S (2 : Fin 6) * ∑ i, (D T i * D R i)
      + 2 * S (3 : Fin 6) * ∑ i, (L T i * L R i) +
      S (4 : Fin 6) * ∑ i, (E T i * E R i) + S (5 : Fin 6) * ∑ i, (N T i * N R i) := byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ ((cubeTriLin ((familyUniversal n) S)) T) R =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i
  rw [cubeTriLin_decompn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i * Q T i * Q R i + 3 * ∑ i, U ((familyUniversal n) S) i * U T i * U R i +
          3 * ∑ i, D ((familyUniversal n) S) i * D T i * D R i +
        2 * ∑ i, L ((familyUniversal n) S) i * L T i * L R i +
      ∑ i, E ((familyUniversal n) S) i * E T i * E R i +
    ∑ i, N ((familyUniversal n) S) i * N T i * N R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i * Q T i * Q R i + 3 * ∑ i, U ((familyUniversal n) S) i * U T i * U R i +
          3 * ∑ i, D ((familyUniversal n) S) i * D T i * D R i +
        2 * ∑ i, L ((familyUniversal n) S) i * L T i * L R i +
      ∑ i, E ((familyUniversal n) S) i * E T i * E R i +
    ∑ i, N ((familyUniversal n) S) i * N T i * N R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i * Q T i * Q R i + 3 * ∑ i, U ((familyUniversal n) S) i * U T i * U R i +
          3 * ∑ i, D ((familyUniversal n) S) i * D T i * D R i +
        2 * ∑ i, L ((familyUniversal n) S) i * L T i * L R i +
      ∑ i, E ((familyUniversal n) S) i * E T i * E R i +
    ∑ i, N ((familyUniversal n) S) i * N T i * N R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i
  repeat rw [sum_familyUniversal_threen:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ((toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) +
            3 * ∑ i, U ((familyUniversal n) S) i * U T i * U R i +
          3 * ∑ i, D ((familyUniversal n) S) i * D T i * D R i +
        2 * ∑ i, L ((familyUniversal n) S) i * L T i * L R i +
      ∑ i, E ((familyUniversal n) S) i * E T i * E R i +
    ∑ i, N ((familyUniversal n) S) i * N T i * N R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ((toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) +
            3 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * ((toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * ((toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    (toSpecies 5) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ((toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) +
            3 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * ((toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * ((toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    ∑ i, N ((familyUniversal n) S) i * N T i * N R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ((toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) +
            3 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * ((toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * ((toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    (toSpecies 5) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * ((toSpecies 0) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) +
            3 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * ((toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * ((toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    (toSpecies 5) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i
  repeat rw [toSpecies_onen:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * (S 0 * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) +
            3 * ((toSpecies 1) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * ((toSpecies 2) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * ((toSpecies 3) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      (toSpecies 4) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    (toSpecies 5) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * (S 0 * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) + 3 * (S 1 * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * (S 2 * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * (S 3 * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      S 4 * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    S 5 * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * (S 0 * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) + 3 * (S 1 * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * (S 2 * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * (S 3 * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      S 4 * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    (toSpecies 5) S ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * (S 0 * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) + 3 * (S 1 * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * (S 2 * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * (S 3 * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      S 4 * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    S 5 * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * (S 0 * ∑ i, (toSpecies 0) T i * (toSpecies 0) R i) + 3 * (S 1 * ∑ i, (toSpecies 1) T i * (toSpecies 1) R i) +
          3 * (S 2 * ∑ i, (toSpecies 2) T i * (toSpecies 2) R i) +
        2 * (S 3 * ∑ i, (toSpecies 3) T i * (toSpecies 3) R i) +
      S 4 * ∑ i, (toSpecies 4) T i * (toSpecies 4) R i +
    S 5 * ∑ i, (toSpecies 5) T i * (toSpecies 5) R i =
  6 * S 0 * ∑ i, Q T i * Q R i + 3 * S 1 * ∑ i, U T i * U R i + 3 * S 2 * ∑ i, D T i * D R i +
        2 * S 3 * ∑ i, L T i * L R i +
      S 4 * ∑ i, E T i * E R i +
    S 5 * ∑ i, N T i * N R i
  simp only [Fin.isValue, toSpecies_apply, add_left_inj]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Charges⊢ 6 * (S 0 * ∑ x, toSpeciesEquiv T 0 x * toSpeciesEquiv R 0 x) +
        3 * (S 1 * ∑ x, toSpeciesEquiv T 1 x * toSpeciesEquiv R 1 x) +
      3 * (S 2 * ∑ x, toSpeciesEquiv T 2 x * toSpeciesEquiv R 2 x) +
    2 * (S 3 * ∑ x, toSpeciesEquiv T 3 x * toSpeciesEquiv R 3 x) =
  6 * S 0 * ∑ x, toSpeciesEquiv T 0 x * toSpeciesEquiv R 0 x +
        3 * S 1 * ∑ x, toSpeciesEquiv T 1 x * toSpeciesEquiv R 1 x +
      3 * S 2 * ∑ x, toSpeciesEquiv T 2 x * toSpeciesEquiv R 2 x +
    2 * S 3 * ∑ x, toSpeciesEquiv T 3 x * toSpeciesEquiv R 3 x
  ringAll goals completed! 🐙

lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).Charges) (R : (SMνCharges n).Charges) :
    cubeTriLin (familyUniversal n S) (familyUniversal n T) R =
      6 * S (0 : Fin 6) * T (0 : Fin 6) * ∑ i, Q R i +
      3 * S (1 : Fin 6) * T (1 : Fin 6) * ∑ i, U R i
      + 3 * S (2 : Fin 6) * T (2 : Fin 6) * ∑ i, D R i +
      2 * S (3 : Fin 6) * T (3 : Fin 6) * ∑ i, L R i +
      S (4 : Fin 6) * T (4 : Fin 6) * ∑ i, E R i + S (5 : Fin 6) * T (5 : Fin 6) * ∑ i, N R i := byn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ ((cubeTriLin ((familyUniversal n) S)) ((familyUniversal n) T)) R =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i
  rw [familyUniversal_cubeTriLinn:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ∑ i, Q ((familyUniversal n) T) i * Q R i + 3 * S 1 * ∑ i, U ((familyUniversal n) T) i * U R i +
          3 * S 2 * ∑ i, D ((familyUniversal n) T) i * D R i +
        2 * S 3 * ∑ i, L ((familyUniversal n) T) i * L R i +
      S 4 * ∑ i, E ((familyUniversal n) T) i * E R i +
    S 5 * ∑ i, N ((familyUniversal n) T) i * N R i =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ∑ i, Q ((familyUniversal n) T) i * Q R i + 3 * S 1 * ∑ i, U ((familyUniversal n) T) i * U R i +
          3 * S 2 * ∑ i, D ((familyUniversal n) T) i * D R i +
        2 * S 3 * ∑ i, L ((familyUniversal n) T) i * L R i +
      S 4 * ∑ i, E ((familyUniversal n) T) i * E R i +
    S 5 * ∑ i, N ((familyUniversal n) T) i * N R i =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ∑ i, Q ((familyUniversal n) T) i * Q R i + 3 * S 1 * ∑ i, U ((familyUniversal n) T) i * U R i +
          3 * S 2 * ∑ i, D ((familyUniversal n) T) i * D R i +
        2 * S 3 * ∑ i, L ((familyUniversal n) T) i * L R i +
      S 4 * ∑ i, E ((familyUniversal n) T) i * E R i +
    S 5 * ∑ i, N ((familyUniversal n) T) i * N R i =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i
  repeat rw [sum_familyUniversal_twon:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ((toSpecies 0) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) R i) + 3 * S 1 * ∑ i, U ((familyUniversal n) T) i * U R i +
          3 * S 2 * ∑ i, D ((familyUniversal n) T) i * D R i +
        2 * S 3 * ∑ i, L ((familyUniversal n) T) i * L R i +
      S 4 * ∑ i, E ((familyUniversal n) T) i * E R i +
    S 5 * ∑ i, N ((familyUniversal n) T) i * N R i =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ((toSpecies 0) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) R i) +
            3 * S 1 * ((toSpecies 1) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * ((toSpecies 2) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * ((toSpecies 3) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) R i) +
      S 4 * ((toSpecies 4) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) R i) +
    S 5 * ((toSpecies 5) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ((toSpecies 0) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) R i) +
            3 * S 1 * ((toSpecies 1) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * ((toSpecies 2) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * ((toSpecies 3) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) R i) +
      S 4 * ((toSpecies 4) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) R i) +
    S 5 * ∑ i, N ((familyUniversal n) T) i * N R i =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ((toSpecies 0) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) R i) +
            3 * S 1 * ((toSpecies 1) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * ((toSpecies 2) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * ((toSpecies 3) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) R i) +
      S 4 * ((toSpecies 4) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) R i) +
    S 5 * ((toSpecies 5) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * ((toSpecies 0) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 0) R i) +
            3 * S 1 * ((toSpecies 1) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * ((toSpecies 2) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * ((toSpecies 3) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) R i) +
      S 4 * ((toSpecies 4) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) R i) +
    S 5 * ((toSpecies 5) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i
  repeat rw [toSpecies_onen:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * (T 0 * ∑ i, (toSpecies 0) R i) + 3 * S 1 * ((toSpecies 1) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * ((toSpecies 2) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * ((toSpecies 3) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 3) R i) +
      S 4 * ((toSpecies 4) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 4) R i) +
    S 5 * ((toSpecies 5) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * (T 0 * ∑ i, (toSpecies 0) R i) + 3 * S 1 * (T 1 * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * (T 2 * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * (T 3 * ∑ i, (toSpecies 3) R i) +
      S 4 * (T 4 * ∑ i, (toSpecies 4) R i) +
    S 5 * (T 5 * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * (T 0 * ∑ i, (toSpecies 0) R i) + 3 * S 1 * (T 1 * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * (T 2 * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * (T 3 * ∑ i, (toSpecies 3) R i) +
      S 4 * (T 4 * ∑ i, (toSpecies 4) R i) +
    S 5 * ((toSpecies 5) T ⟨0, ⋯⟩ * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * (T 0 * ∑ i, (toSpecies 0) R i) + 3 * S 1 * (T 1 * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * (T 2 * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * (T 3 * ∑ i, (toSpecies 3) R i) +
      S 4 * (T 4 * ∑ i, (toSpecies 4) R i) +
    S 5 * (T 5 * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R in:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * (T 0 * ∑ i, (toSpecies 0) R i) + 3 * S 1 * (T 1 * ∑ i, (toSpecies 1) R i) +
          3 * S 2 * (T 2 * ∑ i, (toSpecies 2) R i) +
        2 * S 3 * (T 3 * ∑ i, (toSpecies 3) R i) +
      S 4 * (T 4 * ∑ i, (toSpecies 4) R i) +
    S 5 * (T 5 * ∑ i, (toSpecies 5) R i) =
  6 * S 0 * T 0 * ∑ i, Q R i + 3 * S 1 * T 1 * ∑ i, U R i + 3 * S 2 * T 2 * ∑ i, D R i + 2 * S 3 * T 3 * ∑ i, L R i +
      S 4 * T 4 * ∑ i, E R i +
    S 5 * T 5 * ∑ i, N R i
  simp only [Fin.isValue, toSpecies_apply]n:ℕS:(SMνCharges 1).ChargesT:(SMνCharges 1).ChargesR:(SMνCharges n).Charges⊢ 6 * S 0 * (T 0 * ∑ x, toSpeciesEquiv R 0 x) + 3 * S 1 * (T 1 * ∑ x, toSpeciesEquiv R 1 x) +
          3 * S 2 * (T 2 * ∑ x, toSpeciesEquiv R 2 x) +
        2 * S 3 * (T 3 * ∑ x, toSpeciesEquiv R 3 x) +
      S 4 * (T 4 * ∑ x, toSpeciesEquiv R 4 x) +
    S 5 * (T 5 * ∑ x, toSpeciesEquiv R 5 x) =
  6 * S 0 * T 0 * ∑ x, toSpeciesEquiv R 0 x + 3 * S 1 * T 1 * ∑ x, toSpeciesEquiv R 1 x +
          3 * S 2 * T 2 * ∑ x, toSpeciesEquiv R 2 x +
        2 * S 3 * T 3 * ∑ x, toSpeciesEquiv R 3 x +
      S 4 * T 4 * ∑ x, toSpeciesEquiv R 4 x +
    S 5 * T 5 * ∑ x, toSpeciesEquiv R 5 x
  ringAll goals completed! 🐙

lemma familyUniversal_accCube (S : (SMνCharges 1).Charges) :
    accCube (familyUniversal n S) = n * (accCube S) := byn:ℕS:(SMνCharges 1).Charges⊢ accCube ((familyUniversal n) S) = ↑n * accCube S
  rw [accCube_decompn:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i ^ 3 + 3 * ∑ i, U ((familyUniversal n) S) i ^ 3 +
          3 * ∑ i, D ((familyUniversal n) S) i ^ 3 +
        2 * ∑ i, L ((familyUniversal n) S) i ^ 3 +
      ∑ i, E ((familyUniversal n) S) i ^ 3 +
    ∑ i, N ((familyUniversal n) S) i ^ 3 =
  ↑n * accCube Sn:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i ^ 3 + 3 * ∑ i, U ((familyUniversal n) S) i ^ 3 +
          3 * ∑ i, D ((familyUniversal n) S) i ^ 3 +
        2 * ∑ i, L ((familyUniversal n) S) i ^ 3 +
      ∑ i, E ((familyUniversal n) S) i ^ 3 +
    ∑ i, N ((familyUniversal n) S) i ^ 3 =
  ↑n * accCube S]n:ℕS:(SMνCharges 1).Charges⊢ 6 * ∑ i, Q ((familyUniversal n) S) i ^ 3 + 3 * ∑ i, U ((familyUniversal n) S) i ^ 3 +
          3 * ∑ i, D ((familyUniversal n) S) i ^ 3 +
        2 * ∑ i, L ((familyUniversal n) S) i ^ 3 +
      ∑ i, E ((familyUniversal n) S) i ^ 3 +
    ∑ i, N ((familyUniversal n) S) i ^ 3 =
  ↑n * accCube S
  repeat erw [sum_familyUniversaln:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 3) + 3 * ∑ i, U ((familyUniversal n) S) i ^ 3 +
          3 * ∑ i, D ((familyUniversal n) S) i ^ 3 +
        2 * ∑ i, L ((familyUniversal n) S) i ^ 3 +
      ∑ i, E ((familyUniversal n) S) i ^ 3 +
    ∑ i, N ((familyUniversal n) S) i ^ 3 =
  ↑n * accCube S]n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 3) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 3) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 3 +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ ^ 3 =
  ↑n * accCube S
  rw [accCube_decompn:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 3) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 3) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 3 +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ ^ 3 =
  ↑n *
    (6 * ∑ i, Q S i ^ 3 + 3 * ∑ i, U S i ^ 3 + 3 * ∑ i, D S i ^ 3 + 2 * ∑ i, L S i ^ 3 + ∑ i, E S i ^ 3 +
      ∑ i, N S i ^ 3)n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 3) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 3) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 3 +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ ^ 3 =
  ↑n *
    (6 * ∑ i, Q S i ^ 3 + 3 * ∑ i, U S i ^ 3 + 3 * ∑ i, D S i ^ 3 + 2 * ∑ i, L S i ^ 3 + ∑ i, E S i ^ 3 +
      ∑ i, N S i ^ 3)]n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * (toSpecies 0) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 1) S ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * (toSpecies 2) S ⟨0, ⋯⟩ ^ 3) +
        2 * (↑n * (toSpecies 3) S ⟨0, ⋯⟩ ^ 3) +
      ↑n * (toSpecies 4) S ⟨0, ⋯⟩ ^ 3 +
    ↑n * (toSpecies 5) S ⟨0, ⋯⟩ ^ 3 =
  ↑n *
    (6 * ∑ i, Q S i ^ 3 + 3 * ∑ i, U S i ^ 3 + 3 * ∑ i, D S i ^ 3 + 2 * ∑ i, L S i ^ 3 + ∑ i, E S i ^ 3 +
      ∑ i, N S i ^ 3)
  simp only [Fin.isValue, toSpecies_apply, sum_one]n:ℕS:(SMνCharges 1).Charges⊢ 6 * (↑n * toSpeciesEquiv S 0 ⟨0, ⋯⟩ ^ 3) + 3 * (↑n * toSpeciesEquiv S 1 ⟨0, ⋯⟩ ^ 3) +
          3 * (↑n * toSpeciesEquiv S 2 ⟨0, ⋯⟩ ^ 3) +
        2 * (↑n * toSpeciesEquiv S 3 ⟨0, ⋯⟩ ^ 3) +
      ↑n * toSpeciesEquiv S 4 ⟨0, ⋯⟩ ^ 3 +
    ↑n * toSpeciesEquiv S 5 ⟨0, ⋯⟩ ^ 3 =
  ↑n *
    (6 * toSpeciesEquiv S 0 ⟨0, sum_one._proof_1⟩ ^ 3 + 3 * toSpeciesEquiv S 1 ⟨0, sum_one._proof_1⟩ ^ 3 +
            3 * toSpeciesEquiv S 2 ⟨0, sum_one._proof_1⟩ ^ 3 +
          2 * toSpeciesEquiv S 3 ⟨0, sum_one._proof_1⟩ ^ 3 +
        toSpeciesEquiv S 4 ⟨0, sum_one._proof_1⟩ ^ 3 +
      toSpeciesEquiv S 5 ⟨0, sum_one._proof_1⟩ ^ 3)
  ringAll goals completed! 🐙