Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3

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.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic

Plane Y₃ B₃ and an orthogonal third point

The plane spanned by Y₃, B₃ and third orthogonal point.

References

https://arxiv.org/pdf/2107.07926.pdf

@[expose] public section

The plane of linear solutions spanned by Y₃, B₃ and R, a point orthogonal to Y₃ and B₃.

def planeY₃B₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) : MSSMACC.LinSols :=
  a • Y₃.1.1 + b • B₃.1.1 + c • R.1

              lemma planeY₃B₃_val (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
    (planeY₃B₃ R a b c).val = a • Y₃.val + b • B₃.val + c • R.val := byR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ (planeY₃B₃ R a b c).val = a • Y₃.val + b • B₃.val + c • R.val
  rflAll goals completed! 🐙

lemma planeY₃B₃_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
    planeY₃B₃ R (d * a) (d * b) (d * c) = d • planeY₃B₃ R a b c := byR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ planeY₃B₃ R (d * a) (d * b) (d * c) = d • planeY₃B₃ R a b c
  apply ACCSystemLinear.LinSols.extR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (planeY₃B₃ R (d * a) (d * b) (d * c)).val = (d • planeY₃B₃ R a b c).val
  change _ = d • (planeY₃B₃ R a b c).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (planeY₃B₃ R (d * a) (d * b) (d * c)).val = d • (planeY₃B₃ R a b c).val
  rw [planeY₃B₃_val,R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • (planeY₃B₃ R a b c).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • (a • Y₃.val + b • B₃.val + c • R.val) planeY₃B₃_valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • (a • Y₃.val + b • B₃.val + c • R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • (a • Y₃.val + b • B₃.val + c • R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • (a • Y₃.val + b • B₃.val + c • R.val)
  rw [smul_add,R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • (a • Y₃.val + b • B₃.val) + d • c • R.valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • a • Y₃.val + d • b • B₃.val + d • c • R.val smul_addR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • a • Y₃.val + d • b • B₃.val + d • c • R.valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • a • Y₃.val + d • b • B₃.val + d • c • R.val]R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = d • a • Y₃.val + d • b • B₃.val + d • c • R.val
  rw [smul_smul,R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = (d * a) • Y₃.val + d • b • B₃.val + d • c • R.valAll goals completed! 🐙 smul_smul,R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = (d * a) • Y₃.val + (d * b) • B₃.val + d • c • R.valAll goals completed! 🐙 smul_smulR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.val = (d * a) • Y₃.val + (d * b) • B₃.val + (d * c) • R.valAll goals completed! 🐙]All goals completed! 🐙

lemma planeY₃B₃_eq (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h : a = a' ∧ b = b' ∧ c = c') :
    (planeY₃B₃ R a b c) = (planeY₃B₃ R a' b' c') := bya':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚh:a = a' ∧ b = b' ∧ c = c'⊢ planeY₃B₃ R a b c = planeY₃B₃ R a' b' c'
  rw [h.1,a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚh:a = a' ∧ b = b' ∧ c = c'⊢ planeY₃B₃ R a' b c = planeY₃B₃ R a' b' c'All goals completed! 🐙 h.2.1,a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚh:a = a' ∧ b = b' ∧ c = c'⊢ planeY₃B₃ R a' b' c = planeY₃B₃ R a' b' c'All goals completed! 🐙 h.2.2a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚh:a = a' ∧ b = b' ∧ c = c'⊢ planeY₃B₃ R a' b' c' = planeY₃B₃ R a' b' c'All goals completed! 🐙]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R.val ≠ 0)
    (h : (planeY₃B₃ R a b c).val = (planeY₃B₃ R a' b' c').val) :
    a = a' ∧ b = b' ∧ c = c' := bya':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:(planeY₃B₃ R a b c).val = (planeY₃B₃ R a' b' c').val⊢ a = a' ∧ b = b' ∧ c = c'
  rw [planeY₃B₃_val,a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = (planeY₃B₃ R a' b' c').val⊢ a = a' ∧ b = b' ∧ c = c'a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.val⊢ a = a' ∧ b = b' ∧ c = c' planeY₃B₃_vala':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.val⊢ a = a' ∧ b = b' ∧ c = c'a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.val⊢ a = a' ∧ b = b' ∧ c = c'] at ha':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.val⊢ a = a' ∧ b = b' ∧ c = c'
  have h1 := congrArg (fun S => dot Y₃.val S) ha':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:(dot Y₃.val) (a • Y₃.val + b • B₃.val + c • R.val) = (dot Y₃.val) (a' • Y₃.val + b' • B₃.val + c' • R.val)⊢ a = a' ∧ b = b' ∧ c = c'
  have h2 := congrArg (fun S => dot B₃.val S) ha':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:(dot Y₃.val) (a • Y₃.val + b • B₃.val + c • R.val) = (dot Y₃.val) (a' • Y₃.val + b' • B₃.val + c' • R.val)h2:(dot B₃.val) (a • Y₃.val + b • B₃.val + c • R.val) = (dot B₃.val) (a' • Y₃.val + b' • B₃.val + c' • R.val)⊢ a = a' ∧ b = b' ∧ c = c'
  simp only [dot.map_add₂, dot.map_smul₂, R.perpY₃, R.perpB₃,
    show dot Y₃.val Y₃.val = 216 by with_unfolding_all rfl,
    show dot B₃.val B₃.val = 108 by with_unfolding_all rfl,
    show dot Y₃.val B₃.val = 108 by with_unfolding_all rfl,
    show dot B₃.val Y₃.val = 108 by with_unfolding_all rfl,
    mul_zero, add_zero] at h1 h2a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108⊢ a = a' ∧ b = b' ∧ c = c'
  have ha : a = a' := by linaritha':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'⊢ a = a' ∧ b = b' ∧ c = c'a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'⊢ a = a' ∧ b = b' ∧ c = c'
  have hb : b = b' := by linaritha':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c'a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c'
  rw [ha,a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a' • Y₃.val + b • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c'a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a' • Y₃.val + b' • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c' hba':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a' • Y₃.val + b' • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c'a':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a' • Y₃.val + b' • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c'] at ha':ℚb':ℚc':ℚR:AnomalyFreePerpa:ℚb:ℚc:ℚhR':R.val ≠ 0h:a' • Y₃.val + b' • B₃.val + c • R.val = a' • Y₃.val + b' • B₃.val + c' • R.valh1:a * 216 + b * 108 = a' * 216 + b' * 108h2:a * 108 + b * 108 = a' * 108 + b' * 108ha:a = a'hb:b = b'⊢ a = a' ∧ b = b' ∧ c = c'
  exact ⟨ha, hb, smul_left_injective ℚ hR' (add_left_cancel h)⟩All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
    accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin Y₃.val R.val
    + 2 * b * quadBiLin B₃.val R.val + c * quadBiLin R.val R.val) := byR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (planeY₃B₃ R a b c).val =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [planeY₃B₃_valR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (a • Y₃.val + b • B₃.val + c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (a • Y₃.val + b • B₃.val + c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (a • Y₃.val + b • B₃.val + c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [accQuad,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ quadBiLin.toHomogeneousQuad (a • Y₃.val + b • B₃.val + c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ quadBiLin.toHomogeneousQuad (a • Y₃.val + b • B₃.val) + quadBiLin.toHomogeneousQuad (c • R.val) +
    2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) BiLinearSymm.toHomogeneousQuad_addR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ quadBiLin.toHomogeneousQuad (a • Y₃.val + b • B₃.val) + quadBiLin.toHomogeneousQuad (c • R.val) +
    2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ quadBiLin.toHomogeneousQuad (a • Y₃.val + b • B₃.val) + quadBiLin.toHomogeneousQuad (c • R.val) +
    2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ quadBiLin.toHomogeneousQuad (a • Y₃.val + b • B₃.val) + quadBiLin.toHomogeneousQuad (c • R.val) +
    2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [← lineY₃B₃Charges_val,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ quadBiLin.toHomogeneousQuad (lineY₃B₃Charges a b).val + quadBiLin.toHomogeneousQuad (c • R.val) +
    2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (lineY₃B₃Charges a b).val + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) ← accQuadR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (lineY₃B₃Charges a b).val + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (lineY₃B₃Charges a b).val + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (lineY₃B₃Charges a b).val + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [lineY₃B₃Charges_quadR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accQuad (c • R.val) + 2 * (quadBiLin (lineY₃B₃Charges a b).val) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [lineY₃B₃Charges_val,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accQuad (c • R.val) + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + quadBiLin.toHomogeneousQuad (c • R.val) + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) accQuadR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + quadBiLin.toHomogeneousQuad (c • R.val) + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + quadBiLin.toHomogeneousQuad (c • R.val) + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + quadBiLin.toHomogeneousQuad (c • R.val) + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [quadBiLin.toHomogeneousQuad.map_smulR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val + 2 * (quadBiLin (a • Y₃.val + b • B₃.val)) (c • R.val) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [quadBiLin.map_add₁,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * ((quadBiLin (a • Y₃.val)) (c • R.val) + (quadBiLin (b • B₃.val)) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (quadBiLin Y₃.val) (c • R.val) + b * (quadBiLin B₃.val) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) quadBiLin.map_smul₁,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (quadBiLin Y₃.val) (c • R.val) + (quadBiLin (b • B₃.val)) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (quadBiLin Y₃.val) (c • R.val) + b * (quadBiLin B₃.val) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) quadBiLin.map_smul₁R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (quadBiLin Y₃.val) (c • R.val) + b * (quadBiLin B₃.val) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (quadBiLin Y₃.val) (c • R.val) + b * (quadBiLin B₃.val) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (quadBiLin Y₃.val) (c • R.val) + b * (quadBiLin B₃.val) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [quadBiLin.map_smul₂,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (quadBiLin B₃.val) (c • R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) quadBiLin.map_smul₂R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * quadBiLin.toHomogeneousQuad R.val +
    2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  rw [show (BiLinearSymm.toHomogeneousQuad quadBiLin) R.val = quadBiLin R.val R.val byR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accQuad (planeY₃B₃ R a b c).val =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * (quadBiLin R.val) R.val + 2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val) rflAll goals completed! 🐙R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * (quadBiLin R.val) R.val + 2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 2 * (quadBiLin R.val) R.val + 2 * (a * (c * (quadBiLin Y₃.val) R.val) + b * (c * (quadBiLin B₃.val) R.val)) =
  c * (2 * a * (quadBiLin Y₃.val) R.val + 2 * b * (quadBiLin B₃.val) R.val + c * (quadBiLin R.val) R.val)
  ringAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
    accCube (planeY₃B₃ R a b c).val = c ^ 2 *
    (3 * a * cubeTriLin R.val R.val Y₃.val
    + 3 * b * cubeTriLin R.val R.val B₃.val + c * cubeTriLin R.val R.val R.val) := byR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (planeY₃B₃ R a b c).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [planeY₃B₃_valR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val + c • R.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val + c • R.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val + c • R.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [accCube,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ cubeTriLin.toCubic (a • Y₃.val + b • B₃.val + c • R.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val) + accCube (c • R.val) +
      3 * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) TriLinearSymm.toCubic_add,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ cubeTriLin.toCubic (a • Y₃.val + b • B₃.val) + cubeTriLin.toCubic (c • R.val) +
      3 * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val) + accCube (c • R.val) +
      3 * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) ← accCubeR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val) + accCube (c • R.val) +
      3 * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val) + accCube (c • R.val) +
      3 * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (a • Y₃.val + b • B₃.val) + accCube (c • R.val) +
      3 * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [← lineY₃B₃Charges_valR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (lineY₃B₃Charges a b).val + accCube (c • R.val) +
      3 * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (lineY₃B₃Charges a b).val + accCube (c • R.val) +
      3 * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (lineY₃B₃Charges a b).val + accCube (c • R.val) +
      3 * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [lineY₃B₃Charges_cubicR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) (c • R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [TriLinearSymm.map_smul₃,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (lineY₃B₃Charges a b).val) (lineY₃B₃Charges a b).val) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃Charges a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (lineY₃B₃ a b).val) (lineY₃B₃ a b).val) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) lineY₃B₃Charges_val,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (a • Y₃.val + b • B₃.val)) (a • Y₃.val + b • B₃.val)) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (lineY₃B₃ a b).val) (lineY₃B₃ a b).val) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) ← lineY₃B₃_valR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (lineY₃B₃ a b).val) (lineY₃B₃ a b).val) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (lineY₃B₃ a b).val) (lineY₃B₃ a b).val) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * ((cubeTriLin (lineY₃B₃ a b).val) (lineY₃B₃ a b).val) R.val) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [lineY₃B₃_doublePointR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * 0) + 3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * 0) + 3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * 0) + 3 * ((cubeTriLin (c • R.val)) (c • R.val)) (lineY₃B₃ a b).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [lineY₃B₃_val,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + accCube (c • R.val) + 3 * (c * 0) + 3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + cubeTriLin.toCubic (c • R.val) + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) accCubeR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + cubeTriLin.toCubic (c • R.val) + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + cubeTriLin.toCubic (c • R.val) + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + cubeTriLin.toCubic (c • R.val) + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [cubeTriLin.toCubic.map_smulR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * ((cubeTriLin (c • R.val)) (c • R.val)) (a • Y₃.val + b • B₃.val) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [cubeTriLin.map_smul₁,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * ((cubeTriLin R.val) (c • R.val)) (a • Y₃.val + b • B₃.val)) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * ((cubeTriLin R.val) R.val) (a • Y₃.val + b • B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) cubeTriLin.map_smul₂R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * ((cubeTriLin R.val) R.val) (a • Y₃.val + b • B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * ((cubeTriLin R.val) R.val) (a • Y₃.val + b • B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * ((cubeTriLin R.val) R.val) (a • Y₃.val + b • B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [cubeTriLin.map_add₃,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (((cubeTriLin R.val) R.val) (a • Y₃.val) + ((cubeTriLin R.val) R.val) (b • B₃.val)))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) cubeTriLin.map_smul₃,R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + ((cubeTriLin R.val) R.val) (b • B₃.val)))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) cubeTriLin.map_smul₃R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * cubeTriLin.toCubic R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  rw [show (TriLinearSymm.toCubic cubeTriLin) R.val = cubeTriLin R.val R.val R.val byR:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ accCube (planeY₃B₃ R a b c).val =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * ((cubeTriLin R.val) R.val) R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val) rflAll goals completed! 🐙R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * ((cubeTriLin R.val) R.val) R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)]R:AnomalyFreePerpa:ℚb:ℚc:ℚ⊢ 0 + c ^ 3 * ((cubeTriLin R.val) R.val) R.val + 3 * (c * 0) +
    3 * (c * (c * (a * ((cubeTriLin R.val) R.val) Y₃.val + b * ((cubeTriLin R.val) R.val) B₃.val))) =
  c ^ 2 *
    (3 * a * ((cubeTriLin R.val) R.val) Y₃.val + 3 * b * ((cubeTriLin R.val) R.val) B₃.val +
      c * ((cubeTriLin R.val) R.val) R.val)
  ringAll goals completed! 🐙

