Physlib.Relativity.Tensors.ComplexTensor.OfRat

Imports
                /-
Copyright (c) 2025 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.Relativity.Tensors.ComplexTensor.Basic
public import Physlib.Mathematics.RatComplexNum
public import Physlib.Relativity.Tensors.Dual

              
                Basis for tensors in a tensor species
              

              @[expose] public section@[simp]
lemma ofRat_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.Color}
    (f : (ComponentIdx c) → RatComplexNum)
    (b :(ComponentIdx c)) :
  (Tensor.basis c).repr (ofRat f) b = toComplexNum (f b) := byn:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumb:ComponentIdx c⊢ ((Tensor.basis c).repr (ofRat f)) b = toComplexNum (f b)
  simp [ofRat]All goals completed! 🐙

lemma basis_eq_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.Color}
    (b : (ComponentIdx c)) :
    Tensor.basis c b
    = ofRat (fun b' => if b = b' then ⟨1, 0⟩ else ⟨0, 0⟩) := byn:ℕc:Fin n → Colorb:ComponentIdx c⊢ (Tensor.basis c) b = ofRat fun b' => if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }
  apply (Tensor.basis c).repr.injectiven:ℕc:Fin n → Colorb:ComponentIdx c⊢ (Tensor.basis c).repr ((Tensor.basis c) b) =
  (Tensor.basis c).repr (ofRat fun b' => if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })
  simp only [Basis.repr_self]n:ℕc:Fin n → Colorb:ComponentIdx c⊢ Finsupp.single b 1 =
  (Tensor.basis c).repr (ofRat fun b' => if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })
  ext b'n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (Finsupp.single b 1) b' =
  ((Tensor.basis c).repr (ofRat fun b' => if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })) b'
  simp only [ofRat_basis_repr_apply]n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (Finsupp.single b 1) b' = toComplexNum (if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })
  rw [Finsupp.single_apply,n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) = toComplexNum (if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) =
  { toFun := fun x => ↑x.fst + ↑x.snd * Complex.I, map_one' := toComplexNum._proof_1, map_mul' := ⋯,
      map_zero' := toComplexNum._proof_3, map_add' := ⋯ }
    (if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) toComplexNumn:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) =
  { toFun := fun x => ↑x.fst + ↑x.snd * Complex.I, map_one' := toComplexNum._proof_1, map_mul' := ⋯,
      map_zero' := toComplexNum._proof_3, map_add' := ⋯ }
    (if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) =
  { toFun := fun x => ↑x.fst + ↑x.snd * Complex.I, map_one' := toComplexNum._proof_1, map_mul' := ⋯,
      map_zero' := toComplexNum._proof_3, map_add' := ⋯ }
    (if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })]n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) =
  { toFun := fun x => ↑x.fst + ↑x.snd * Complex.I, map_one' := toComplexNum._proof_1, map_mul' := ⋯,
      map_zero' := toComplexNum._proof_3, map_add' := ⋯ }
    (if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })
  simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]n:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) =
  ↑(if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }).fst +
    ↑(if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }).snd * Complex.I
  splitisTruen:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx ch✝:b = b'⊢ 1 = ↑{ fst := 1, snd := 0 }.fst + ↑{ fst := 1, snd := 0 }.snd * Complex.IisFalsen:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx ch✝:¬b = b'⊢ 0 = ↑{ fst := 0, snd := 0 }.fst + ↑{ fst := 0, snd := 0 }.snd * Complex.I
  simp only [Rat.cast_one, Rat.cast_zero, zero_mul, add_zero]isFalsen:ℕc:Fin n → Colorb:ComponentIdx cb':ComponentIdx ch✝:¬b = b'⊢ 0 = ↑{ fst := 0, snd := 0 }.fst + ↑{ fst := 0, snd := 0 }.snd * Complex.I
  simpAll goals completed! 🐙

