Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization

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.StandardModel.AnomalyCancellation.NoGrav.Basic
public import Mathlib.NumberTheory.FLT.Three

Parameterizations for solutions to the linear ACCs for 1 family

In this file we give two parameterizations

linearParameters of solutions to the linear ACCs for 1 family

linearParametersQENeqZero of solutions to the linear ACCs for 1 family with Q and E non-zero

These parameterizations are based on: https://arxiv.org/abs/1907.00514

@[expose] public section

The parameters for a linear parameterization to the solution of the linear ACCs.

The parameter Q'.

The parameter Y.

The parameter E'.

              structure linearParameters where  Q' : ℚ  Y : ℚ  E' : ℚ

@[ext]
lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E' = T.E') :
    S = T := byS:linearParametersT:linearParametershQ:S.Q' = T.Q'hY:S.Y = T.YhE:S.E' = T.E'⊢ S = T
  cases' SmkT:linearParametersQ'✝:ℚY✝:ℚE'✝:ℚhQ:{ Q' := Q'✝, Y := Y✝, E' := E'✝ }.Q' = T.Q'hY:{ Q' := Q'✝, Y := Y✝, E' := E'✝ }.Y = T.YhE:{ Q' := Q'✝, Y := Y✝, E' := E'✝ }.E' = T.E'⊢ { Q' := Q'✝, Y := Y✝, E' := E'✝ } = T
  simp_all onlyAll goals completed! 🐙

The map from the linear parameters to elements of (SMNoGrav 1).charges.