The line in the plane spanned by Y₃, B₃ and R which is in the quadratic, as LinSols.

def lineQuadAFL (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.LinSols :=
  planeY₃B₃ R (c2 * quadBiLin R.val R.val - 2 * c3 * quadBiLin B₃.val R.val)
  (2 * c3 * quadBiLin Y₃.val R.val - c1 * quadBiLin R.val R.val)
  (2 * c1 * quadBiLin B₃.val R.val - 2 * c2 * quadBiLin Y₃.val R.val)



lemma lineQuadAFL_quad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
    accQuad (lineQuadAFL R c1 c2 c3).val = 0 := byR:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ accQuad (lineQuadAFL R c1 c2 c3).val = 0
  rw [lineQuadAFL,R:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ accQuad
    (planeY₃B₃ R (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val)
        (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val)
        (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val)).val =
  0R:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) *
    (2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val) =
  0 planeY₃B₃_quadR:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) *
    (2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val) =
  0R:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) *
    (2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val) =
  0]R:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) *
    (2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val) =
  0
  rw [mul_eq_zeroR:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ 2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val = 0 ∨
  2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val =
    0R:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ 2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val = 0 ∨
  2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val =
    0]R:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ 2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val = 0 ∨
  2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
        2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val =
    0
  apply Or.inrR:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ 2 * (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val) * (quadBiLin Y₃.val) R.val +
      2 * (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val) * (quadBiLin B₃.val) R.val +
    (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val) * (quadBiLin R.val) R.val =
  0
  ringAll goals completed! 🐙

The line in the plane spanned by Y₃, B₃ and R which is in the quadratic.

def lineQuad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.QuadSols :=
  AnomalyFreeQuadMk' (lineQuadAFL R c1 c2 c3) (lineQuadAFL_quad R c1 c2 c3)

lemma lineQuad_val (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
    (lineQuad R c1 c2 c3).val = (planeY₃B₃ R
    (c2 * quadBiLin R.val R.val - 2 * c3 * quadBiLin B₃.val R.val)
    (2 * c3 * quadBiLin Y₃.val R.val - c1 * quadBiLin R.val R.val)
    (2 * c1 * quadBiLin B₃.val R.val - 2 * c2 * quadBiLin Y₃.val R.val)).val := byR:AnomalyFreePerpc1:ℚc2:ℚc3:ℚ⊢ (lineQuad R c1 c2 c3).val =
  (planeY₃B₃ R (c2 * (quadBiLin R.val) R.val - 2 * c3 * (quadBiLin B₃.val) R.val)
      (2 * c3 * (quadBiLin Y₃.val) R.val - c1 * (quadBiLin R.val) R.val)
      (2 * c1 * (quadBiLin B₃.val) R.val - 2 * c2 * (quadBiLin Y₃.val) R.val)).val
  rflAll goals completed! 🐙



lemma lineQuad_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
    lineQuad R (d * a) (d * b) (d * c) = d • lineQuad R a b c := byR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ lineQuad R (d * a) (d * b) (d * c) = d • lineQuad R a b c
  apply ACCSystemQuad.QuadSols.extR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineQuad R (d * a) (d * b) (d * c)).val = (d • lineQuad R a b c).val
  change _ = (d • planeY₃B₃ R _ _ _).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineQuad R (d * a) (d * b) (d * c)).val =
  (d •
      planeY₃B₃ R (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val)
        (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val)
        (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val)).val
  rw [← planeY₃B₃_smulR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineQuad R (d * a) (d * b) (d * c)).val =
  (planeY₃B₃ R (d * (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val))
      (d * (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val))
      (d * (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val))).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineQuad R (d * a) (d * b) (d * c)).val =
  (planeY₃B₃ R (d * (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val))
      (d * (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val))
      (d * (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val))).val]R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineQuad R (d * a) (d * b) (d * c)).val =
  (planeY₃B₃ R (d * (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val))
      (d * (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val))
      (d * (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val))).val
  rw [lineQuad_valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (planeY₃B₃ R (d * b * (quadBiLin R.val) R.val - 2 * (d * c) * (quadBiLin B₃.val) R.val)
      (2 * (d * c) * (quadBiLin Y₃.val) R.val - d * a * (quadBiLin R.val) R.val)
      (2 * (d * a) * (quadBiLin B₃.val) R.val - 2 * (d * b) * (quadBiLin Y₃.val) R.val)).val =
  (planeY₃B₃ R (d * (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val))
      (d * (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val))
      (d * (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val))).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (planeY₃B₃ R (d * b * (quadBiLin R.val) R.val - 2 * (d * c) * (quadBiLin B₃.val) R.val)
      (2 * (d * c) * (quadBiLin Y₃.val) R.val - d * a * (quadBiLin R.val) R.val)
      (2 * (d * a) * (quadBiLin B₃.val) R.val - 2 * (d * b) * (quadBiLin Y₃.val) R.val)).val =
  (planeY₃B₃ R (d * (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val))
      (d * (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val))
      (d * (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val))).val]R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (planeY₃B₃ R (d * b * (quadBiLin R.val) R.val - 2 * (d * c) * (quadBiLin B₃.val) R.val)
      (2 * (d * c) * (quadBiLin Y₃.val) R.val - d * a * (quadBiLin R.val) R.val)
      (2 * (d * a) * (quadBiLin B₃.val) R.val - 2 * (d * b) * (quadBiLin Y₃.val) R.val)).val =
  (planeY₃B₃ R (d * (b * (quadBiLin R.val) R.val - 2 * c * (quadBiLin B₃.val) R.val))
      (d * (2 * c * (quadBiLin Y₃.val) R.val - a * (quadBiLin R.val) R.val))
      (d * (2 * a * (quadBiLin B₃.val) R.val - 2 * b * (quadBiLin Y₃.val) R.val))).val
  ring_nfAll goals completed! 🐙

