Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols — Physlib

Imports

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

public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
public import Mathlib.Tactic.LinearCombination

Plane of non-solutions

Working in the three family case, we show that there exists an eleven dimensional plane in the vector space of charges on which there are no solutions.

The main result of this file is eleven_dim_plane_of_no_sols_exists, which states that an 11 dimensional plane of charges exists on which there are no solutions except the origin.

@[expose] public section

A charge assignment forming one of the basis elements of the plane.

def B₀ : (PlusU1 3).Charges := ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₁ : (PlusU1 3).Charges := ![0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₂ : (PlusU1 3).Charges := ![0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₃ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₄ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₅ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₆ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₇ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₈ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0]

A charge assignment forming one of the basis elements of the plane.

def B₉ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0]

A charge assignment forming one of the basis elements of the plane.

def B₁₀ : (PlusU1 3).Charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]

The charge assignment forming a basis of the plane.

def B : Fin 11 → (PlusU1 3).Charges := fun i =>
  match i with
  | 0 => B₀
  | 1 => B₁
  | 2 => B₂
  | 3 => B₃
  | 4 => B₄
  | 5 => B₅
  | 6 => B₆
  | 7 => B₇
  | 8 => B₈
  | 9 => B₉
  | 10 => B₁₀

lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i) (B j) = 0 := byi:Fin 11j:Fin 11hi:i ≠ j⊢ (quadBiLin (B i)) (B j) = 0
  fin_cases i«0»j:Fin 11hi:(fun i => i) ⟨0, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨0, ⋯⟩))) (B j) = 0«1»j:Fin 11hi:(fun i => i) ⟨1, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨1, ⋯⟩))) (B j) = 0«2»j:Fin 11hi:(fun i => i) ⟨2, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨2, ⋯⟩))) (B j) = 0«3»j:Fin 11hi:(fun i => i) ⟨3, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨3, ⋯⟩))) (B j) = 0«4»j:Fin 11hi:(fun i => i) ⟨4, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨4, ⋯⟩))) (B j) = 0«5»j:Fin 11hi:(fun i => i) ⟨5, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨5, ⋯⟩))) (B j) = 0«6»j:Fin 11hi:(fun i => i) ⟨6, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨6, ⋯⟩))) (B j) = 0«7»j:Fin 11hi:(fun i => i) ⟨7, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨7, ⋯⟩))) (B j) = 0«8»j:Fin 11hi:(fun i => i) ⟨8, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨8, ⋯⟩))) (B j) = 0«9»j:Fin 11hi:(fun i => i) ⟨9, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨9, ⋯⟩))) (B j) = 0«10»j:Fin 11hi:(fun i => i) ⟨10, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B j) = 0 <;>«0»j:Fin 11hi:(fun i => i) ⟨0, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨0, ⋯⟩))) (B j) = 0«1»j:Fin 11hi:(fun i => i) ⟨1, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨1, ⋯⟩))) (B j) = 0«2»j:Fin 11hi:(fun i => i) ⟨2, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨2, ⋯⟩))) (B j) = 0«3»j:Fin 11hi:(fun i => i) ⟨3, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨3, ⋯⟩))) (B j) = 0«4»j:Fin 11hi:(fun i => i) ⟨4, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨4, ⋯⟩))) (B j) = 0«5»j:Fin 11hi:(fun i => i) ⟨5, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨5, ⋯⟩))) (B j) = 0«6»j:Fin 11hi:(fun i => i) ⟨6, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨6, ⋯⟩))) (B j) = 0«7»j:Fin 11hi:(fun i => i) ⟨7, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨7, ⋯⟩))) (B j) = 0«8»j:Fin 11hi:(fun i => i) ⟨8, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨8, ⋯⟩))) (B j) = 0«9»j:Fin 11hi:(fun i => i) ⟨9, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨9, ⋯⟩))) (B j) = 0«10»j:Fin 11hi:(fun i => i) ⟨10, ⋯⟩ ≠ j⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B j) = 0 fin_cases j«10».«0»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨0, ⋯⟩)) = 0«10».«1»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨1, ⋯⟩)) = 0«10».«2»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨2, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨2, ⋯⟩)) = 0«10».«3»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨3, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨3, ⋯⟩)) = 0«10».«4»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨4, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨4, ⋯⟩)) = 0«10».«5»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨5, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨5, ⋯⟩)) = 0«10».«6»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨6, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨6, ⋯⟩)) = 0«10».«7»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨7, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨7, ⋯⟩)) = 0«10».«8»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨8, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨8, ⋯⟩)) = 0«10».«9»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨9, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨9, ⋯⟩)) = 0«10».«10»hi:(fun i => i) ⟨10, ⋯⟩ ≠ (fun i => i) ⟨10, ⋯⟩⊢ (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨10, ⋯⟩)) = 0
  any_goals with_unfolding_all rflAll goals completed! 🐙
  all_goals simp at hiAll goals completed! 🐙



set_option backward.isDefEq.respectTransparency false in
lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
    quadBiLin (B i) (∑ k, f k • B k) = f i * quadBiLin (B i) (B i) := byi:Fin 11f:Fin 11 → ℚ⊢ (quadBiLin (B i)) (∑ k, f k • B k) = f i * (quadBiLin (B i)) (B i)
  rw [quadBiLin.map_sum₂,i:Fin 11f:Fin 11 → ℚ⊢ ∑ i_1, (quadBiLin (B i)) (f i_1 • B i_1) = f i * (quadBiLin (B i)) (B i)i:Fin 11f:Fin 11 → ℚ⊢ (quadBiLin (B i)) (f i • B i) = f i * (quadBiLin (B i)) (B i)i:Fin 11f:Fin 11 → ℚ⊢ ∀ (x : Fin 11), x ≠ i → (quadBiLin (B i)) (f x • B x) = 0 Fintype.sum_eq_single ii:Fin 11f:Fin 11 → ℚ⊢ (quadBiLin (B i)) (f i • B i) = f i * (quadBiLin (B i)) (B i)i:Fin 11f:Fin 11 → ℚ⊢ ∀ (x : Fin 11), x ≠ i → (quadBiLin (B i)) (f x • B x) = 0i:Fin 11f:Fin 11 → ℚ⊢ (quadBiLin (B i)) (f i • B i) = f i * (quadBiLin (B i)) (B i)i:Fin 11f:Fin 11 → ℚ⊢ ∀ (x : Fin 11), x ≠ i → (quadBiLin (B i)) (f x • B x) = 0]i:Fin 11f:Fin 11 → ℚ⊢ (quadBiLin (B i)) (f i • B i) = f i * (quadBiLin (B i)) (B i)i:Fin 11f:Fin 11 → ℚ⊢ ∀ (x : Fin 11), x ≠ i → (quadBiLin (B i)) (f x • B x) = 0
  ·i:Fin 11f:Fin 11 → ℚ⊢ (quadBiLin (B i)) (f i • B i) = f i * (quadBiLin (B i)) (B i) rw [quadBiLin.map_smul₂i:Fin 11f:Fin 11 → ℚ⊢ f i * (quadBiLin (B i)) (B i) = f i * (quadBiLin (B i)) (B i)All goals completed! 🐙]All goals completed! 🐙
  ·i:Fin 11f:Fin 11 → ℚ⊢ ∀ (x : Fin 11), x ≠ i → (quadBiLin (B i)) (f x • B x) = 0 intro k hiji:Fin 11f:Fin 11 → ℚk:Fin 11hij:k ≠ i⊢ (quadBiLin (B i)) (f k • B k) = 0
    rw [quadBiLin.map_smul₂,i:Fin 11f:Fin 11 → ℚk:Fin 11hij:k ≠ i⊢ f k * (quadBiLin (B i)) (B k) = 0i:Fin 11f:Fin 11 → ℚk:Fin 11hij:k ≠ i⊢ f k * 0 = 0 Bi_Bj_quad hij.symmi:Fin 11f:Fin 11 → ℚk:Fin 11hij:k ≠ i⊢ f k * 0 = 0i:Fin 11f:Fin 11 → ℚk:Fin 11hij:k ≠ i⊢ f k * 0 = 0]i:Fin 11f:Fin 11 → ℚk:Fin 11hij:k ≠ i⊢ f k * 0 = 0
    exact Rat.mul_zero (f k)All goals completed! 🐙

The coefficients of the quadratic equation in our basis.

@[simp]
def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]

              lemma quadCoeff_eq_bilinear (i : Fin 11) : quadCoeff i = quadBiLin (B i) (B i) := byi:Fin 11⊢ quadCoeff i = (quadBiLin (B i)) (B i)
  fin_cases i«0»⊢ quadCoeff ((fun i => i) ⟨0, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨0, ⋯⟩))) (B ((fun i => i) ⟨0, ⋯⟩))«1»⊢ quadCoeff ((fun i => i) ⟨1, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨1, ⋯⟩))) (B ((fun i => i) ⟨1, ⋯⟩))«2»⊢ quadCoeff ((fun i => i) ⟨2, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨2, ⋯⟩))) (B ((fun i => i) ⟨2, ⋯⟩))«3»⊢ quadCoeff ((fun i => i) ⟨3, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨3, ⋯⟩))) (B ((fun i => i) ⟨3, ⋯⟩))«4»⊢ quadCoeff ((fun i => i) ⟨4, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨4, ⋯⟩))) (B ((fun i => i) ⟨4, ⋯⟩))«5»⊢ quadCoeff ((fun i => i) ⟨5, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨5, ⋯⟩))) (B ((fun i => i) ⟨5, ⋯⟩))«6»⊢ quadCoeff ((fun i => i) ⟨6, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨6, ⋯⟩))) (B ((fun i => i) ⟨6, ⋯⟩))«7»⊢ quadCoeff ((fun i => i) ⟨7, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨7, ⋯⟩))) (B ((fun i => i) ⟨7, ⋯⟩))«8»⊢ quadCoeff ((fun i => i) ⟨8, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨8, ⋯⟩))) (B ((fun i => i) ⟨8, ⋯⟩))«9»⊢ quadCoeff ((fun i => i) ⟨9, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨9, ⋯⟩))) (B ((fun i => i) ⟨9, ⋯⟩))«10»⊢ quadCoeff ((fun i => i) ⟨10, ⋯⟩) = (quadBiLin (B ((fun i => i) ⟨10, ⋯⟩))) (B ((fun i => i) ⟨10, ⋯⟩))
  all_goals with_unfolding_all rflAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma on_accQuad (f : Fin 11 → ℚ) :
    accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * (f i)^2 := byf:Fin 11 → ℚ⊢ accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * f i ^ 2
  change quadBiLin _ _ = _f:Fin 11 → ℚ⊢ (quadBiLin (∑ i, f i • B i)) (∑ i, f i • B i) = ∑ i, quadCoeff i * f i ^ 2
  rw [quadBiLin.map_sum₁f:Fin 11 → ℚ⊢ ∑ i, (quadBiLin (f i • B i)) (∑ i, f i • B i) = ∑ i, quadCoeff i * f i ^ 2f:Fin 11 → ℚ⊢ ∑ i, (quadBiLin (f i • B i)) (∑ i, f i • B i) = ∑ i, quadCoeff i * f i ^ 2]f:Fin 11 → ℚ⊢ ∑ i, (quadBiLin (f i • B i)) (∑ i, f i • B i) = ∑ i, quadCoeff i * f i ^ 2
  refine Fintype.sum_congr _ _ fun i ↦ ?_f:Fin 11 → ℚi:Fin 11⊢ (quadBiLin (f i • B i)) (∑ i, f i • B i) = quadCoeff i * f i ^ 2
  rw [quadBiLin.map_smul₁,f:Fin 11 → ℚi:Fin 11⊢ f i * (quadBiLin (B i)) (∑ i, f i • B i) = quadCoeff i * f i ^ 2f:Fin 11 → ℚi:Fin 11⊢ f i * (f i * (quadBiLin (B i)) (B i)) = (quadBiLin (B i)) (B i) * f i ^ 2 Bi_sum_quad,f:Fin 11 → ℚi:Fin 11⊢ f i * (f i * (quadBiLin (B i)) (B i)) = quadCoeff i * f i ^ 2f:Fin 11 → ℚi:Fin 11⊢ f i * (f i * (quadBiLin (B i)) (B i)) = (quadBiLin (B i)) (B i) * f i ^ 2 quadCoeff_eq_bilinearf:Fin 11 → ℚi:Fin 11⊢ f i * (f i * (quadBiLin (B i)) (B i)) = (quadBiLin (B i)) (B i) * f i ^ 2f:Fin 11 → ℚi:Fin 11⊢ f i * (f i * (quadBiLin (B i)) (B i)) = (quadBiLin (B i)) (B i) * f i ^ 2]f:Fin 11 → ℚi:Fin 11⊢ f i * (f i * (quadBiLin (B i)) (B i)) = (quadBiLin (B i)) (B i) * f i ^ 2
  ringAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i))
    (k : Fin 11) : quadCoeff k * (f k)^2 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)k:Fin 11⊢ quadCoeff k * f k ^ 2 = 0
  obtain ⟨S, hS⟩ := hSf:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B i⊢ quadCoeff k * f k ^ 2 = 0
  have hQ := quadSol S.1f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:accQuad S.val = 0⊢ quadCoeff k * f k ^ 2 = 0
  rw [hS,f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:accQuad (∑ i, f i • B i) = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:(fun i => quadCoeff i * f i ^ 2) = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ fun i => quadCoeff i * f i ^ 2 on_accQuad,f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:(fun i => quadCoeff i * f i ^ 2) = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ fun i => quadCoeff i * f i ^ 2 Fintype.sum_eq_zero_iff_of_nonnegf:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:(fun i => quadCoeff i * f i ^ 2) = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ fun i => quadCoeff i * f i ^ 2f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:(fun i => quadCoeff i * f i ^ 2) = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ fun i => quadCoeff i * f i ^ 2] at hQf:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:(fun i => quadCoeff i * f i ^ 2) = 0⊢ quadCoeff k * f k ^ 2 = 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ fun i => quadCoeff i * f i ^ 2
  ·f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:(fun i => quadCoeff i * f i ^ 2) = 0⊢ quadCoeff k * f k ^ 2 = 0 exact congrFun hQ kAll goals completed! 🐙
  ·f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ fun i => quadCoeff i * f i ^ 2 intro if:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 i ≤ (fun i => quadCoeff i * f i ^ 2) i
    simp only [Pi.zero_apply, quadCoeff]f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i * f i ^ 2
    rw [mul_nonneg_ifff:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i ∧ 0 ≤ f i ^ 2 ∨ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i ≤ 0 ∧ f i ^ 2 ≤ 0f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i ∧ 0 ≤ f i ^ 2 ∨ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i ≤ 0 ∧ f i ^ 2 ≤ 0]f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i ∧ 0 ≤ f i ^ 2 ∨ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] i ≤ 0 ∧ f i ^ 2 ≤ 0
    apply Or.inl (And.intro _ _)f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] if:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0i:Fin 11⊢ 0 ≤ f i ^ 2
    fin_cases i«0»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨0, ⋯⟩)«1»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨1, ⋯⟩)«2»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨2, ⋯⟩)«3»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨3, ⋯⟩)«4»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨4, ⋯⟩)«5»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨5, ⋯⟩)«6»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨6, ⋯⟩)«7»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨7, ⋯⟩)«8»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨8, ⋯⟩)«9»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨9, ⋯⟩)«10»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨10, ⋯⟩) <;>«0»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨0, ⋯⟩)«1»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨1, ⋯⟩)«2»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨2, ⋯⟩)«3»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨3, ⋯⟩)«4»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨4, ⋯⟩)«5»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨5, ⋯⟩)«6»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨6, ⋯⟩)«7»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨7, ⋯⟩)«8»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨8, ⋯⟩)«9»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨9, ⋯⟩)«10»f:Fin 11 → ℚk:Fin 11S:(PlusU1 3).SolshS:S.val = ∑ i, f i • B ihQ:∑ i, quadCoeff i * f i ^ 2 = 0⊢ 0 ≤ ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0] ((fun i => i) ⟨10, ⋯⟩) rflAll goals completed! 🐙
    exact sq_nonneg (f i)All goals completed! 🐙lemma isSolution_f0 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 0 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 0 = 0
  simpa using (isSolution_quadCoeff_f_sq_zero f hS 0)All goals completed! 🐙lemma isSolution_f1 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 1 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 1 = 0
  simpa using (isSolution_quadCoeff_f_sq_zero f hS 1)All goals completed! 🐙lemma isSolution_f2 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 2 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 2 = 0
  simpa using (isSolution_quadCoeff_f_sq_zero f hS 2)All goals completed! 🐙lemma isSolution_f3 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 3 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 3 = 0
  simpa using (isSolution_quadCoeff_f_sq_zero f hS 3)All goals completed! 🐙lemma isSolution_f4 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 4 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 4 = 0
  simpa using (isSolution_quadCoeff_f_sq_zero f hS 4)All goals completed! 🐙

lemma isSolution_f5 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 5 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 5 = 0
  have h := isSolution_quadCoeff_f_sq_zero f hS 5f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 5 * f 5 ^ 2 = 0⊢ f 5 = 0
  rw [mul_eq_zerof:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 5 = 0 ∨ f 5 ^ 2 = 0⊢ f 5 = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 5 = 0 ∨ f 5 ^ 2 = 0⊢ f 5 = 0] at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 5 = 0 ∨ f 5 ^ 2 = 0⊢ f 5 = 0
  change 1 = 0 ∨ _ = _ at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:1 = 0 ∨ f 5 ^ 2 = 0⊢ f 5 = 0
  simpa using hAll goals completed! 🐙

lemma isSolution_f6 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 6 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 6 = 0
  have h := isSolution_quadCoeff_f_sq_zero f hS 6f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 6 * f 6 ^ 2 = 0⊢ f 6 = 0
  rw [mul_eq_zerof:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 6 = 0 ∨ f 6 ^ 2 = 0⊢ f 6 = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 6 = 0 ∨ f 6 ^ 2 = 0⊢ f 6 = 0] at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 6 = 0 ∨ f 6 ^ 2 = 0⊢ f 6 = 0
  change 1 = 0 ∨ _ = _ at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:1 = 0 ∨ f 6 ^ 2 = 0⊢ f 6 = 0
  simpa using hAll goals completed! 🐙

lemma isSolution_f7 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 7 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 7 = 0
  have h := isSolution_quadCoeff_f_sq_zero f hS 7f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 7 * f 7 ^ 2 = 0⊢ f 7 = 0
  rw [mul_eq_zerof:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 7 = 0 ∨ f 7 ^ 2 = 0⊢ f 7 = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 7 = 0 ∨ f 7 ^ 2 = 0⊢ f 7 = 0] at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 7 = 0 ∨ f 7 ^ 2 = 0⊢ f 7 = 0
  change 1 = 0 ∨ _ = _ at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:1 = 0 ∨ f 7 ^ 2 = 0⊢ f 7 = 0
  simpa using hAll goals completed! 🐙

lemma isSolution_f8 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : f 8 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 8 = 0
  have h := isSolution_quadCoeff_f_sq_zero f hS 8f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 8 * f 8 ^ 2 = 0⊢ f 8 = 0
  rw [mul_eq_zerof:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 8 = 0 ∨ f 8 ^ 2 = 0⊢ f 8 = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 8 = 0 ∨ f 8 ^ 2 = 0⊢ f 8 = 0] at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:quadCoeff 8 = 0 ∨ f 8 ^ 2 = 0⊢ f 8 = 0
  change 1 = 0 ∨ _ = _ at hf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)h:1 = 0 ∨ f 8 ^ 2 = 0⊢ f 8 = 0
  simpa using hAll goals completed! 🐙

lemma isSolution_sum_part (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    ∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀ := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ ∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀
  rw [Fin.sum_univ_castSucc,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ ∑ i, f i.castSucc • B i.castSucc + f (Fin.last 10) • B (Fin.last 10) = f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f (Fin.castSucc 0).castSucc.castSucc • B (Fin.castSucc 0).castSucc.castSucc +
                      f (Fin.castSucc 1).castSucc.castSucc • B (Fin.castSucc 1).castSucc.castSucc +
                    f (Fin.castSucc 2).castSucc.castSucc • B (Fin.castSucc 2).castSucc.castSucc +
                  f (Fin.castSucc 3).castSucc.castSucc • B (Fin.castSucc 3).castSucc.castSucc +
                f (Fin.castSucc 4).castSucc.castSucc • B (Fin.castSucc 4).castSucc.castSucc +
              f (Fin.castSucc 5).castSucc.castSucc • B (Fin.castSucc 5).castSucc.castSucc +
            f (Fin.castSucc 6).castSucc.castSucc • B (Fin.castSucc 6).castSucc.castSucc +
          f (Fin.castSucc 7).castSucc.castSucc • B (Fin.castSucc 7).castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀ Fin.sum_univ_castSucc,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ ∑ i, f i.castSucc.castSucc • B i.castSucc.castSucc + f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f (Fin.castSucc 0).castSucc.castSucc • B (Fin.castSucc 0).castSucc.castSucc +
                      f (Fin.castSucc 1).castSucc.castSucc • B (Fin.castSucc 1).castSucc.castSucc +
                    f (Fin.castSucc 2).castSucc.castSucc • B (Fin.castSucc 2).castSucc.castSucc +
                  f (Fin.castSucc 3).castSucc.castSucc • B (Fin.castSucc 3).castSucc.castSucc +
                f (Fin.castSucc 4).castSucc.castSucc • B (Fin.castSucc 4).castSucc.castSucc +
              f (Fin.castSucc 5).castSucc.castSucc • B (Fin.castSucc 5).castSucc.castSucc +
            f (Fin.castSucc 6).castSucc.castSucc • B (Fin.castSucc 6).castSucc.castSucc +
          f (Fin.castSucc 7).castSucc.castSucc • B (Fin.castSucc 7).castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀ Fin.sum_univ_castSucc,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ ∑ i, f i.castSucc.castSucc.castSucc • B i.castSucc.castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f (Fin.castSucc 0).castSucc.castSucc • B (Fin.castSucc 0).castSucc.castSucc +
                      f (Fin.castSucc 1).castSucc.castSucc • B (Fin.castSucc 1).castSucc.castSucc +
                    f (Fin.castSucc 2).castSucc.castSucc • B (Fin.castSucc 2).castSucc.castSucc +
                  f (Fin.castSucc 3).castSucc.castSucc • B (Fin.castSucc 3).castSucc.castSucc +
                f (Fin.castSucc 4).castSucc.castSucc • B (Fin.castSucc 4).castSucc.castSucc +
              f (Fin.castSucc 5).castSucc.castSucc • B (Fin.castSucc 5).castSucc.castSucc +
            f (Fin.castSucc 6).castSucc.castSucc • B (Fin.castSucc 6).castSucc.castSucc +
          f (Fin.castSucc 7).castSucc.castSucc • B (Fin.castSucc 7).castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀ Fin.sum_univ_eightf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f (Fin.castSucc 0).castSucc.castSucc • B (Fin.castSucc 0).castSucc.castSucc +
                      f (Fin.castSucc 1).castSucc.castSucc • B (Fin.castSucc 1).castSucc.castSucc +
                    f (Fin.castSucc 2).castSucc.castSucc • B (Fin.castSucc 2).castSucc.castSucc +
                  f (Fin.castSucc 3).castSucc.castSucc • B (Fin.castSucc 3).castSucc.castSucc +
                f (Fin.castSucc 4).castSucc.castSucc • B (Fin.castSucc 4).castSucc.castSucc +
              f (Fin.castSucc 5).castSucc.castSucc • B (Fin.castSucc 5).castSucc.castSucc +
            f (Fin.castSucc 6).castSucc.castSucc • B (Fin.castSucc 6).castSucc.castSucc +
          f (Fin.castSucc 7).castSucc.castSucc • B (Fin.castSucc 7).castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f (Fin.castSucc 0).castSucc.castSucc • B (Fin.castSucc 0).castSucc.castSucc +
                      f (Fin.castSucc 1).castSucc.castSucc • B (Fin.castSucc 1).castSucc.castSucc +
                    f (Fin.castSucc 2).castSucc.castSucc • B (Fin.castSucc 2).castSucc.castSucc +
                  f (Fin.castSucc 3).castSucc.castSucc • B (Fin.castSucc 3).castSucc.castSucc +
                f (Fin.castSucc 4).castSucc.castSucc • B (Fin.castSucc 4).castSucc.castSucc +
              f (Fin.castSucc 5).castSucc.castSucc • B (Fin.castSucc 5).castSucc.castSucc +
            f (Fin.castSucc 6).castSucc.castSucc • B (Fin.castSucc 6).castSucc.castSucc +
          f (Fin.castSucc 7).castSucc.castSucc • B (Fin.castSucc 7).castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀]f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f (Fin.castSucc 0).castSucc.castSucc • B (Fin.castSucc 0).castSucc.castSucc +
                      f (Fin.castSucc 1).castSucc.castSucc • B (Fin.castSucc 1).castSucc.castSucc +
                    f (Fin.castSucc 2).castSucc.castSucc • B (Fin.castSucc 2).castSucc.castSucc +
                  f (Fin.castSucc 3).castSucc.castSucc • B (Fin.castSucc 3).castSucc.castSucc +
                f (Fin.castSucc 4).castSucc.castSucc • B (Fin.castSucc 4).castSucc.castSucc +
              f (Fin.castSucc 5).castSucc.castSucc • B (Fin.castSucc 5).castSucc.castSucc +
            f (Fin.castSucc 6).castSucc.castSucc • B (Fin.castSucc 6).castSucc.castSucc +
          f (Fin.castSucc 7).castSucc.castSucc • B (Fin.castSucc 7).castSucc.castSucc +
        f (Fin.last 8).castSucc.castSucc • B (Fin.last 8).castSucc.castSucc +
      f (Fin.last 9).castSucc • B (Fin.last 9).castSucc +
    f (Fin.last 10) • B (Fin.last 10) =
  f 9 • B₉ + f 10 • B₁₀
  change f 0 • B 0 + f 1 • B 1 + f 2 • B 2 + f 3 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 +
  f 7 • B 7 + f 8 • B 8 + f 9 • B 9 + f 10 • B 10 = f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 0 • B 0 + f 1 • B 1 + f 2 • B 2 + f 3 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀
  rw [isSolution_f0 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + f 1 • B 1 + f 2 • B 2 + f 3 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀ isSolution_f1 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + f 2 • B 2 + f 3 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀ isSolution_f2 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + f 3 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀ isSolution_f3 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀
    isSolution_f4 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + f 5 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀ isSolution_f5 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + f 6 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 +
    f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀
    isSolution_f6 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + f 7 • B 7 + f 8 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀ isSolution_f7 f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + f 8 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀ isSolution_f8 f hSf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀]f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B 0 + 0 • B 1 + 0 • B 2 + 0 • B 3 + 0 • B 4 + 0 • B 5 + 0 • B 6 + 0 • B 7 + 0 • B 8 + f 9 • B 9 + f 10 • B 10 =
  f 9 • B₉ + f 10 • B₁₀
  simp only [Fin.isValue, zero_smul, add_zero, zero_add]f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 9 • B 9 + f 10 • B 10 = f 9 • B₉ + f 10 • B₁₀
  rflAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    f 10 = - 3 * f 9 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 10 = -3 * f 9
  have hx := isSolution_sum_part f hSf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)hx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀⊢ f 10 = -3 * f 9
  obtain ⟨S, hS'⟩ := hSf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B i⊢ f 10 = -3 * f 9
  have hg := gravSol S.toLinSolsf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:accGrav S.val = 0⊢ f 10 = -3 * f 9
  rw [hS',f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:accGrav (∑ i, f i • B i) = 0⊢ f 10 = -3 * f 9f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9 hx,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:accGrav (f 9 • B₉ + f 10 • B₁₀) = 0⊢ f 10 = -3 * f 9f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9 accGrav.map_add,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:accGrav (f 9 • B₉) + accGrav (f 10 • B₁₀) = 0⊢ f 10 = -3 * f 9f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9 accGrav.map_smul,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • accGrav B₉ + accGrav (f 10 • B₁₀) = 0⊢ f 10 = -3 * f 9f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9 accGrav.map_smul,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • accGrav B₉ + f 10 • accGrav B₁₀ = 0⊢ f 10 = -3 * f 9f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9
    show accGrav B₉ = 3 by with_unfolding_all rflAll goals completed! 🐙f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9,
    show accGrav B₁₀ = 1 by with_unfolding_all rflAll goals completed! 🐙f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9] at hgf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 • 3 + f 10 • 1 = 0⊢ f 10 = -3 * f 9
  simp only [Fin.isValue, smul_eq_mul, mul_one] at hgf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihg:f 9 * 3 + f 10 = 0⊢ f 10 = -3 * f 9
  linear_combination hgAll goals completed! 🐙

lemma isSolution_sum_part' (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    ∑ i, f i • B i = f 9 • B₉ + (- 3 * f 9) • B₁₀ := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ ∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀
  rw [isSolution_sum_part f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 9 • B₉ + f 10 • B₁₀ = f 9 • B₉ + (-3 * f 9) • B₁₀All goals completed! 🐙 isSolution_grav f hSf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 9 • B₉ + (-3 * f 9) • B₁₀ = f 9 • B₉ + (-3 * f 9) • B₁₀All goals completed! 🐙]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    f 9 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 9 = 0
  have hx := isSolution_sum_part' f hSf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)hx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀⊢ f 9 = 0
  obtain ⟨S, hS'⟩ := hSf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B i⊢ f 9 = 0
  have hc := cubeSol Sf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:accCube S.val = 0⊢ f 9 = 0
  rw [hS',f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:accCube (∑ i, f i • B i) = 0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:accCube (f 9 • B₉ + (-3 * f 9) • B₁₀) = 0⊢ f 9 = 0 hxf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:accCube (f 9 • B₉ + (-3 * f 9) • B₁₀) = 0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:accCube (f 9 • B₉ + (-3 * f 9) • B₁₀) = 0⊢ f 9 = 0] at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:accCube (f 9 • B₉ + (-3 * f 9) • B₁₀) = 0⊢ f 9 = 0
  change cubeTriLin.toCubic _ = _ at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:cubeTriLin.toCubic (f 9 • B₉ + (-3 * f 9) • B₁₀) = 0⊢ f 9 = 0
  rw [cubeTriLin.toCubic_addf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:cubeTriLin.toCubic (f 9 • B₉) + cubeTriLin.toCubic ((-3 * f 9) • B₁₀) +
      3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:cubeTriLin.toCubic (f 9 • B₉) + cubeTriLin.toCubic ((-3 * f 9) • B₁₀) +
      3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0] at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:cubeTriLin.toCubic (f 9 • B₉) + cubeTriLin.toCubic ((-3 * f 9) • B₁₀) +
      3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0
  erw [accCube.map_smulf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + cubeTriLin.toCubic ((-3 * f 9) • B₁₀) +
      3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0]f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + cubeTriLin.toCubic ((-3 * f 9) • B₁₀) +
      3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0 at hc
  erw [accCube.map_smul (- 3 * f 9) B₁₀f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0]f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * ((cubeTriLin (f 9 • B₉)) (f 9 • B₉)) ((-3 * f 9) • B₁₀) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0 at hc
  rw [cubeTriLin.map_smul₁,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * ((cubeTriLin B₉) (f 9 • B₉)) ((-3 * f 9) • B₁₀)) +
    3 * ((cubeTriLin ((-3 * f 9) • B₁₀)) ((-3 * f 9) • B₁₀)) (f 9 • B₉) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0 cubeTriLin.map_smul₁,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * ((cubeTriLin B₉) (f 9 • B₉)) ((-3 * f 9) • B₁₀)) +
    3 * (-3 * f 9 * ((cubeTriLin B₁₀) ((-3 * f 9) • B₁₀)) (f 9 • B₉)) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0 cubeTriLin.map_smul₂,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * ((cubeTriLin B₉) B₉) ((-3 * f 9) • B₁₀))) +
    3 * (-3 * f 9 * ((cubeTriLin B₁₀) ((-3 * f 9) • B₁₀)) (f 9 • B₉)) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0 cubeTriLin.map_smul₂,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * ((cubeTriLin B₉) B₉) ((-3 * f 9) • B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * ((cubeTriLin B₁₀) B₁₀) (f 9 • B₉))) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0
    cubeTriLin.map_smul₃,f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * ((cubeTriLin B₁₀) B₁₀) (f 9 • B₉))) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0 cubeTriLin.map_smul₃f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0] at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * accCube B₉ + (-3 * f 9) ^ 3 * accCube B₁₀ + 3 * (f 9 * (f 9 * (-3 * f 9 * ((cubeTriLin B₉) B₉) B₁₀))) +
    3 * (-3 * f 9 * (-3 * f 9 * (f 9 * ((cubeTriLin B₁₀) B₁₀) B₉))) =
  0⊢ f 9 = 0
  rw [show accCube B₉ = 9 by with_unfolding_all rflAll goals completed! 🐙f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-3 * f 9) ^ 3 * 1 + 3 * (f 9 * (f 9 * (-3 * f 9 * 0))) + 3 * (-3 * f 9 * (-3 * f 9 * (f 9 * 0))) = 0⊢ f 9 = 0,
    show accCube B₁₀ = 1 by with_unfolding_all rflAll goals completed! 🐙f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-3 * f 9) ^ 3 * 1 + 3 * (f 9 * (f 9 * (-3 * f 9 * 0))) + 3 * (-3 * f 9 * (-3 * f 9 * (f 9 * 0))) = 0⊢ f 9 = 0,
    show cubeTriLin B₉ B₉ B₁₀ = 0 by with_unfolding_all rflAll goals completed! 🐙f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-3 * f 9) ^ 3 * 1 + 3 * (f 9 * (f 9 * (-3 * f 9 * 0))) + 3 * (-3 * f 9 * (-3 * f 9 * (f 9 * 0))) = 0⊢ f 9 = 0,
    show cubeTriLin B₁₀ B₁₀ B₉ = 0 by with_unfolding_all rflAll goals completed! 🐙f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-3 * f 9) ^ 3 * 1 + 3 * (f 9 * (f 9 * (-3 * f 9 * 0))) + 3 * (-3 * f 9 * (-3 * f 9 * (f 9 * 0))) = 0⊢ f 9 = 0] at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-3 * f 9) ^ 3 * 1 + 3 * (f 9 * (f 9 * (-3 * f 9 * 0))) + 3 * (-3 * f 9 * (-3 * f 9 * (f 9 * 0))) = 0⊢ f 9 = 0
  simp only [Fin.isValue, neg_mul, mul_one, mul_zero, add_zero] at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = 0⊢ f 9 = 0
  have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by ringf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = 0h1:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = -18 * f 9 ^ 3⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = 0h1:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = -18 * f 9 ^ 3⊢ f 9 = 0
  rw [h1f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:-18 * f 9 ^ 3 = 0h1:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = -18 * f 9 ^ 3⊢ f 9 = 0f:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:-18 * f 9 ^ 3 = 0h1:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = -18 * f 9 ^ 3⊢ f 9 = 0] at hcf:Fin 11 → ℚhx:∑ i, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀S:(PlusU1 3).SolshS':S.val = ∑ i, f i • B ihc:-18 * f 9 ^ 3 = 0h1:f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = -18 * f 9 ^ 3⊢ f 9 = 0
  simpa using hcAll goals completed! 🐙