def asCharges (S : linearParameters) : (SMNoGrav 1).Charges := fun i =>
  match i with
  | (0 : Fin 5) => S.Q'
  | (1 : Fin 5) => S.Y - S.Q'
  | (2 : Fin 5) => - (S.Y + S.Q')
  | (3: Fin 5) => - 3 * S.Q'
  | (4 : Fin 5) => S.E'

lemma speciesVal (S : linearParameters) :
    toSpeciesEquiv S.asCharges= fun i _ => S.asCharges i := byS:linearParameters⊢ toSpeciesEquiv S.asCharges = fun i x => S.asCharges i
  funext i jS:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges i j = S.asCharges i
  match j with
  | (0 : Fin 1) =>S:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges i 0 = S.asCharges i
  match i with
  | 0 =>S:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges 0 0 = S.asCharges 0 rflAll goals completed! 🐙
  | 1 =>S:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges 1 0 = S.asCharges 1 rflAll goals completed! 🐙
  | 2 =>S:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges 2 0 = S.asCharges 2 rflAll goals completed! 🐙
  | 3 =>S:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges 3 0 = S.asCharges 3 rflAll goals completed! 🐙
  | 4 =>S:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ toSpeciesEquiv S.asCharges 4 0 = S.asCharges 4 rflAll goals completed! 🐙

lemma toSpecies_apply_asCharges (S : linearParameters) (i : Fin 5) :
    toSpecies i S.asCharges = fun _ => S.asCharges i := byS:linearParametersi:Fin 5⊢ (toSpecies i) S.asCharges = fun x => S.asCharges i
  funext jS:linearParametersi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ (toSpecies i) S.asCharges j = S.asCharges i
  simp only [SMCharges.toSpecies_apply_eq, speciesVal]All goals completed! 🐙

The map from the linear parameters to elements of (SMNoGrav 1).LinSols.

def asLinear (S : linearParameters) : (SMNoGrav 1).LinSols :=
  chargeToLinear S.asCharges (byS:linearParameters⊢ accSU2 S.asCharges = 0
    simp only [accSU2, toSpecies_apply_asCharges, Fin.isValue, sum_SMSpecies_numberCharges_one,
      LinearMap.coe_mk, AddHom.coe_mk]S:linearParameters⊢ 3 * S.asCharges 0 + S.asCharges 3 = 0
    simp [asCharges]All goals completed! 🐙)
    (byS:linearParameters⊢ accSU3 S.asCharges = 0
    simp only [accSU3, SMCharges.toSpecies_apply_eq, sum_SMSpecies_numberCharges_one,
      LinearMap.coe_mk, AddHom.coe_mk, speciesVal, asCharges, neg_add_rev]S:linearParameters⊢ 2 * S.Q' + (S.Y - S.Q') + (-S.Q' + -S.Y) = 0
    ringAll goals completed! 🐙)

              lemma asLinear_val (S : linearParameters) : S.asLinear.val = S.asCharges := byS:linearParameters⊢ S.asLinear.val = S.asCharges
  rflAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma cubic (S : linearParameters) :
    accCube (S.asCharges) = - 54 * S.Q'^3 - 18 * S.Q' * S.Y ^ 2 + S.E'^3 := byS:linearParameters⊢ accCube S.asCharges = -54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3
  simp only [HomogeneousCubic, accCube, cubeTriLin, TriLinearSymm.toCubic_apply,
    TriLinearSymm.mk₃_toFun_apply_apply]S:linearParameters⊢ ∑ x,
    (6 * (Q S.asCharges x * Q S.asCharges x * Q S.asCharges x) +
            3 * (U S.asCharges x * U S.asCharges x * U S.asCharges x) +
          3 * (D S.asCharges x * D S.asCharges x * D S.asCharges x) +
        2 * (L S.asCharges x * L S.asCharges x * L S.asCharges x) +
      E S.asCharges x * E S.asCharges x * E S.asCharges x) =
  -54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3
  simp only [toSpecies_apply, Fin.isValue, sum_SMSpecies_numberCharges_one, Fin.zero_eta, neg_mul]S:linearParameters⊢ 6 * (toSpeciesEquiv S.asCharges 0 0 * toSpeciesEquiv S.asCharges 0 0 * toSpeciesEquiv S.asCharges 0 0) +
          3 * (toSpeciesEquiv S.asCharges 1 0 * toSpeciesEquiv S.asCharges 1 0 * toSpeciesEquiv S.asCharges 1 0) +
        3 * (toSpeciesEquiv S.asCharges 2 0 * toSpeciesEquiv S.asCharges 2 0 * toSpeciesEquiv S.asCharges 2 0) +
      2 * (toSpeciesEquiv S.asCharges 3 0 * toSpeciesEquiv S.asCharges 3 0 * toSpeciesEquiv S.asCharges 3 0) +
    toSpeciesEquiv S.asCharges 4 0 * toSpeciesEquiv S.asCharges 4 0 * toSpeciesEquiv S.asCharges 4 0 =
  -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3
  repeat erw [speciesValS:linearParameters⊢ 6 * ((fun i x => S.asCharges i) 0 0 * (fun i x => S.asCharges i) 0 0 * (fun i x => S.asCharges i) 0 0) +
          3 * ((fun i x => S.asCharges i) 1 0 * (fun i x => S.asCharges i) 1 0 * (fun i x => S.asCharges i) 1 0) +
        3 * ((fun i x => S.asCharges i) 2 0 * (fun i x => S.asCharges i) 2 0 * (fun i x => S.asCharges i) 2 0) +
      2 * ((fun i x => S.asCharges i) 3 0 * (fun i x => S.asCharges i) 3 0 * (fun i x => S.asCharges i) 3 0) +
    (fun i x => S.asCharges i) 4 0 * (fun i x => S.asCharges i) 4 0 * (fun i x => S.asCharges i) 4 0 =
  -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3]S:linearParameters⊢ 6 * ((fun i x => S.asCharges i) 0 0 * (fun i x => S.asCharges i) 0 0 * (fun i x => S.asCharges i) 0 0) +
          3 * ((fun i x => S.asCharges i) 1 0 * (fun i x => S.asCharges i) 1 0 * (fun i x => S.asCharges i) 1 0) +
        3 * ((fun i x => S.asCharges i) 2 0 * (fun i x => S.asCharges i) 2 0 * (fun i x => S.asCharges i) 2 0) +
      2 * ((fun i x => S.asCharges i) 3 0 * (fun i x => S.asCharges i) 3 0 * (fun i x => S.asCharges i) 3 0) +
    (fun i x => S.asCharges i) 4 0 * (fun i x => S.asCharges i) 4 0 * (fun i x => S.asCharges i) 4 0 =
  -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3
  simp only [asCharges, neg_add_rev, neg_mul, mul_neg, neg_neg]S:linearParameters⊢ 6 * (S.Q' * S.Q' * S.Q') + 3 * ((S.Y - S.Q') * (S.Y - S.Q') * (S.Y - S.Q')) +
        3 * ((-S.Q' + -S.Y) * (-S.Q' + -S.Y) * (-S.Q' + -S.Y)) +
      -(2 * (3 * S.Q' * (3 * S.Q') * (3 * S.Q'))) +
    S.E' * S.E' * S.E' =
  -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3
  ringAll goals completed! 🐙

lemma cubic_zero_Q'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
    (h : S.Q' = 0) : S.E' = 0 := byS:linearParametershc:accCube S.asCharges = 0h:S.Q' = 0⊢ S.E' = 0
  rw [cubic,S:linearParametershc:-54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3 = 0h:S.Q' = 0⊢ S.E' = 0S:linearParametershc:-54 * 0 ^ 3 - 18 * 0 * S.Y ^ 2 + S.E' ^ 3 = 0h:S.Q' = 0⊢ S.E' = 0 hS:linearParametershc:-54 * 0 ^ 3 - 18 * 0 * S.Y ^ 2 + S.E' ^ 3 = 0h:S.Q' = 0⊢ S.E' = 0S:linearParametershc:-54 * 0 ^ 3 - 18 * 0 * S.Y ^ 2 + S.E' ^ 3 = 0h:S.Q' = 0⊢ S.E' = 0] at hcS:linearParametershc:-54 * 0 ^ 3 - 18 * 0 * S.Y ^ 2 + S.E' ^ 3 = 0h:S.Q' = 0⊢ S.E' = 0
  simpa using hcAll goals completed! 🐙

lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
    (h : S.E' = 0) : S.Q' = 0 := byS:linearParametershc:accCube S.asCharges = 0h:S.E' = 0⊢ S.Q' = 0
  rw [cubic,S:linearParametershc:-54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3 = 0h:S.E' = 0⊢ S.Q' = 0S:linearParametershc:-54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + 0 ^ 3 = 0h:S.E' = 0⊢ S.Q' = 0 hS:linearParametershc:-54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + 0 ^ 3 = 0h:S.E' = 0⊢ S.Q' = 0S:linearParametershc:-54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + 0 ^ 3 = 0h:S.E' = 0⊢ S.Q' = 0] at hcS:linearParametershc:-54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + 0 ^ 3 = 0h:S.E' = 0⊢ S.Q' = 0
  simp only [neg_mul, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at hcS:linearParametersh:S.E' = 0hc:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = 0⊢ S.Q' = 0
  have h1 : -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = - 18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q' := by
    ringS:linearParametersh:S.E' = 0hc:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'⊢ S.Q' = 0S:linearParametersh:S.E' = 0hc:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'⊢ S.Q' = 0
  rw [h1S:linearParametersh:S.E' = 0hc:-18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'⊢ S.Q' = 0S:linearParametersh:S.E' = 0hc:-18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'⊢ S.Q' = 0] at hcS:linearParametersh:S.E' = 0hc:-18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'⊢ S.Q' = 0
  simp only [neg_mul, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hcS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0 ∨ S.Q' = 0⊢ S.Q' = 0
  cases' hc with hc hcinlS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0⊢ S.Q' = 0inrS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:S.Q' = 0⊢ S.Q' = 0
  ·inlS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0⊢ S.Q' = 0 have h2 := (add_eq_zero_iff_of_nonneg (byS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0⊢ 0 ≤ 3 * S.Q' ^ 2inlS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0h2:3 * S.Q' ^ 2 = 0 ∧ S.Y ^ 2 = 0⊢ S.Q' = 0 nlinarithAll goals completed! 🐙inlS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0h2:3 * S.Q' ^ 2 = 0 ∧ S.Y ^ 2 = 0⊢ S.Q' = 0) (sq_nonneg S.Y)).mp hcinlS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0h2:3 * S.Q' ^ 2 = 0 ∧ S.Y ^ 2 = 0⊢ S.Q' = 0
    simp only [mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff,
      false_or] at h2inlS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:3 * S.Q' ^ 2 + S.Y ^ 2 = 0h2:S.Q' = 0 ∧ S.Y = 0⊢ S.Q' = 0
    exact h2.1All goals completed! 🐙
  ·inrS:linearParametersh:S.E' = 0h1:-(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = -18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q'hc:S.Q' = 0⊢ S.Q' = 0 exact hcAll goals completed! 🐙

The bijection between the type of linear parameters and (SMNoGrav 1).LinSols.

set_option backward.isDefEq.respectTransparency false in


def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
  toFun S := S.asLinear
  invFun S := ⟨SMCharges.Q S.val (0 : Fin 1), (SMCharges.U S.val (0 : Fin 1) -
      SMCharges.D S.val (0 : Fin 1))/2,
      SMCharges.E S.val (0 : Fin 1)⟩
  left_inv S := byS:linearParameters⊢ (fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S) = S
    apply linearParameters.exthQS:linearParameters⊢ ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S)).Q' = S.Q'hYS:linearParameters⊢ ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S)).Y = S.YhES:linearParameters⊢ ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S)).E' = S.E'
    ·hQS:linearParameters⊢ ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S)).Q' = S.Q' rflAll goals completed! 🐙
    ·hYS:linearParameters⊢ ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S)).Y = S.Y simp only [Fin.isValue]hYS:linearParameters⊢ (U S.asLinear.val 0 - D S.asLinear.val 0) / 2 = S.Y
      repeat erw [asLinear_valhYS:linearParameters⊢ (U S.asCharges 0 - D S.asCharges 0) / 2 = S.Y]hYS:linearParameters⊢ (U S.asCharges 0 - D S.asCharges 0) / 2 = S.Y
      simp only [Fin.isValue, toSpecies_apply]hYS:linearParameters⊢ (toSpeciesEquiv S.asCharges 1 0 - toSpeciesEquiv S.asCharges 2 0) / 2 = S.Y
      repeat erw [speciesValhYS:linearParameters⊢ ((fun i x => S.asCharges i) 1 0 - (fun i x => S.asCharges i) 2 0) / 2 = S.Y]hYS:linearParameters⊢ ((fun i x => S.asCharges i) 1 0 - (fun i x => S.asCharges i) 2 0) / 2 = S.Y
      simp only [asCharges, neg_add_rev]hYS:linearParameters⊢ (S.Y - S.Q' - (-S.Q' + -S.Y)) / 2 = S.Y
      ringAll goals completed! 🐙
    ·hES:linearParameters⊢ ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) ((fun S => S.asLinear) S)).E' = S.E' rflAll goals completed! 🐙
  right_inv S := byS:(SMNoGrav 1).LinSols⊢ (fun S => S.asLinear) ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) S) = S
    simp only [Fin.isValue, toSpecies_apply_eq]S:(SMNoGrav 1).LinSols⊢ { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
      E' := toSpeciesEquiv S.val 4 0 }.asLinear =
  S
    apply ACCSystemLinear.LinSols.extS:(SMNoGrav 1).LinSols⊢ { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asLinear.val =
  S.val
    rw [charges_eq_toSpecies_eqS:(SMNoGrav 1).LinSols⊢ ∀ (i : Fin 5),
  (toSpecies i)
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asLinear.val =
    (toSpecies i) S.valS:(SMNoGrav 1).LinSols⊢ ∀ (i : Fin 5),
  (toSpecies i)
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asLinear.val =
    (toSpecies i) S.val]S:(SMNoGrav 1).LinSols⊢ ∀ (i : Fin 5),
  (toSpecies i)
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asLinear.val =
    (toSpecies i) S.val
    intro iS:(SMNoGrav 1).LinSolsi:Fin 5⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
          E' := toSpeciesEquiv S.val 4 0 }.asLinear.val =
  (toSpecies i) S.val
    rw [asLinear_valS:(SMNoGrav 1).LinSolsi:Fin 5⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges =
  (toSpecies i) S.valS:(SMNoGrav 1).LinSolsi:Fin 5⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges =
  (toSpecies i) S.val]S:(SMNoGrav 1).LinSolsi:Fin 5⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges =
  (toSpecies i) S.val
    funext jS:(SMNoGrav 1).LinSolsi:Fin 5j:Fin (SMSpecies 1).numberCharges⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges
    j =
  (toSpecies i) S.val j
    have hj : j = (0 : Fin 1) := byS:(SMNoGrav 1).LinSols⊢ (fun S => S.asLinear) ((fun S => { Q' := Q S.val 0, Y := (U S.val 0 - D S.val 0) / 2, E' := E S.val 0 }) S) = SS:(SMNoGrav 1).LinSolsi:Fin 5j:Fin (SMSpecies 1).numberChargeshj:j = 0⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges
    j =
  (toSpecies i) S.val j
      match j with
      | ⟨0, _⟩ =>S:(SMNoGrav 1).LinSolsi:Fin 5j:Fin (SMSpecies 1).numberChargesisLt✝:0 < (SMSpecies 1).numberCharges⊢ ⟨0, isLt✝⟩ = 0S:(SMNoGrav 1).LinSolsi:Fin 5j:Fin (SMSpecies 1).numberChargeshj:j = 0⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges
    j =
  (toSpecies i) S.val j rflS:(SMNoGrav 1).LinSolsi:Fin 5j:Fin (SMSpecies 1).numberChargeshj:j = 0⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges
    j =
  (toSpecies i) S.val jS:(SMNoGrav 1).LinSolsi:Fin 5j:Fin (SMSpecies 1).numberChargeshj:j = 0⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges
    j =
  (toSpecies i) S.val j
    subst hjS:(SMNoGrav 1).LinSolsi:Fin 5⊢ (toSpecies i)
    { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
        E' := toSpeciesEquiv S.val 4 0 }.asCharges
    0 =
  (toSpecies i) S.val 0
    rw [toSpecies_apply_asChargesS:(SMNoGrav 1).LinSolsi:Fin 5⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0S:(SMNoGrav 1).LinSolsi:Fin 5⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0]S:(SMNoGrav 1).LinSolsi:Fin 5⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0
    have h1 := SU3Sol SS:(SMNoGrav 1).LinSolsi:Fin 5h1:accSU3 S.val = 0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0
    simp only [accSU3, toSpecies_apply_eq, Fin.isValue, sum_SMSpecies_numberCharges_one,
      LinearMap.coe_mk, AddHom.coe_mk] at h1S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0
    have h2 := SU2Sol SS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:accSU2 S.val = 0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0
    simp only [accSU2,
      Fin.isValue, toSpecies_apply_eq, sum_SMSpecies_numberCharges_one,
      LinearMap.coe_mk, AddHom.coe_mk] at h2S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        i)
    0 =
  (toSpecies i) S.val 0
    match i with
    | 0 =>S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        0)
    0 =
  (toSpecies 0) S.val 0 rflAll goals completed! 🐙
    | 1 =>S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        1)
    0 =
  (toSpecies 1) S.val 0
      simp only [asCharges, Fin.isValue, toSpecies_apply_eq]S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2 - toSpeciesEquiv S.val 0 0 = toSpeciesEquiv S.val 1 0
      field_simpS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0 - 2 * toSpeciesEquiv S.val 0 0 = toSpeciesEquiv S.val 1 0 * 2
      linear_combination (norm := ring_nfaS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0 - toSpeciesEquiv S.val 0 0 * 2 +
        toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ * 2 +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0) -(1 * h1)
      simp only [Fin.isValue, Fin.zero_eta, toSpeciesEquiv_apply, Nat.reduceMul]aS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -S.val (finProdFinEquiv (1, 0)) - S.val (finProdFinEquiv (2, 0)) - S.val (finProdFinEquiv (0, 0)) * 2 +
        S.val (finProdFinEquiv (0, 0)) * 2 +
      S.val (finProdFinEquiv (1, 0)) +
    S.val (finProdFinEquiv (2, 0)) =
  0
      ringAll goals completed! 🐙
    | 2 =>S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        2)
    0 =
  (toSpecies 2) S.val 0
      simp only [asCharges, Fin.isValue, neg_add_rev, toSpecies_apply_eq]S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -toSpeciesEquiv S.val 0 0 + -((toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2) = toSpeciesEquiv S.val 2 0
      field_simpS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(toSpeciesEquiv S.val 0 0 * 2) + -(toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) = toSpeciesEquiv S.val 2 0 * 2
      linear_combination (norm := ring_nfaS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(toSpeciesEquiv S.val 0 0 * 2) - toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0 +
        toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ * 2 +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0) -(1 * h1)
      simp only [Fin.isValue, Fin.zero_eta, toSpeciesEquiv_apply, Nat.reduceMul]aS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(S.val (finProdFinEquiv (0, 0)) * 2) - S.val (finProdFinEquiv (1, 0)) - S.val (finProdFinEquiv (2, 0)) +
        S.val (finProdFinEquiv (0, 0)) * 2 +
      S.val (finProdFinEquiv (1, 0)) +
    S.val (finProdFinEquiv (2, 0)) =
  0
      ringAll goals completed! 🐙
    | 3 =>S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        3)
    0 =
  (toSpecies 3) S.val 0
      simp only [asCharges, Fin.isValue, neg_mul, toSpecies_apply_eq]S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(3 * toSpeciesEquiv S.val 0 0) = toSpeciesEquiv S.val 3 0
      field_simpS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(3 * toSpeciesEquiv S.val 0 0) = toSpeciesEquiv S.val 3 0
      linear_combination (norm := ring_nfaS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(toSpeciesEquiv S.val 0 0 * 3) + toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ * 3 +
      toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ -
    toSpeciesEquiv S.val 3 0 =
  0) -(1 * h2)
      simp only [Fin.isValue, Fin.zero_eta, toSpeciesEquiv_apply, Nat.reduceMul]aS:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ -(S.val (finProdFinEquiv (0, 0)) * 3) + S.val (finProdFinEquiv (0, 0)) * 3 + S.val (finProdFinEquiv (3, 0)) -
    S.val (finProdFinEquiv (3, 0)) =
  0
      ringAll goals completed! 🐙
    | 4 =>S:(SMNoGrav 1).LinSolsi:Fin 5h1:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ (fun x =>
      { Q' := toSpeciesEquiv S.val 0 0, Y := (toSpeciesEquiv S.val 1 0 - toSpeciesEquiv S.val 2 0) / 2,
            E' := toSpeciesEquiv S.val 4 0 }.asCharges
        4)
    0 =
  (toSpecies 4) S.val 0 rflAll goals completed! 🐙

The bijection between the linear parameters and (SMNoGrav 1).LinSols in the special case when Q and E are both not zero.

def bijectionQEZero : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} ≃
    {S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} where
  toFun S := ⟨bijection S, S.2⟩
  invFun S := ⟨bijection.symm S, S.2⟩
  left_inv S := Subtype.ext (bijection.left_inv S.1)
  right_inv S := Subtype.ext (bijection.right_inv S.1)



lemma grav (S : linearParameters) :
    accGrav S.asCharges = 0 ↔ S.E' = 6 * S.Q' := byS:linearParameters⊢ accGrav S.asCharges = 0 ↔ S.E' = 6 * S.Q'
  rw [accGravS:linearParameters⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
      S.asCharges =
    0 ↔
  S.E' = 6 * S.Q'S:linearParameters⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
      S.asCharges =
    0 ↔
  S.E' = 6 * S.Q']S:linearParameters⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
      S.asCharges =
    0 ↔
  S.E' = 6 * S.Q'
  simp only [toSpecies_apply_eq, Fin.isValue, sum_SMSpecies_numberCharges_one, LinearMap.coe_mk,
    AddHom.coe_mk]S:linearParameters⊢ 6 * toSpeciesEquiv S.asCharges 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
            3 * toSpeciesEquiv S.asCharges 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * toSpeciesEquiv S.asCharges 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        2 * toSpeciesEquiv S.asCharges 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.asCharges 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
    0 ↔
  S.E' = 6 * S.Q'
  repeat rw [speciesValS:linearParameters⊢ 6 * (fun i x => S.asCharges i) 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
            3 * (fun i x => S.asCharges i) 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * (fun i x => S.asCharges i) 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        2 * (fun i x => S.asCharges i) 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      (fun i x => S.asCharges i) 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
    0 ↔
  S.E' = 6 * S.Q'S:linearParameters⊢ 6 * (fun i x => S.asCharges i) 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
            3 * (fun i x => S.asCharges i) 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * (fun i x => S.asCharges i) 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        2 * (fun i x => S.asCharges i) 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      (fun i x => S.asCharges i) 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
    0 ↔
  S.E' = 6 * S.Q']S:linearParameters⊢ 6 * (fun i x => S.asCharges i) 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
            3 * (fun i x => S.asCharges i) 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * (fun i x => S.asCharges i) 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        2 * (fun i x => S.asCharges i) 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      (fun i x => S.asCharges i) 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
    0 ↔
  S.E' = 6 * S.Q'
  simp only [asCharges, neg_add_rev, neg_mul, mul_neg]S:linearParameters⊢ 6 * S.Q' + 3 * (S.Y - S.Q') + 3 * (-S.Q' + -S.Y) + -(2 * (3 * S.Q')) + S.E' = 0 ↔ S.E' = 6 * S.Q'
  ring_nfS:linearParameters⊢ -(S.Q' * 6) + S.E' = 0 ↔ S.E' = S.Q' * 6
  rw [add_comm,S:linearParameters⊢ S.E' + -(S.Q' * 6) = 0 ↔ S.E' = S.Q' * 6S:linearParameters⊢ S.E' = - -(S.Q' * 6) ↔ S.E' = S.Q' * 6 add_eq_zero_iff_eq_negS:linearParameters⊢ S.E' = - -(S.Q' * 6) ↔ S.E' = S.Q' * 6S:linearParameters⊢ S.E' = - -(S.Q' * 6) ↔ S.E' = S.Q' * 6]S:linearParameters⊢ S.E' = - -(S.Q' * 6) ↔ S.E' = S.Q' * 6
  simpAll goals completed! 🐙