lemma contr_basis_ratComplexNum {c : complexLorentzTensor.Color}
    (i : Fin (complexLorentzTensor.repDim c))
    (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
      ((complexLorentzTensor.contr c)
      (complexLorentzTensor.basis c i ⊗ₜ
      complexLorentzTensor.basis (complexLorentzTensor.τ c) j))
      = toComplexNum (if i.val = j.val then 1 else 0) := byc:Colori:Fin (repDim c)j:Fin (repDim (complexLorentzTensor.τ c))⊢ (complexLorentzTensor.contr c) ((basis c) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ c)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
  match c with
  | Color.upL =>c:Colori:Fin (repDim Color.upL)j:Fin (repDim (complexLorentzTensor.τ Color.upL))⊢ (complexLorentzTensor.contr Color.upL) ((basis Color.upL) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ Color.upL)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    change Fermion.leftDualContraction
      (Fermion.LeftHandedWeyl.basis i ⊗ₜ Fermion.DualLeftHandedWeyl.basis j) = _c:Colori:Fin (repDim Color.upL)j:Fin (repDim (complexLorentzTensor.τ Color.upL))⊢ Fermion.leftDualContraction (Fermion.LeftHandedWeyl.basis i ⊗ₜ[ℂ] Fermion.DualLeftHandedWeyl.basis j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    rw [Fermion.leftDualContraction_basisc:Colori:Fin (repDim Color.upL)j:Fin (repDim (complexLorentzTensor.τ Color.upL))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)c:Colori:Fin (repDim Color.upL)j:Fin (repDim (complexLorentzTensor.τ Color.upL))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)]c:Colori:Fin (repDim Color.upL)j:Fin (repDim (complexLorentzTensor.τ Color.upL))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)
    simpAll goals completed! 🐙
  | Color.downL =>c:Colori:Fin (repDim Color.downL)j:Fin (repDim (complexLorentzTensor.τ Color.downL))⊢ (complexLorentzTensor.contr Color.downL) ((basis Color.downL) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ Color.downL)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    change Fermion.dualLeftContraction
      (Fermion.DualLeftHandedWeyl.basis i ⊗ₜ Fermion.LeftHandedWeyl.basis j) = _c:Colori:Fin (repDim Color.downL)j:Fin (repDim (complexLorentzTensor.τ Color.downL))⊢ Fermion.dualLeftContraction (Fermion.DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] Fermion.LeftHandedWeyl.basis j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    rw [Fermion.dualLeftContraction_basisc:Colori:Fin (repDim Color.downL)j:Fin (repDim (complexLorentzTensor.τ Color.downL))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)c:Colori:Fin (repDim Color.downL)j:Fin (repDim (complexLorentzTensor.τ Color.downL))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)]c:Colori:Fin (repDim Color.downL)j:Fin (repDim (complexLorentzTensor.τ Color.downL))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)
    simpAll goals completed! 🐙
  | Color.upR =>c:Colori:Fin (repDim Color.upR)j:Fin (repDim (complexLorentzTensor.τ Color.upR))⊢ (complexLorentzTensor.contr Color.upR) ((basis Color.upR) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ Color.upR)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    change Fermion.rightDualContraction
      (Fermion.RightHandedWeyl.basis i ⊗ₜ Fermion.DualRightHandedWeyl.basis j) = _c:Colori:Fin (repDim Color.upR)j:Fin (repDim (complexLorentzTensor.τ Color.upR))⊢ Fermion.rightDualContraction (Fermion.RightHandedWeyl.basis i ⊗ₜ[ℂ] Fermion.DualRightHandedWeyl.basis j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    rw [Fermion.rightDualContraction_basisc:Colori:Fin (repDim Color.upR)j:Fin (repDim (complexLorentzTensor.τ Color.upR))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)c:Colori:Fin (repDim Color.upR)j:Fin (repDim (complexLorentzTensor.τ Color.upR))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)]c:Colori:Fin (repDim Color.upR)j:Fin (repDim (complexLorentzTensor.τ Color.upR))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)
    simpAll goals completed! 🐙
  | Color.downR =>c:Colori:Fin (repDim Color.downR)j:Fin (repDim (complexLorentzTensor.τ Color.downR))⊢ (complexLorentzTensor.contr Color.downR) ((basis Color.downR) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ Color.downR)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    change Fermion.rightDualContraction
      (Fermion.RightHandedWeyl.basis i ⊗ₜ Fermion.DualRightHandedWeyl.basis j) = _c:Colori:Fin (repDim Color.downR)j:Fin (repDim (complexLorentzTensor.τ Color.downR))⊢ Fermion.rightDualContraction (Fermion.RightHandedWeyl.basis i ⊗ₜ[ℂ] Fermion.DualRightHandedWeyl.basis j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    rw [Fermion.rightDualContraction_basisc:Colori:Fin (repDim Color.downR)j:Fin (repDim (complexLorentzTensor.τ Color.downR))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)c:Colori:Fin (repDim Color.downR)j:Fin (repDim (complexLorentzTensor.τ Color.downR))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)]c:Colori:Fin (repDim Color.downR)j:Fin (repDim (complexLorentzTensor.τ Color.downR))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)
    simpAll goals completed! 🐙
  | Color.up =>c:Colori:Fin (repDim Color.up)j:Fin (repDim (complexLorentzTensor.τ Color.up))⊢ (complexLorentzTensor.contr Color.up) ((basis Color.up) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ Color.up)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    change Lorentz.contrCoContraction
      (Lorentz.complexContrBasisFin4 i ⊗ₜ Lorentz.complexCoBasisFin4 j) = _c:Colori:Fin (repDim Color.up)j:Fin (repDim (complexLorentzTensor.τ Color.up))⊢ Lorentz.contrCoContraction (Lorentz.complexContrBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    rw [Lorentz.contrCoContraction_basisc:Colori:Fin (repDim Color.up)j:Fin (repDim (complexLorentzTensor.τ Color.up))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)c:Colori:Fin (repDim Color.up)j:Fin (repDim (complexLorentzTensor.τ Color.up))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)]c:Colori:Fin (repDim Color.up)j:Fin (repDim (complexLorentzTensor.τ Color.up))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)
    simpAll goals completed! 🐙
  | Color.down =>c:Colori:Fin (repDim Color.down)j:Fin (repDim (complexLorentzTensor.τ Color.down))⊢ (complexLorentzTensor.contr Color.down) ((basis Color.down) i ⊗ₜ[ℂ] (basis (complexLorentzTensor.τ Color.down)) j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    change Lorentz.contrCoContraction
      (Lorentz.complexContrBasisFin4 i ⊗ₜ Lorentz.complexCoBasisFin4 j) = _c:Colori:Fin (repDim Color.down)j:Fin (repDim (complexLorentzTensor.τ Color.down))⊢ Lorentz.contrCoContraction (Lorentz.complexContrBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 j) =
  toComplexNum (if ↑i = ↑j then 1 else 0)
    rw [Lorentz.contrCoContraction_basisc:Colori:Fin (repDim Color.down)j:Fin (repDim (complexLorentzTensor.τ Color.down))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)c:Colori:Fin (repDim Color.down)j:Fin (repDim (complexLorentzTensor.τ Color.down))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)]c:Colori:Fin (repDim Color.down)j:Fin (repDim (complexLorentzTensor.τ Color.down))⊢ (if ↑i = ↑j then 1 else 0) = toComplexNum (if ↑i = ↑j then 1 else 0)
    simpAll goals completed! 🐙

