Physlib.Particles.StandardModel.Fermions.UpSinglet

Imports

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

public import Physlib.Particles.StandardModel.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.Basic

Up-type singlets

In this module we define the type corresponding to the target vector space of an up-type singlet quark field in the Standard Model.

On this type we define a representation of the Lorentz group, and a representation of the Standard Model gauge group.

@[expose] public section

The vector space of an up-type singlet quark field in the Standard Model. These live in the (3, 1)_{4} representation of the gauge group.

The underlying value of the up-type quark field in the tensor product space.

@[ext]
structure UpSinglet where

val : Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3)

Equivalence with the underlying tensor product space

The linear equivalence between UpSinglet and its underlying tensor product space.

def valEquiv : UpSinglet ≃ Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3) where
  toFun := val
  invFun := fun m => ⟨m⟩

The structure of a module

The AddCommGroup and module instances are inherited from the underlying tensor product space.

instance : AddCommGroup UpSinglet := Equiv.addCommGroup valEquivinstance : Module ℂ UpSinglet := Equiv.module ℂ valEquiv

The linear equivalence between UpSinglet and its underlying tensor product space.

def valLinEquiv : UpSinglet ≃ₗ[ℂ]
    Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3) where
  toFun := val
  invFun := fun m => ⟨m⟩
  map_add' := by⊢ ∀ (x y : UpSinglet), (x + y).val = x.val + y.val introsx✝:UpSinglety✝:UpSinglet⊢ (x✝ + y✝).val = x✝.val + y✝.val; rflAll goals completed! 🐙
  map_smul' := by⊢ ∀ (m : ℂ) (x : UpSinglet), (m • x).val = (RingHom.id ℂ) m • x.val introsm✝:ℂx✝:UpSinglet⊢ (m✝ • x✝).val = (RingHom.id ℂ) m✝ • x✝.val; rflAll goals completed! 🐙

              @[simp]
lemma valLinEquiv_apply (q : UpSinglet) : valLinEquiv q = q.val := rfllemma valLinEquiv_symm_apply (m : Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3)) :
    valLinEquiv.symm m = ⟨m⟩ := rfl@[simp]
lemma val_add (q1 q2 : UpSinglet) : (q1 + q2).val = q1.val + q2.val := rfl@[simp]
lemma val_smul (r : ℂ) (q : UpSinglet) : (r • q).val = r • q.val := rfl

Lorentz group representation

The representation of the Standard Model gauge group

              lemma repGaugeGroupI_tmul (g : GaugeGroupI) (ψ : Fermion.RightHandedWeyl)
    (v : EuclideanSpace ℂ (Fin 3)) :
    repGaugeGroupI g ⟨ψ ⊗ₜ v⟩ = ⟨g.toU1 ^ 4 • ψ ⊗ₜ (g.toSU3.1.toEuclideanLin v)⟩ := rfl