lemma isSolution_f10 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    f 10 = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 10 = 0
  rw [isSolution_grav f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ -3 * f 9 = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ -3 * 0 = 0 isSolution_f9 f hSf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ -3 * 0 = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ -3 * 0 = 0]f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ -3 * 0 = 0
  with_unfolding_all rflAll goals completed! 🐙lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i))
    (k : Fin 11) : f k = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)k:Fin 11⊢ f k = 0
  fin_cases k«0»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨0, ⋯⟩) = 0«1»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨1, ⋯⟩) = 0«2»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨2, ⋯⟩) = 0«3»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨3, ⋯⟩) = 0«4»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨4, ⋯⟩) = 0«5»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨5, ⋯⟩) = 0«6»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨6, ⋯⟩) = 0«7»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨7, ⋯⟩) = 0«8»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨8, ⋯⟩) = 0«9»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨9, ⋯⟩) = 0«10»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨10, ⋯⟩) = 0
  ·«0»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨0, ⋯⟩) = 0 exact isSolution_f0 f hSAll goals completed! 🐙
  ·«1»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨1, ⋯⟩) = 0 exact isSolution_f1 f hSAll goals completed! 🐙
  ·«2»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨2, ⋯⟩) = 0 exact isSolution_f2 f hSAll goals completed! 🐙
  ·«3»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨3, ⋯⟩) = 0 exact isSolution_f3 f hSAll goals completed! 🐙
  ·«4»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨4, ⋯⟩) = 0 exact isSolution_f4 f hSAll goals completed! 🐙
  ·«5»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨5, ⋯⟩) = 0 exact isSolution_f5 f hSAll goals completed! 🐙
  ·«6»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨6, ⋯⟩) = 0 exact isSolution_f6 f hSAll goals completed! 🐙
  ·«7»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨7, ⋯⟩) = 0 exact isSolution_f7 f hSAll goals completed! 🐙
  ·«8»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨8, ⋯⟩) = 0 exact isSolution_f8 f hSAll goals completed! 🐙
  ·«9»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨9, ⋯⟩) = 0 exact isSolution_f9 f hSAll goals completed! 🐙
  ·«10»f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f ((fun i => i) ⟨10, ⋯⟩) = 0 exact isSolution_f10 f hSAll goals completed! 🐙

lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    ∑ i, f i • B i = 0 := byf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ ∑ i, f i • B i = 0
  rw [isSolution_sum_part f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 9 • B₉ + f 10 • B₁₀ = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B₉ + (-3 * 0) • B₁₀ = 0 isSolution_grav f hS,f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ f 9 • B₉ + (-3 * f 9) • B₁₀ = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B₉ + (-3 * 0) • B₁₀ = 0 isSolution_f9 f hSf:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B₉ + (-3 * 0) • B₁₀ = 0f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B₉ + (-3 * 0) • B₁₀ = 0]f:Fin 11 → ℚhS:(PlusU1 3).IsSolution (∑ i, f i • B i)⊢ 0 • B₉ + (-3 * 0) • B₁₀ = 0
  simpAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
theorem basis_linear_independent : LinearIndependent ℚ B :=
  Fintype.linearIndependent_iff.mpr fun f h ↦ isSolution_f_zero f
    ⟨chargeToAF 0 (byf:Fin 11 → ℚh:∑ i, f i • B i = 0⊢ accGrav 0 = 0 with_unfolding_all rflAll goals completed! 🐙) (byf:Fin 11 → ℚh:∑ i, f i • B i = 0⊢ accSU2 0 = 0 with_unfolding_all rflAll goals completed! 🐙)
      (byf:Fin 11 → ℚh:∑ i, f i • B i = 0⊢ accSU3 0 = 0 with_unfolding_all rflAll goals completed! 🐙) (byf:Fin 11 → ℚh:∑ i, f i • B i = 0⊢ accYY 0 = 0 with_unfolding_all rflAll goals completed! 🐙) (byf:Fin 11 → ℚh:∑ i, f i • B i = 0⊢ accQuad 0 = 0 with_unfolding_all rflAll goals completed! 🐙)
      (byf:Fin 11 → ℚh:∑ i, f i • B i = 0⊢ accCube 0 = 0 with_unfolding_all rflAll goals completed! 🐙), id (Eq.symm h)⟩theorem eleven_dim_plane_of_no_sols_exists : ∃ (B : Fin 11 → (PlusU1 3).Charges),
    LinearIndependent ℚ B ∧
    ∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0 :=
  ⟨ElevenPlane.B, ElevenPlane.basis_linear_independent, ElevenPlane.isSolution_only_if_zero⟩