The parameters for solutions to the linear ACCs with the condition that Q and E are non-zero.

The parameter x.

The parameter v.

The parameter w.

              structure linearParametersQENeqZero where  x : ℚ  v : ℚ  w : ℚ
  hx : x ≠ 0
  hvw : v + w ≠ 0

@[ext]
lemma ext {S T : linearParametersQENeqZero} (hx : S.x = T.x) (hv : S.v = T.v)
    (hw : S.w = T.w) : S = T := byS:linearParametersQENeqZeroT:linearParametersQENeqZerohx:S.x = T.xhv:S.v = T.vhw:S.w = T.w⊢ S = T
  cases' SmkT:linearParametersQENeqZerox✝:ℚv✝:ℚw✝:ℚhx✝:x✝ ≠ 0hvw✝:v✝ + w✝ ≠ 0hx:{ x := x✝, v := v✝, w := w✝, hx := hx✝, hvw := hvw✝ }.x = T.xhv:{ x := x✝, v := v✝, w := w✝, hx := hx✝, hvw := hvw✝ }.v = T.vhw:{ x := x✝, v := v✝, w := w✝, hx := hx✝, hvw := hvw✝ }.w = T.w⊢ { x := x✝, v := v✝, w := w✝, hx := hx✝, hvw := hvw✝ } = T
  simp_all onlyAll goals completed! 🐙

A map from linearParametersQENeqZero to linearParameters.


@[simps!]
def toLinearParameters (S : linearParametersQENeqZero) :
    {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} :=
  ⟨⟨S.x, 3 * S.x * (S.v - S.w) / (S.v + S.w), - 6 * S.x / (S.v + S.w)⟩,
    byS:linearParametersQENeqZero⊢ { Q' := S.x, Y := 3 * S.x * (S.v - S.w) / (S.v + S.w), E' := -6 * S.x / (S.v + S.w) }.Q' ≠ 0 ∧
  { Q' := S.x, Y := 3 * S.x * (S.v - S.w) / (S.v + S.w), E' := -6 * S.x / (S.v + S.w) }.E' ≠ 0
      apply And.intro S.hxS:linearParametersQENeqZero⊢ { Q' := S.x, Y := 3 * S.x * (S.v - S.w) / (S.v + S.w), E' := -6 * S.x / (S.v + S.w) }.E' ≠ 0
      simp only [neg_mul, ne_eq, div_eq_zero_iff, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero,
        false_or]S:linearParametersQENeqZero⊢ ¬(S.x = 0 ∨ S.v + S.w = 0)
      rw [not_orS:linearParametersQENeqZero⊢ ¬S.x = 0 ∧ ¬S.v + S.w = 0S:linearParametersQENeqZero⊢ ¬S.x = 0 ∧ ¬S.v + S.w = 0]S:linearParametersQENeqZero⊢ ¬S.x = 0 ∧ ¬S.v + S.w = 0
      exact And.intro S.hx S.hvwAll goals completed! 🐙⟩

A map from linearParameters to linearParametersQENeqZero in the special case when Q' and E' of the linear parameters are non-zero.

@[simps!]
def tolinearParametersQNeqZero (S : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0}) :
    linearParametersQENeqZero :=
  ⟨S.1.Q', - (3 * S.1.Q' + S.1.Y) / S.1.E', - (3 * S.1.Q' - S.1.Y)/ S.1.E', S.2.1,
    byS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ -(3 * (↑S).Q' + (↑S).Y) / (↑S).E' + -(3 * (↑S).Q' - (↑S).Y) / (↑S).E' ≠ 0
      simp only [ne_eq, neg_add_rev, neg_sub]S:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ ¬(-(↑S).Y + -(3 * (↑S).Q')) / (↑S).E' + ((↑S).Y - 3 * (↑S).Q') / (↑S).E' = 0
      field_simpS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ ¬(-(↑S).Y + -(3 * (↑S).Q') + ((↑S).Y - 3 * (↑S).Q')) / (↑S).E' = 0
      ring_nfS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ ¬-((↑S).Q' * (↑S).E'⁻¹ * 6) = 0
      simp only [neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, or_false]S:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ ¬((↑S).Q' = 0 ∨ (↑S).E'⁻¹ = 0)
      simpa using S.2All goals completed! 🐙⟩

A bijection between the type linearParametersQENeqZero and linear parameters with Q' and E' non-zero.

@[simps!]
def bijectionLinearParameters :
    linearParametersQENeqZero ≃ {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} where
  toFun := toLinearParameters
  invFun := tolinearParametersQNeqZero
  left_inv S := byS:linearParametersQENeqZero⊢ tolinearParametersQNeqZero S.toLinearParameters = S
    have hvw := S.hvwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0⊢ tolinearParametersQNeqZero S.toLinearParameters = S
    have hQ := S.hxS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ tolinearParametersQNeqZero S.toLinearParameters = S
    apply linearParametersQENeqZero.exthxS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (tolinearParametersQNeqZero S.toLinearParameters).x = S.xhvS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (tolinearParametersQNeqZero S.toLinearParameters).v = S.vhwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (tolinearParametersQNeqZero S.toLinearParameters).w = S.w
    ·hxS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (tolinearParametersQNeqZero S.toLinearParameters).x = S.x rflAll goals completed! 🐙
    ·hvS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (tolinearParametersQNeqZero S.toLinearParameters).v = S.v simp only [tolinearParametersQNeqZero_v, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
      toLinearParameters_coe_E']hvS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (-(3 * S.x * (S.v - S.w) / (S.v + S.w)) + -(3 * S.x)) / (-(6 * S.x) / (S.v + S.w)) = S.v
      field_simphvS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ -(3 * (-(S.v - S.w) + -(S.v + S.w))) = S.v * 6
      ringAll goals completed! 🐙
    ·hwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (tolinearParametersQNeqZero S.toLinearParameters).w = S.w simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
        toLinearParameters_coe_E']hwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (3 * S.x * (S.v - S.w) / (S.v + S.w) - 3 * S.x) / (-(6 * S.x) / (S.v + S.w)) = S.w
      field_simphwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ -(3 * (S.v - S.w - (S.v + S.w))) = S.w * 6
      ringAll goals completed! 🐙
  right_inv S := byS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ (tolinearParametersQNeqZero S).toLinearParameters = S
    apply Subtype.extS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }⊢ ↑(tolinearParametersQNeqZero S).toLinearParameters = ↑S
    have hQ := S.2.1S:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0⊢ ↑(tolinearParametersQNeqZero S).toLinearParameters = ↑S
    have hE := S.2.2S:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ ↑(tolinearParametersQNeqZero S).toLinearParameters = ↑S
    apply linearParameters.exthQS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑(tolinearParametersQNeqZero S).toLinearParameters).Q' = (↑S).Q'hYS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑(tolinearParametersQNeqZero S).toLinearParameters).Y = (↑S).YhES:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑(tolinearParametersQNeqZero S).toLinearParameters).E' = (↑S).E'
    ·hQS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑(tolinearParametersQNeqZero S).toLinearParameters).Q' = (↑S).Q' rflAll goals completed! 🐙
    ·hYS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑(tolinearParametersQNeqZero S).toLinearParameters).Y = (↑S).Y simp only [ne_eq, toLinearParameters_coe_Y, tolinearParametersQNeqZero_x,
      tolinearParametersQNeqZero_v, tolinearParametersQNeqZero_w]hYS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ 3 * (↑S).Q' * ((-(↑S).Y + -(3 * (↑S).Q')) / (↑S).E' - ((↑S).Y - 3 * (↑S).Q') / (↑S).E') /
    ((-(↑S).Y + -(3 * (↑S).Q')) / (↑S).E' + ((↑S).Y - 3 * (↑S).Q') / (↑S).E') =
  (↑S).Y
      field_simphYS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ 3 * (↑S).Q' * (-(↑S).Y + -(3 * (↑S).Q') - ((↑S).Y - 3 * (↑S).Q')) /
    (-(↑S).Y + -(3 * (↑S).Q') + ((↑S).Y - 3 * (↑S).Q')) =
  (↑S).Y
      ring_nfhYS:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑S).Q' * (↑S).Y * (↑S).Q'⁻¹ = (↑S).Y
      field_simp [hQ, hE]All goals completed! 🐙
    ·hES:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑(tolinearParametersQNeqZero S).toLinearParameters).E' = (↑S).E' simp only [ne_eq, toLinearParameters_coe_E', tolinearParametersQNeqZero_x,
      tolinearParametersQNeqZero_v, tolinearParametersQNeqZero_w]hES:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ -(6 * (↑S).Q') / ((-(↑S).Y + -(3 * (↑S).Q')) / (↑S).E' + ((↑S).Y - 3 * (↑S).Q') / (↑S).E') = (↑S).E'
      field_simphES:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ -(6 * (↑S).Q' / (-(↑S).Y + -((↑S).Q' * 3) + ((↑S).Y - (↑S).Q' * 3))) = 1
      ring_nfhES:{ S // S.Q' ≠ 0 ∧ S.E' ≠ 0 }hQ:(↑S).Q' ≠ 0hE:(↑S).E' ≠ 0⊢ (↑S).Q' * (↑S).Q'⁻¹ = 1
      field_simp [hQ, hE]All goals completed! 🐙

The bijection between linearParametersQENeqZero and LinSols with Q and E non-zero.

def bijection : linearParametersQENeqZero ≃
    {S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} :=
  bijectionLinearParameters.trans (linearParameters.bijectionQEZero)

              lemma bijection_coe_val (S : linearParametersQENeqZero) :
    (bijection S).1.val = (bijectionLinearParameters S : linearParameters).asCharges := rfl

lemma cubic (S : linearParametersQENeqZero) :
    accCube (bijection S).1.val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1 := byS:linearParametersQENeqZero⊢ accCube (↑(bijection S)).val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
  rw [bijection_coe_val,S:linearParametersQENeqZero⊢ accCube (↑(bijectionLinearParameters S)).asCharges = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1S:linearParametersQENeqZero⊢ -54 * (↑(bijectionLinearParameters S)).Q' ^ 3 -
        18 * (↑(bijectionLinearParameters S)).Q' * (↑(bijectionLinearParameters S)).Y ^ 2 +
      (↑(bijectionLinearParameters S)).E' ^ 3 =
    0 ↔
  S.v ^ 3 + S.w ^ 3 = -1 linearParameters.cubicS:linearParametersQENeqZero⊢ -54 * (↑(bijectionLinearParameters S)).Q' ^ 3 -
        18 * (↑(bijectionLinearParameters S)).Q' * (↑(bijectionLinearParameters S)).Y ^ 2 +
      (↑(bijectionLinearParameters S)).E' ^ 3 =
    0 ↔
  S.v ^ 3 + S.w ^ 3 = -1S:linearParametersQENeqZero⊢ -54 * (↑(bijectionLinearParameters S)).Q' ^ 3 -
        18 * (↑(bijectionLinearParameters S)).Q' * (↑(bijectionLinearParameters S)).Y ^ 2 +
      (↑(bijectionLinearParameters S)).E' ^ 3 =
    0 ↔
  S.v ^ 3 + S.w ^ 3 = -1]S:linearParametersQENeqZero⊢ -54 * (↑(bijectionLinearParameters S)).Q' ^ 3 -
        18 * (↑(bijectionLinearParameters S)).Q' * (↑(bijectionLinearParameters S)).Y ^ 2 +
      (↑(bijectionLinearParameters S)).E' ^ 3 =
    0 ↔
  S.v ^ 3 + S.w ^ 3 = -1
  simp only [ne_eq, bijectionLinearParameters_apply_coe_Q', neg_mul,
    bijectionLinearParameters_apply_coe_Y, div_pow, bijectionLinearParameters_apply_coe_E']S:linearParametersQENeqZero⊢ -(54 * S.x ^ 3) - 18 * S.x * ((3 * S.x * (S.v - S.w)) ^ 2 / (S.v + S.w) ^ 2) + (-(6 * S.x)) ^ 3 / (S.v + S.w) ^ 3 = 0 ↔
  S.v ^ 3 + S.w ^ 3 = -1
  have hvw := S.hvwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0⊢ -(54 * S.x ^ 3) - 18 * S.x * ((3 * S.x * (S.v - S.w)) ^ 2 / (S.v + S.w) ^ 2) + (-(6 * S.x)) ^ 3 / (S.v + S.w) ^ 3 = 0 ↔
  S.v ^ 3 + S.w ^ 3 = -1
  have hQ := S.hxS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ -(54 * S.x ^ 3) - 18 * S.x * ((3 * S.x * (S.v - S.w)) ^ 2 / (S.v + S.w) ^ 2) + (-(6 * S.x)) ^ 3 / (S.v + S.w) ^ 3 = 0 ↔
  S.v ^ 3 + S.w ^ 3 = -1
  field_simpS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ S.x ^ 3 * ((S.v + S.w) * (-(54 * (S.v + S.w) ^ 2) - 18 * 3 ^ 2 * (S.v - S.w) ^ 2) + -6 ^ 3) = (S.v + S.w) ^ 3 * 0 ↔
  S.v ^ 3 + S.w ^ 3 = -1
  simp [hQ]S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (S.v + S.w) * (-(54 * (S.v + S.w) ^ 2) - 18 * 3 ^ 2 * (S.v - S.w) ^ 2) + -6 ^ 3 = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
  ring_nfS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ -216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
  have h1 : -216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = - 216 *(S.v ^3 + S.w ^3 +1) := byS:linearParametersQENeqZero⊢ accCube (↑(bijection S)).val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -216 * (S.v ^ 3 + S.w ^ 3 + 1)⊢ -216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
    ringS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -216 * (S.v ^ 3 + S.w ^ 3 + 1)⊢ -216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -216 * (S.v ^ 3 + S.w ^ 3 + 1)⊢ -216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
  rw [h1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -216 * (S.v ^ 3 + S.w ^ 3 + 1)⊢ -216 * (S.v ^ 3 + S.w ^ 3 + 1) = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -216 * (S.v ^ 3 + S.w ^ 3 + 1)⊢ -216 * (S.v ^ 3 + S.w ^ 3 + 1) = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1]S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -216 * (S.v ^ 3 + S.w ^ 3 + 1)⊢ -216 * (S.v ^ 3 + S.w ^ 3 + 1) = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
  simp_allS:linearParametersQENeqZerohvw:¬S.v + S.w = 0hQ:¬S.x = 0h1:-216 - S.v ^ 3 * 216 - S.w ^ 3 * 216 = -(216 * (S.v ^ 3 + S.w ^ 3 + 1))⊢ S.v ^ 3 + S.w ^ 3 + 1 = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1
  exact add_eq_zero_iff_eq_negAll goals completed! 🐙

lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
    S.v = 0 ∨ S.w = 0 := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0⊢ S.v = 0 ∨ S.w = 0
  rw [S.cubicS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0] at hS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0
  have h1 : (-1)^3 = (-1 : ℚ) := by rflS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1h1:(-1) ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1h1:(-1) ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0
  rw [← h1S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0] at hS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1⊢ S.v = 0 ∨ S.w = 0
  by_contra hnS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬(S.v = 0 ∨ S.w = 0)⊢ False
  rw [not_orS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0⊢ FalseS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0⊢ False] at hnS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0⊢ False
  have FLTThree := fermatLastTheoremFor_iff_rat.mp fermatLastTheoremThreeS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0FLTThree:FermatLastTheoremWith ℚ 3⊢ False
  have h2 := FLTThree S.v S.w (-1) hn.1 hn.2 (Ne.symm (ne_of_beq_false (byS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0FLTThree:FermatLastTheoremWith ℚ 3⊢ (0 == -1) = falseS:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0FLTThree:FermatLastTheoremWith ℚ 3h2:S.v ^ 3 + S.w ^ 3 ≠ (-1) ^ 3⊢ False rflAll goals completed! 🐙S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0FLTThree:FermatLastTheoremWith ℚ 3h2:S.v ^ 3 + S.w ^ 3 ≠ (-1) ^ 3⊢ False)))S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = (-1) ^ 3h1:(-1) ^ 3 = -1hn:¬S.v = 0 ∧ ¬S.w = 0FLTThree:FermatLastTheoremWith ℚ 3h2:S.v ^ 3 + S.w ^ 3 ≠ (-1) ^ 3⊢ False
  exact h2 hAll goals completed! 🐙

lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
    (hv : S.v = 0) : S.w = -1 := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hv:S.v = 0⊢ S.w = -1
  rw [S.cubic,S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1hv:S.v = 0⊢ S.w = -1S:linearParametersQENeqZeroh:0 ^ 3 + S.w ^ 3 = -1hv:S.v = 0⊢ S.w = -1 hvS:linearParametersQENeqZeroh:0 ^ 3 + S.w ^ 3 = -1hv:S.v = 0⊢ S.w = -1S:linearParametersQENeqZeroh:0 ^ 3 + S.w ^ 3 = -1hv:S.v = 0⊢ S.w = -1] at hS:linearParametersQENeqZeroh:0 ^ 3 + S.w ^ 3 = -1hv:S.v = 0⊢ S.w = -1
  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_add] at hS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1⊢ S.w = -1
  have h' : (S.w + 1) * (1 * S.w * S.w + (-1) * S.w + 1) = 0 := by
    ring_nfS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1⊢ 1 + S.w ^ 3 = 0S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0⊢ S.w = -1
    exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0⊢ S.w = -1S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0⊢ S.w = -1
  have h'' : (1 * (S.w * S.w) + (-1) * S.w + 1) ≠ 0 := by
    refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.wS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0⊢ ∀ (s : ℚ), discrim 1 (-1) 1 ≠ s ^ 2S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
    intro sS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚ⊢ discrim 1 (-1) 1 ≠ s ^ 2S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
    by_contra hnS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ FalseS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
    have h : s ^ 2 < 0 := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hv:S.v = 0⊢ S.w = -1S:linearParametersQENeqZerohv:S.v = 0h✝:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
      rw [← hnS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ discrim 1 (-1) 1 < 0S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ discrim 1 (-1) 1 < 0S:linearParametersQENeqZerohv:S.v = 0h✝:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1]S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ discrim 1 (-1) 1 < 0S:linearParametersQENeqZerohv:S.v = 0h✝:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
      with_unfolding_all rflS:linearParametersQENeqZerohv:S.v = 0h✝:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1S:linearParametersQENeqZerohv:S.v = 0h✝:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
    nlinarithS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1S:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':(S.w + 1) * (1 * S.w * S.w + -1 * S.w + 1) = 0h'':1 * (S.w * S.w) + -1 * S.w + 1 ≠ 0⊢ S.w = -1
  simp_allS:linearParametersQENeqZerohv:S.v = 0h:S.w ^ 3 = -1h':S.w + 1 = 0h'':¬S.w * S.w + -S.w + 1 = 0⊢ S.w = -1
  exact eq_neg_of_add_eq_zero_left h'All goals completed! 🐙

lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
    (hw : S.w = 0) : S.v = -1 := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hw:S.w = 0⊢ S.v = -1
  rw [S.cubic,S:linearParametersQENeqZeroh:S.v ^ 3 + S.w ^ 3 = -1hw:S.w = 0⊢ S.v = -1S:linearParametersQENeqZeroh:S.v ^ 3 + 0 ^ 3 = -1hw:S.w = 0⊢ S.v = -1 hwS:linearParametersQENeqZeroh:S.v ^ 3 + 0 ^ 3 = -1hw:S.w = 0⊢ S.v = -1S:linearParametersQENeqZeroh:S.v ^ 3 + 0 ^ 3 = -1hw:S.w = 0⊢ S.v = -1] at hS:linearParametersQENeqZeroh:S.v ^ 3 + 0 ^ 3 = -1hw:S.w = 0⊢ S.v = -1
  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at hS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1⊢ S.v = -1
  have h' : (S.v + 1) * (1 * S.v * S.v + (-1) * S.v + 1) = 0 := by
    ring_nfS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1⊢ 1 + S.v ^ 3 = 0S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0⊢ S.v = -1
    exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0⊢ S.v = -1S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0⊢ S.v = -1
  have h'' : (1 * (S.v * S.v) + (-1) * S.v + 1) ≠ 0 := by
    refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.vS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0⊢ ∀ (s : ℚ), discrim 1 (-1) 1 ≠ s ^ 2S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
    intro sS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚ⊢ discrim 1 (-1) 1 ≠ s ^ 2S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
    by_contra hnS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ FalseS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
    have h : s ^ 2 < 0 := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hw:S.w = 0⊢ S.v = -1S:linearParametersQENeqZerohw:S.w = 0h✝:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
      rw [← hnS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ discrim 1 (-1) 1 < 0S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ discrim 1 (-1) 1 < 0S:linearParametersQENeqZerohw:S.w = 0h✝:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1]S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2⊢ discrim 1 (-1) 1 < 0S:linearParametersQENeqZerohw:S.w = 0h✝:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
      with_unfolding_all rflS:linearParametersQENeqZerohw:S.w = 0h✝:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1S:linearParametersQENeqZerohw:S.w = 0h✝:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0s:ℚhn:discrim 1 (-1) 1 = s ^ 2h:s ^ 2 < 0⊢ FalseS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
    nlinarithS:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':(S.v + 1) * (1 * S.v * S.v + -1 * S.v + 1) = 0h'':1 * (S.v * S.v) + -1 * S.v + 1 ≠ 0⊢ S.v = -1
  simp_all only [one_mul, neg_mul, mul_eq_zero, ne_eq, or_false]S:linearParametersQENeqZerohw:S.w = 0h:S.v ^ 3 = -1h':S.v + 1 = 0h'':¬S.v * S.v + -S.v + 1 = 0⊢ S.v = -1
  exact eq_neg_of_add_eq_zero_left h'All goals completed! 🐙lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
    (S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0⊢ S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1
  have h' := cubic_v_or_w_zero S hS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0h':S.v = 0 ∨ S.w = 0⊢ S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1
  cases' h' with hx hxinlS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hx:S.v = 0⊢ S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1inrS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hx:S.w = 0⊢ S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1
  ·inlS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hx:S.v = 0⊢ S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1 simpa [hx] using cubic_v_zero S h hxAll goals completed! 🐙
  ·inrS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0hx:S.w = 0⊢ S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1 simpa [hx] using cube_w_zero S h hxAll goals completed! 🐙

lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ S.v + S.w = -1 := byS:linearParametersQENeqZero⊢ accGrav (↑(bijection S)).val = 0 ↔ S.v + S.w = -1
  rw [bijection_coe_val,S:linearParametersQENeqZero⊢ accGrav (↑(bijectionLinearParameters S)).asCharges = 0 ↔ S.v + S.w = -1S:linearParametersQENeqZero⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1 linearParameters.gravS:linearParametersQENeqZero⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1S:linearParametersQENeqZero⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1]S:linearParametersQENeqZero⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1
  have hvw := S.hvwS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1
  have hQ := S.hxS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1
  field_simpS:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' ↔ S.v + S.w = -1
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:(↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q'⊢ S.v + S.w = -1refine_2S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:S.v + S.w = -1⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q'
  ·refine_1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:(↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q'⊢ S.v + S.w = -1 apply (mul_right_inj' hQ).mprefine_1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:(↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q'⊢ S.x * (S.v + S.w) = S.x * -1
    simp at hrefine_1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:-(6 * S.x) / (S.v + S.w) = 6 * S.x⊢ S.x * (S.v + S.w) = S.x * -1
    field_simp at hrefine_1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:-1 = S.v + S.w⊢ S.x * (S.v + S.w) = S.x * -1
    rw [← hrefine_1S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:-1 = S.v + S.w⊢ S.x * -1 = S.x * -1All goals completed! 🐙]All goals completed! 🐙
  ·refine_2S:linearParametersQENeqZerohvw:S.v + S.w ≠ 0hQ:S.x ≠ 0h:S.v + S.w = -1⊢ (↑(bijectionLinearParameters S)).E' = 6 * (↑(bijectionLinearParameters S)).Q' simp [h]All goals completed! 🐙

lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
    accGrav (bijection S).1.val = 0 := byS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0⊢ accGrav (↑(bijection S)).val = 0
  rw [gravS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0⊢ S.v + S.w = -1S:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0⊢ S.v + S.w = -1]S:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0⊢ S.v + S.w = -1
  have h' := cube_w_v S hS:linearParametersQENeqZeroh:accCube (↑(bijection S)).val = 0h':S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1⊢ S.v + S.w = -1
  cases' h' with h hinlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ S.v + S.w = -1inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ S.v + S.w = -1
  ·inlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ S.v + S.w = -1 rw [h.1,inlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ -1 + S.w = -1inlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ -1 + 0 = -1 h.2inlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ -1 + 0 = -1inlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ -1 + 0 = -1]inlS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = -1 ∧ S.w = 0⊢ -1 + 0 = -1
    exact Rat.add_zero (-1)All goals completed! 🐙
  ·inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ S.v + S.w = -1 rw [h.1,inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ 0 + S.w = -1inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ 0 + -1 = -1 h.2inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ 0 + -1 = -1inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ 0 + -1 = -1]inrS:linearParametersQENeqZeroh✝:accCube (↑(bijection S)).val = 0h:S.v = 0 ∧ S.w = -1⊢ 0 + -1 = -1
    exact Rat.zero_add (-1)All goals completed! 🐙