lemma prodT_ofRat_ofRat {n n1 : ℕ} {c : Fin n → complexLorentzTensor.Color}
    (f : (ComponentIdx c) → RatComplexNum)
    {c1 : Fin n1 → complexLorentzTensor.Color}
    (f1 : (ComponentIdx c1) → RatComplexNum) :
    (prodT (ofRat f) (ofRat f1)) =
    ((ofRat (fun b => f (ComponentIdx.prod b).1 *
      f1 (ComponentIdx.prod b).2))) := byn:ℕn1:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumc1:Fin n1 → Colorf1:ComponentIdx c1 → RatComplexNum⊢ (prodT (ofRat f)) (ofRat f1) = ofRat fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2
  apply (Tensor.basis _).repr.injectiven:ℕn1:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumc1:Fin n1 → Colorf1:ComponentIdx c1 → RatComplexNum⊢ (Tensor.basis (Fin.append c c1)).repr ((prodT (ofRat f)) (ofRat f1)) =
  (Tensor.basis (Fin.append c c1)).repr (ofRat fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2)
  ext bn:ℕn1:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumc1:Fin n1 → Colorf1:ComponentIdx c1 → RatComplexNumb:ComponentIdx (Fin.append c c1)⊢ ((Tensor.basis (Fin.append c c1)).repr ((prodT (ofRat f)) (ofRat f1))) b =
  ((Tensor.basis (Fin.append c c1)).repr (ofRat fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2)) b
  rw [prodT_basis_repr_applyn:ℕn1:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumc1:Fin n1 → Colorf1:ComponentIdx c1 → RatComplexNumb:ComponentIdx (Fin.append c c1)⊢ ((Tensor.basis c).repr (ofRat f)) (ComponentIdx.prod b).1 *
    ((Tensor.basis c1).repr (ofRat f1)) (ComponentIdx.prod b).2 =
  ((Tensor.basis (Fin.append c c1)).repr (ofRat fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2)) bn:ℕn1:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumc1:Fin n1 → Colorf1:ComponentIdx c1 → RatComplexNumb:ComponentIdx (Fin.append c c1)⊢ ((Tensor.basis c).repr (ofRat f)) (ComponentIdx.prod b).1 *
    ((Tensor.basis c1).repr (ofRat f1)) (ComponentIdx.prod b).2 =
  ((Tensor.basis (Fin.append c c1)).repr (ofRat fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2)) b]n:ℕn1:ℕc:Fin n → Colorf:ComponentIdx c → RatComplexNumc1:Fin n1 → Colorf1:ComponentIdx c1 → RatComplexNumb:ComponentIdx (Fin.append c c1)⊢ ((Tensor.basis c).repr (ofRat f)) (ComponentIdx.prod b).1 *
    ((Tensor.basis c1).repr (ofRat f1)) (ComponentIdx.prod b).2 =
  ((Tensor.basis (Fin.append c c1)).repr (ofRat fun b => f (ComponentIdx.prod b).1 * f1 (ComponentIdx.prod b).2)) b
  simp only [ofRat_basis_repr_apply, map_mul]All goals completed! 🐙

lemma contrT_ofRat_eq_sum_dropPairSection {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.Color}
    {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ complexLorentzTensor.τ (c i) = c j }
    (f : (ComponentIdx c) → RatComplexNum) :
  (contrT n i j h (ofRat f)) = ((ofRat (fun b =>
    (∑ x : ComponentIdx.DropPairSection b,
      f x.1 * if (x.1 i).1 = (x.1 j).1 then 1 else 0)))) := byn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (contrT n i j h) (ofRat f) = ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0
  apply (Tensor.basis _).repr.injectiven:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (Tensor.basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) (ofRat f)) =
  (Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)
  ext bn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ((Tensor.basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) (ofRat f))) b =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) b
  rw [contrT_basis_repr_applyn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ∑ b',
    ((Tensor.basis c).repr (ofRat f)) ↑b' *
      (complexLorentzTensor.contr (c i))
        ((match c i with
            | Color.upL => Fermion.LeftHandedWeyl.basis
            | Color.downL => Fermion.DualLeftHandedWeyl.basis
            | Color.upR => Fermion.RightHandedWeyl.basis
            | Color.downR => Fermion.DualRightHandedWeyl.basis
            | Color.up => Lorentz.complexContrBasisFin4
            | Color.down => Lorentz.complexCoBasisFin4)
            (↑b' i) ⊗ₜ[ℂ]
          (match complexLorentzTensor.τ (c i) with
            | Color.upL => Fermion.LeftHandedWeyl.basis
            | Color.downL => Fermion.DualLeftHandedWeyl.basis
            | Color.upR => Fermion.RightHandedWeyl.basis
            | Color.downR => Fermion.DualRightHandedWeyl.basis
            | Color.up => Lorentz.complexContrBasisFin4
            | Color.down => Lorentz.complexCoBasisFin4)
            ((basisIdxCongr ⋯) (↑b' j))) =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) bn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ∑ b',
    ((Tensor.basis c).repr (ofRat f)) ↑b' *
      (complexLorentzTensor.contr (c i))
        ((match c i with
            | Color.upL => Fermion.LeftHandedWeyl.basis
            | Color.downL => Fermion.DualLeftHandedWeyl.basis
            | Color.upR => Fermion.RightHandedWeyl.basis
            | Color.downR => Fermion.DualRightHandedWeyl.basis
            | Color.up => Lorentz.complexContrBasisFin4
            | Color.down => Lorentz.complexCoBasisFin4)
            (↑b' i) ⊗ₜ[ℂ]
          (match complexLorentzTensor.τ (c i) with
            | Color.upL => Fermion.LeftHandedWeyl.basis
            | Color.downL => Fermion.DualLeftHandedWeyl.basis
            | Color.upR => Fermion.RightHandedWeyl.basis
            | Color.downR => Fermion.DualRightHandedWeyl.basis
            | Color.up => Lorentz.complexContrBasisFin4
            | Color.down => Lorentz.complexCoBasisFin4)
            ((basisIdxCongr ⋯) (↑b' j))) =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) b]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ∑ b',
    ((Tensor.basis c).repr (ofRat f)) ↑b' *
      (complexLorentzTensor.contr (c i))
        ((match c i with
            | Color.upL => Fermion.LeftHandedWeyl.basis
            | Color.downL => Fermion.DualLeftHandedWeyl.basis
            | Color.upR => Fermion.RightHandedWeyl.basis
            | Color.downR => Fermion.DualRightHandedWeyl.basis
            | Color.up => Lorentz.complexContrBasisFin4
            | Color.down => Lorentz.complexCoBasisFin4)
            (↑b' i) ⊗ₜ[ℂ]
          (match complexLorentzTensor.τ (c i) with
            | Color.upL => Fermion.LeftHandedWeyl.basis
            | Color.downL => Fermion.DualLeftHandedWeyl.basis
            | Color.upR => Fermion.RightHandedWeyl.basis
            | Color.downR => Fermion.DualRightHandedWeyl.basis
            | Color.up => Lorentz.complexContrBasisFin4
            | Color.down => Lorentz.complexCoBasisFin4)
            ((basisIdxCongr ⋯) (↑b' j))) =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) b
  conv_lhs =>
    enter [2, x]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:↥b.DropPairSection| ((Tensor.basis c).repr (ofRat f)) ↑x *
  (complexLorentzTensor.contr (c i))
    ((match c i with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        (↑x i) ⊗ₜ[ℂ]
      (match complexLorentzTensor.τ (c i) with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        ((basisIdxCongr ⋯) (↑x j)))
    rw [contr_basis_ratComplexNum]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:↥b.DropPairSection| ((Tensor.basis c).repr (ofRat f)) ↑x * toComplexNum (if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0)
    simp only [Nat.succ_eq_add_one, Finset.univ_eq_attach,
    ofRat_basis_repr_apply, Fin.val_cast, mul_one,
    mul_zero, Function.comp_apply]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:↥b.DropPairSection| toComplexNum (f ↑x) * toComplexNum (if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0)
    rw [← Physlib.RatComplexNum.toComplexNum.map_mul]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:↥b.DropPairSection| toComplexNum (f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0)
  rw [← map_sum Physlib.RatComplexNum.toComplexNumn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0) =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) bn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0) =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) b]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0) =
  ((Tensor.basis (c ∘ i.succSuccAbove j)).repr (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)) b
  rw [ofRat_basis_repr_applyn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0) =
  toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0) =
  toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑((basisIdxCongr ⋯) (↑x j)) then 1 else 0) =
  toComplexNum (∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0)
  simp [basisIdxCongr_eq_cast]All goals completed! 🐙
lemma contrT_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.Color}
    {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ complexLorentzTensor.τ (c i) = c j }
    (f : (ComponentIdx c) → RatComplexNum) :
  (contrT n i j h (ofRat f)) = ((ofRat (fun b =>
    (∑ x : Fin (complexLorentzTensor.repDim (c i)),
      f (DropPairSection.ofFinEquiv h.1 b (x, Fin.cast (byn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ repDim (c i) = repDim (c j)
        simp [← h.2, complexLorentzTensor.repDim_tau]All goals completed! 🐙) x)))))) := byn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (contrT n i j h) (ofRat f) = ofRat fun b => ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  rw [contrT_ofRat_eq_sum_dropPairSectionn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0) =
  ofRat fun b => ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0) =
  ofRat fun b => ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))]n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (ofRat fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0) =
  ofRat fun b => ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  congre_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNum⊢ (fun b => ∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0) = fun b =>
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  funext be_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ x, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0) = ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  rw [← (DropPairSection.ofFinEquiv h.1 b).sum_compe_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ i_1,
    f ↑((DropPairSection.ofFinEquiv ⋯ b) i_1) *
      if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) i_1) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) i_1) j) then 1 else 0) =
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))e_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ i_1,
    f ↑((DropPairSection.ofFinEquiv ⋯ b) i_1) *
      if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) i_1) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) i_1) j) then 1 else 0) =
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))]e_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ i_1,
    f ↑((DropPairSection.ofFinEquiv ⋯ b) i_1) *
      if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) i_1) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) i_1) j) then 1 else 0) =
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  rw [Fintype.sum_prod_typee_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ x,
    ∑ y,
      f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) then 1
        else 0) =
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))e_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ x,
    ∑ y,
      f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) then 1
        else 0) =
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))]e_6n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (∑ x,
    ∑ y,
      f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) then 1
        else 0) =
  ∑ x, f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  congre_6.e_fn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)⊢ (fun x =>
    ∑ y,
      f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) then 1
        else 0) =
  fun x => f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  funext xe_6.e_fn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ (∑ y,
    f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) *
      if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) then 1
      else 0) =
  f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))
  rw [Finset.sum_eq_single (Fin.cast (byn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ repDim (c i) = repDim (c j)e_6.e_fn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
    if
        ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
      1
    else 0) =
  f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ Fin.cast ⋯ x →
    (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) j) then 1
        else 0) =
      0e_6.e_f.h₁n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ Fin.cast ⋯ x ∉ Finset.univ →
  (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
      if
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
            ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
        1
      else 0) =
    0 simp [← h.2, repDim_tau]All goals completed! 🐙e_6.e_fn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
    if
        ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
      1
    else 0) =
  f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ Fin.cast ⋯ x →
    (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) j) then 1
        else 0) =
      0e_6.e_f.h₁n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ Fin.cast ⋯ x ∉ Finset.univ →
  (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
      if
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
            ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
        1
      else 0) =
    0) x)]e_6.e_fn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
    if
        ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
      1
    else 0) =
  f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ Fin.cast ⋯ x →
    (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) j) then 1
        else 0) =
      0e_6.e_f.h₁n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ Fin.cast ⋯ x ∉ Finset.univ →
  (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
      if
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
            ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
        1
      else 0) =
    0
  ·e_6.e_fn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
    if
        ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
      1
    else 0) =
  f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) simpAll goals completed! 🐙
  ·e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ Fin.cast ⋯ x →
    (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) *
        if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, b_1)) j) then 1
        else 0) =
      0 intro y _ hye_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) *
    if ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) then 1
    else 0) =
  0
    rw [if_nege_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) * 0 = 0e_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ ¬↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j)e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) * 0 = 0e_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ ¬↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j)]e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) * 0 = 0e_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ ¬↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j)
    ·e_6.e_f.h₀n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) * 0 = 0 simpAll goals completed! 🐙
    ·e_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ ¬↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) i) = ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, y)) j) simp only [DropPairSection.ofFinEquiv_apply_fst, DropPairSection.ofFinEquiv_apply_snd]e_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:y ≠ Fin.cast ⋯ x⊢ ¬↑x = ↑y
      rw [@Fin.ne_iff_vnee_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:↑y ≠ ↑(Fin.cast ⋯ x)⊢ ¬↑x = ↑ye_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:↑y ≠ ↑(Fin.cast ⋯ x)⊢ ¬↑x = ↑y] at hye_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:↑y ≠ ↑(Fin.cast ⋯ x)⊢ ¬↑x = ↑y
      simp only [Fin.val_cast, ne_eq] at hye_6.e_f.h₀.hncn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))y:Fin (repDim (c j))a✝:y ∈ Finset.univhy:¬↑y = ↑x⊢ ¬↑x = ↑y
      exact fun a => hy ((Eq.symm a))All goals completed! 🐙
  ·e_6.e_f.h₁n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jf:ComponentIdx c → RatComplexNumb:ComponentIdx (c ∘ i.succSuccAbove j)x:Fin (repDim (c i))⊢ Fin.cast ⋯ x ∉ Finset.univ →
  (f ↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) *
      if
          ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) i) =
            ↑(↑((DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x)) j) then
        1
      else 0) =
    0 simpAll goals completed! 🐙lemma permT_ofRat {n m : ℕ} {c : Fin n → complexLorentzTensor.Color}
    {c1 : Fin m → complexLorentzTensor.Color}
    {σ : Fin m → Fin n} (h : IsReindexing c c1 σ)
    (f : ComponentIdx c → RatComplexNum) :
    (permT σ h ((ofRat f))) =
    ((ofRat (fun b => f (fun i => Fin.cast (byn:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNumb:ComponentIdx c1i:Fin n⊢ repDim (c1 (IsReindexing.inv σ h i)) = repDim (c i) simp [IsReindexing.inv_perserve_color]All goals completed! 🐙)
      (b (h.inv σ i)))))) := byn:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNum⊢ (permT σ h) (ofRat f) = ofRat fun b => f fun i => Fin.cast ⋯ (b (IsReindexing.inv σ h i))
  apply (Tensor.basis _).repr.injectiven:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNum⊢ (Tensor.basis c1).repr ((permT σ h) (ofRat f)) =
  (Tensor.basis c1).repr (ofRat fun b => f fun i => Fin.cast ⋯ (b (IsReindexing.inv σ h i)))
  ext bn:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNumb:ComponentIdx c1⊢ ((Tensor.basis c1).repr ((permT σ h) (ofRat f))) b =
  ((Tensor.basis c1).repr (ofRat fun b => f fun i => Fin.cast ⋯ (b (IsReindexing.inv σ h i)))) b
  simp only [permT_basis_repr_symm_apply, ofRat_basis_repr_apply]n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNumb:ComponentIdx c1⊢ toComplexNum (f fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv σ h i))) =
  toComplexNum (f fun i => Fin.cast ⋯ (b (IsReindexing.inv σ h i)))
  congre_6n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNumb:ComponentIdx c1⊢ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv σ h i))) = fun i => Fin.cast ⋯ (b (IsReindexing.inv σ h i))
  ext ie_6n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σf:ComponentIdx c → RatComplexNumb:ComponentIdx c1i:Fin n⊢ ↑((basisIdxCongr ⋯) (b (IsReindexing.inv σ h i))) = ↑(Fin.cast ⋯ (b (IsReindexing.inv σ h i)))
  simp [basisIdxCongr_eq_cast]All goals completed! 🐙