A helper function to simplify following expressions.

def α₁ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
  (3 * cubeTriLin T.val T.val B₃.val * quadBiLin T.val T.val -
    2 * cubeTriLin T.val T.val T.val * quadBiLin B₃.val T.val)

A helper function to simplify following expressions.

def α₂ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
  (2 * cubeTriLin T.val T.val T.val * quadBiLin Y₃.val T.val -
  3 * cubeTriLin T.val T.val Y₃.val * quadBiLin T.val T.val)

A helper function to simplify following expressions.

def α₃ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
  6 * ((cubeTriLin T.val T.val Y₃.val) * quadBiLin B₃.val T.val -
      (cubeTriLin T.val T.val B₃.val) * quadBiLin Y₃.val T.val)



lemma lineQuad_cube (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ : ℚ) :
    accCube (lineQuad R c₁ c₂ c₃).val =
    - 4 * (c₁ * quadBiLin B₃.val R.val - c₂ * quadBiLin Y₃.val R.val) ^ 2 *
    (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃) := byR:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ accCube (lineQuad R c₁ c₂ c₃).val =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 * (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃)
  rw [lineQuad_valR:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ accCube
    (planeY₃B₃ R (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val)
        (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val)
        (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val)).val =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 * (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃)R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ accCube
    (planeY₃B₃ R (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val)
        (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val)
        (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val)).val =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 * (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃)]R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ accCube
    (planeY₃B₃ R (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val)
        (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val)
        (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val)).val =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 * (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃)
  rw [planeY₃B₃_cubic,R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 * (α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃)R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        c₃) α₁,R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        α₂ R * c₂ +
      α₃ R * c₃)R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        c₃) α₂,R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      α₃ R * c₃)R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        c₃) α₃R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        c₃)R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        c₃)]R:AnomalyFreePerpc₁:ℚc₂:ℚc₃:ℚ⊢ (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    (3 * (c₂ * (quadBiLin R.val) R.val - 2 * c₃ * (quadBiLin B₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (2 * c₃ * (quadBiLin Y₃.val) R.val - c₁ * (quadBiLin R.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val +
      (2 * c₁ * (quadBiLin B₃.val) R.val - 2 * c₂ * (quadBiLin Y₃.val) R.val) * ((cubeTriLin R.val) R.val) R.val) =
  -4 * (c₁ * (quadBiLin B₃.val) R.val - c₂ * (quadBiLin Y₃.val) R.val) ^ 2 *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          c₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          c₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        c₃)
  ringAll goals completed! 🐙

The line in the plane spanned by Y₃, B₃ and R which is in the cubic.

def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
    MSSMACC.LinSols :=
  planeY₃B₃ R
    (a₂ * cubeTriLin R.val R.val R.val - 3 * a₃ * cubeTriLin R.val R.val B₃.val)
    (3 * a₃ * cubeTriLin R.val R.val Y₃.val - a₁ * cubeTriLin R.val R.val R.val)
    (3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val))

              

lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
    lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c := byR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c
  apply ACCSystemLinear.LinSols.extR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineCube R (d * a) (d * b) (d * c)).val = (d • lineCube R a b c).val
  change _ = (d • planeY₃B₃ R _ _ _).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineCube R (d * a) (d * b) (d * c)).val =
  (d •
      planeY₃B₃ R (b * ((cubeTriLin R.val) R.val) R.val - 3 * c * ((cubeTriLin R.val) R.val) B₃.val)
        (3 * c * ((cubeTriLin R.val) R.val) Y₃.val - a * ((cubeTriLin R.val) R.val) R.val)
        (3 * (a * ((cubeTriLin R.val) R.val) B₃.val - b * ((cubeTriLin R.val) R.val) Y₃.val))).val
  rw [← planeY₃B₃_smulR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineCube R (d * a) (d * b) (d * c)).val =
  (planeY₃B₃ R (d * (b * ((cubeTriLin R.val) R.val) R.val - 3 * c * ((cubeTriLin R.val) R.val) B₃.val))
      (d * (3 * c * ((cubeTriLin R.val) R.val) Y₃.val - a * ((cubeTriLin R.val) R.val) R.val))
      (d * (3 * (a * ((cubeTriLin R.val) R.val) B₃.val - b * ((cubeTriLin R.val) R.val) Y₃.val)))).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineCube R (d * a) (d * b) (d * c)).val =
  (planeY₃B₃ R (d * (b * ((cubeTriLin R.val) R.val) R.val - 3 * c * ((cubeTriLin R.val) R.val) B₃.val))
      (d * (3 * c * ((cubeTriLin R.val) R.val) Y₃.val - a * ((cubeTriLin R.val) R.val) R.val))
      (d * (3 * (a * ((cubeTriLin R.val) R.val) B₃.val - b * ((cubeTriLin R.val) R.val) Y₃.val)))).val]R:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (lineCube R (d * a) (d * b) (d * c)).val =
  (planeY₃B₃ R (d * (b * ((cubeTriLin R.val) R.val) R.val - 3 * c * ((cubeTriLin R.val) R.val) B₃.val))
      (d * (3 * c * ((cubeTriLin R.val) R.val) Y₃.val - a * ((cubeTriLin R.val) R.val) R.val))
      (d * (3 * (a * ((cubeTriLin R.val) R.val) B₃.val - b * ((cubeTriLin R.val) R.val) Y₃.val)))).val
  change (planeY₃B₃ R _ _ _).val = (planeY₃B₃ R _ _ _).valR:AnomalyFreePerpa:ℚb:ℚc:ℚd:ℚ⊢ (planeY₃B₃ R (d * b * ((cubeTriLin R.val) R.val) R.val - 3 * (d * c) * ((cubeTriLin R.val) R.val) B₃.val)
      (3 * (d * c) * ((cubeTriLin R.val) R.val) Y₃.val - d * a * ((cubeTriLin R.val) R.val) R.val)
      (3 * (d * a * ((cubeTriLin R.val) R.val) B₃.val - d * b * ((cubeTriLin R.val) R.val) Y₃.val))).val =
  (planeY₃B₃ R (d * (b * ((cubeTriLin R.val) R.val) R.val - 3 * c * ((cubeTriLin R.val) R.val) B₃.val))
      (d * (3 * c * ((cubeTriLin R.val) R.val) Y₃.val - a * ((cubeTriLin R.val) R.val) R.val))
      (d * (3 * (a * ((cubeTriLin R.val) R.val) B₃.val - b * ((cubeTriLin R.val) R.val) Y₃.val)))).val
  ring_nfAll goals completed! 🐙

lemma lineCube_cube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
    accCube (lineCube R a₁ a₂ a₃).val = 0 := byR:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ accCube (lineCube R a₁ a₂ a₃).val = 0
  rw [lineCube,R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ accCube
    (planeY₃B₃ R (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val)
        (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val)
        (3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val))).val =
  0R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ (3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val)) ^ 2 *
    (3 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          ((cubeTriLin R.val) R.val) B₃.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
        ((cubeTriLin R.val) R.val) R.val) =
  0 planeY₃B₃_cubicR:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ (3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val)) ^ 2 *
    (3 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          ((cubeTriLin R.val) R.val) B₃.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
        ((cubeTriLin R.val) R.val) R.val) =
  0R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ (3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val)) ^ 2 *
    (3 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          ((cubeTriLin R.val) R.val) B₃.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
        ((cubeTriLin R.val) R.val) R.val) =
  0]R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ (3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val)) ^ 2 *
    (3 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          ((cubeTriLin R.val) R.val) Y₃.val +
        3 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          ((cubeTriLin R.val) R.val) B₃.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
        ((cubeTriLin R.val) R.val) R.val) =
  0
  ring_nfAll goals completed! 🐙

lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
    accQuad (lineCube R a₁ a₂ a₃).val =
    3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val) *
    (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃) := byR:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ accQuad (lineCube R a₁ a₂ a₃).val =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃)
  rw [lineCube,R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ accQuad
    (planeY₃B₃ R (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val)
        (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val)
        (3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val))).val =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃)R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃) planeY₃B₃_quad,R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃)R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃) α₁,R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        α₂ R * a₂ +
      α₃ R * a₃)R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃) α₂,R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      α₃ R * a₃)R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃) α₃R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃)R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃)]R:AnomalyFreePerpa₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    (2 * (a₂ * ((cubeTriLin R.val) R.val) R.val - 3 * a₃ * ((cubeTriLin R.val) R.val) B₃.val) *
          (quadBiLin Y₃.val) R.val +
        2 * (3 * a₃ * ((cubeTriLin R.val) R.val) Y₃.val - a₁ * ((cubeTriLin R.val) R.val) R.val) *
          (quadBiLin B₃.val) R.val +
      3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin R.val) R.val) =
  3 * (a₁ * ((cubeTriLin R.val) R.val) B₃.val - a₂ * ((cubeTriLin R.val) R.val) Y₃.val) *
    ((3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
            2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
          a₁ +
        (2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
            3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
          a₂ +
      6 *
          (((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
            ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val) *
        a₃)
  ringAll goals completed! 🐙

lemma α₃_proj (T : MSSMACC.Sols) : α₃ (proj T.1.1) =
    6 * dot Y₃.val B₃.val ^ 3 *
    (cubeTriLin T.val T.val Y₃.val * quadBiLin B₃.val T.val -
    cubeTriLin T.val T.val B₃.val * quadBiLin Y₃.val T.val) := byT:MSSMACC.Sols⊢ α₃ (proj T.toLinSols) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)
  rw [α₃,T:MSSMACC.Sols⊢ 6 *
    (((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) Y₃.val * (quadBiLin B₃.val) (proj T.toLinSols).val -
      ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) B₃.val * (quadBiLin Y₃.val) (proj T.toLinSols).val) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val) cube_proj_proj_Y₃,T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) (proj T.toLinSols).val -
      ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) B₃.val * (quadBiLin Y₃.val) (proj T.toLinSols).val) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val) cube_proj_proj_B₃,T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) (proj T.toLinSols).val -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) (proj T.toLinSols).val) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val) quad_B₃_proj,T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) (proj T.toLinSols).val) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val) quad_Y₃_projT:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)]T:MSSMACC.Sols⊢ 6 *
    ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val * ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) -
      (dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val * ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val)) =
  6 * (dot Y₃.val) B₃.val ^ 3 *
    (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
      ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)
  ringAll goals completed! 🐙

lemma α₂_proj (T : MSSMACC.Sols) : α₂ (proj T.1.1) =
    - α₃ (proj T.1.1) * (dot Y₃.val T.val - 2 * dot B₃.val T.val) := byT:MSSMACC.Sols⊢ α₂ (proj T.toLinSols) = -α₃ (proj T.toLinSols) * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)
  rw [α₃_proj,T:MSSMACC.Sols⊢ α₂ (proj T.toLinSols) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) α₂,T:MSSMACC.Sols⊢ 2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin Y₃.val) (proj T.toLinSols).val -
    3 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) Y₃.val *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) cube_proj_proj_Y₃,T:MSSMACC.Sols⊢ 2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin Y₃.val) (proj T.toLinSols).val -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) quad_Y₃_proj,T:MSSMACC.Sols⊢ 2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) quad_proj,T:MSSMACC.Sols⊢ 2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) cube_projT:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)]T:MSSMACC.Sols⊢ 2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin Y₃.val) T.val) -
    3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) Y₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)
  ringAll goals completed! 🐙

lemma α₁_proj (T : MSSMACC.Sols) : α₁ (proj T.1.1) =
    - α₃ (proj T.1.1) * (dot B₃.val T.val - dot Y₃.val T.val) := byT:MSSMACC.Sols⊢ α₁ (proj T.toLinSols) = -α₃ (proj T.toLinSols) * ((dot B₃.val) T.val - (dot Y₃.val) T.val)
  rw [α₃_proj,T:MSSMACC.Sols⊢ α₁ (proj T.toLinSols) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)T:MSSMACC.Sols⊢ 3 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) B₃.val *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin B₃.val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val) α₁T:MSSMACC.Sols⊢ 3 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) B₃.val *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin B₃.val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)T:MSSMACC.Sols⊢ 3 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) B₃.val *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin B₃.val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)]T:MSSMACC.Sols⊢ 3 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) B₃.val *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin B₃.val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)
  rw [cube_proj_proj_B₃,T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      (quadBiLin B₃.val) (proj T.toLinSols).val =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val) quad_B₃_proj,T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (quadBiLin (proj T.toLinSols).val) (proj T.toLinSols).val -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val) quad_proj,T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 * ((cubeTriLin (proj T.toLinSols).val) (proj T.toLinSols).val) (proj T.toLinSols).val *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val) cube_projT:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)]T:MSSMACC.Sols⊢ 3 * ((dot Y₃.val) B₃.val ^ 2 * ((cubeTriLin T.val) T.val) B₃.val) *
      (2 * (dot Y₃.val) B₃.val *
        (((dot B₃.val) T.val - (dot Y₃.val) T.val) * (quadBiLin Y₃.val) T.val +
          ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * (quadBiLin B₃.val) T.val)) -
    2 *
        (3 * (dot Y₃.val) B₃.val ^ 2 *
          (((dot B₃.val) T.val - (dot Y₃.val) T.val) * ((cubeTriLin T.val) T.val) Y₃.val +
            ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) * ((cubeTriLin T.val) T.val) B₃.val)) *
      ((dot Y₃.val) B₃.val * (quadBiLin B₃.val) T.val) =
  -(6 * (dot Y₃.val) B₃.val ^ 3 *
        (((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
          ((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val)) *
    ((dot B₃.val) T.val - (dot Y₃.val) T.val)
  ringAll goals completed! 🐙

lemma α₁_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
    α₁ (proj T.1.1) = 0 := byT:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ α₁ (proj T.toLinSols) = 0
  rw [α₁_proj,T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -α₃ (proj T.toLinSols) * ((dot B₃.val) T.val - (dot Y₃.val) T.val) = 0T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot B₃.val) T.val - (dot Y₃.val) T.val) = 0 h1T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot B₃.val) T.val - (dot Y₃.val) T.val) = 0T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot B₃.val) T.val - (dot Y₃.val) T.val) = 0]T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot B₃.val) T.val - (dot Y₃.val) T.val) = 0
  exact mul_eq_zero_of_left rfl ((dot B₃.val) T.val - (dot Y₃.val) T.val)All goals completed! 🐙

lemma α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
    α₂ (proj T.1.1) = 0 := byT:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ α₂ (proj T.toLinSols) = 0
  rw [α₂_proj,T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -α₃ (proj T.toLinSols) * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) = 0T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) = 0 h1T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) = 0T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) = 0]T:MSSMACC.Solsh1:α₃ (proj T.toLinSols) = 0⊢ -0 * ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val) = 0
  exact mul_eq_zero_of_left rfl ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)All goals completed! 🐙