lemma mem_repGaugeGroupI_ker_iff_eq {g : GaugeGroupI} :
    g ∈ repGaugeGroupI.ker ↔ ∃ a : ℂ, g.toSU3.1 = a • 1 ∧  a * g.toU1.1 ^ 4 = 1 := byg:GaugeGroupI⊢ g ∈ MonoidHom.ker repGaugeGroupI ↔ ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
  rw [MonoidHom.mem_ker,g:GaugeGroupI⊢ repGaugeGroupI g = 1 ↔ ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1g:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) ↔
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1 ← MonoidHom.map_one repGaugeGroupI,g:GaugeGroupI⊢ repGaugeGroupI g = repGaugeGroupI 1 ↔ ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1g:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) ↔
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1 repGaugeGroupI_eq_iff_mul_eqg:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) ↔
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1g:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) ↔
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1]g:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) ↔
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
  constructormpg:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) →
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1mprg:GaugeGroupI⊢ (∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1) →
  ∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i; swapmprg:GaugeGroupI⊢ (∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1) →
  ∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' impg:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) →
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
  ·mprg:GaugeGroupI⊢ (∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1) →
  ∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i rintro ⟨a, h1, h2⟩ i i'mprg:GaugeGroupIa:ℂh1:↑(GaugeGroupI.toSU3 g) = a • 1h2:a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1i:Fin 3i':Fin 3⊢ ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i
    simp only [Matrix.smul_apply, smul_eq_mul, h1, map_one, OneMemClass.coe_one]mprg:GaugeGroupIa:ℂh1:↑(GaugeGroupI.toSU3 g) = a • 1h2:a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1i:Fin 3i':Fin 3⊢ ↑(GaugeGroupI.toU1 g) ^ 4 * (a * 1 i' i) = 1 ^ 4 * 1 i' i
    linear_combination h2 * (1 : Matrix _ _ ℂ) i' iAll goals completed! 🐙
  ·mpg:GaugeGroupI⊢ (∀ (i i' : Fin 3),
    ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i) →
  ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1 intro hmpg:GaugeGroupIh:∀ (i i' : Fin 3),
  ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i⊢ ∃ a, ↑(GaugeGroupI.toSU3 g) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
    use g.toSU3.1 0 0hg:GaugeGroupIh:∀ (i i' : Fin 3),
  ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) i' i = ↑(GaugeGroupI.toU1 1) ^ 4 * ↑(GaugeGroupI.toSU3 1) i' i⊢ ↑(GaugeGroupI.toSU3 g) = ↑(GaugeGroupI.toSU3 g) 0 0 • 1 ∧ ↑(GaugeGroupI.toSU3 g) 0 0 * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
    simp only [map_one, OneMemClass.coe_one, Fin.forall_fin_succ, Fin.isValue,
      Fin.succ_zero_eq_one, IsEmpty.forall_iff, and_true, one_apply_eq, mul_one, ne_eq, one_ne_zero,
      not_false_eq_true, one_apply_ne, mul_zero, mul_eq_zero, zero_ne_one, Fin.succ_one_eq_two,
      Fin.reduceEq] at hhg:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) = ↑(GaugeGroupI.toSU3 g) 0 0 • 1 ∧ ↑(GaugeGroupI.toSU3 g) 0 0 * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
    refine ⟨?_, ?_⟩h.refine_1g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) = ↑(GaugeGroupI.toSU3 g) 0 0 • 1h.refine_2g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 0 0 * ↑(GaugeGroupI.toU1 g) ^ 4 = 1
    ·h.refine_1g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) = ↑(GaugeGroupI.toSU3 g) 0 0 • 1 ext i jh.refine_1g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4i:Fin 3j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) i j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) i j
      fin_cases ih.refine_1.«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨0, ⋯⟩) j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨0, ⋯⟩) jh.refine_1.«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨1, ⋯⟩) j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨1, ⋯⟩) jh.refine_1.«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) j <;>h.refine_1.«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨0, ⋯⟩) j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨0, ⋯⟩) jh.refine_1.«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨1, ⋯⟩) j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨1, ⋯⟩) jh.refine_1.«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4j:Fin 3⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) j = (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) j fin_cases jh.refine_1.«2».«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)h.refine_1.«2».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)h.refine_1.«2».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) <;>h.refine_1.«0».«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)h.refine_1.«0».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)h.refine_1.«0».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)h.refine_1.«1».«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)h.refine_1.«1».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)h.refine_1.«1».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)h.refine_1.«2».«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)h.refine_1.«2».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)h.refine_1.«2».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑(GaugeGroupI.toSU3 g) 0 0 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) simph.refine_1.«2».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 2 2 = ↑(GaugeGroupI.toSU3 g) 0 0 <;>h.refine_1.«0».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 0 1 = 0h.refine_1.«0».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 0 2 = 0h.refine_1.«1».«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 1 0 = 0h.refine_1.«1».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 1 1 = ↑(GaugeGroupI.toSU3 g) 0 0h.refine_1.«1».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 1 2 = 0h.refine_1.«2».«0»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 2 0 = 0h.refine_1.«2».«1»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 2 1 = 0h.refine_1.«2».«2»g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 2 2 = ↑(GaugeGroupI.toSU3 g) 0 0 grindAll goals completed! 🐙
    ·h.refine_2g:GaugeGroupIh:(↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 0 0 = 1 ^ 4 ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 0 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 0 = 0)) ∧
  ((↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 1 = 0) ∧
      ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 1 1 = 1 ^ 4 ∧
        (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 2 1 = 0)) ∧
    (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 0 2 = 0) ∧
      (↑(GaugeGroupI.toU1 g) ^ 4 = 0 ∨ ↑(GaugeGroupI.toSU3 g) 1 2 = 0) ∧
        ↑(GaugeGroupI.toU1 g) ^ 4 * ↑(GaugeGroupI.toSU3 g) 2 2 = 1 ^ 4⊢ ↑(GaugeGroupI.toSU3 g) 0 0 * ↑(GaugeGroupI.toU1 g) ^ 4 = 1 grindAll goals completed! 🐙lemma gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI :
    GaugeGroupQuot.subgroup .ℤ₆ ≤ repGaugeGroupI.ker := by⊢ GaugeGroupQuot.ℤ₆.subgroup ≤ MonoidHom.ker repGaugeGroupI
  simp only [GaugeGroupQuot.subgroup, gaugeGroupℤ₆SubGroup, SetLike.le_def, MonoidHom.mem_range,
    gaugeGroupℤ₆Hom_apply, Subtype.exists, mem_repGaugeGroupI_ker_iff_eq, forall_exists_index]⊢ ∀ ⦃x : GaugeGroupI⦄ (x_1 : ℂˣ) (x_2 : x_1 ∈ rootsOfUnity 6 ℂ),
  gaugeGroupℤ₆OfRoot ⟨x_1, x_2⟩ = x → ∃ a, ↑(GaugeGroupI.toSU3 x) = a • 1 ∧ a * ↑(GaugeGroupI.toU1 x) ^ 4 = 1
  rintro g x hx ⟨rfl⟩x:ℂˣhx:x ∈ rootsOfUnity 6 ℂ⊢ ∃ a,
  ↑(GaugeGroupI.toSU3 (gaugeGroupℤ₆OfRoot ⟨x, hx⟩)) = a • 1 ∧
    a * ↑(GaugeGroupI.toU1 (gaugeGroupℤ₆OfRoot ⟨x, hx⟩)) ^ 4 = 1
  use  (x ^ 2)hx:ℂˣhx:x ∈ rootsOfUnity 6 ℂ⊢ ↑(GaugeGroupI.toSU3 (gaugeGroupℤ₆OfRoot ⟨x, hx⟩)) = ↑x ^ 2 • 1 ∧
  ↑x ^ 2 * ↑(GaugeGroupI.toU1 (gaugeGroupℤ₆OfRoot ⟨x, hx⟩)) ^ 4 = 1
  simp only [gaugeGroupℤ₆OfRoot_toSU3, gaugeGroupℤ₆SU3OfRoot_eq_mul_id, gaugeGroupℤ₆OfRoot_toU1,
    gaugeGroupℤ₆UnitaryOfRoot_coe, true_and]hx:ℂˣhx:x ∈ rootsOfUnity 6 ℂ⊢ ↑x ^ 2 * ↑x ^ 4 = 1
  field_simphx:ℂˣhx:x ∈ rootsOfUnity 6 ℂ⊢ ↑x ^ 6 = 1
  exact (mem_rootsOfUnity' 6 x).mp hxAll goals completed! 🐙lemma gaugeGroup_subgroup_le_ker_repGaugeGroupI (Q : GaugeGroupQuot) :
    Q.subgroup ≤ repGaugeGroupI.ker := Q.subgroup_le_subgroup_ℤ₆.trans
  gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI