Physlib.Relativity.Tensors.ComplexTensor.Units.Basic

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.Relativity.Tensors.ComplexTensor.OfRat

Unit tensors for complex Lorentz tensors

@[expose] public section

Definitions.

The unit δᵢⁱ as a complex Lorentz tensor.

abbrev coContrUnit : ℂT[.down, .up] := complexLorentzTensor.unitTensor Color.up

The unit δⁱᵢ as a complex Lorentz tensor.

abbrev contrCoUnit : ℂT[.up, .down] := complexLorentzTensor.unitTensor Color.down

The unit δₐᵃ as a complex Lorentz tensor.

abbrev dualLeftLeftUnit : ℂT[.downL, .upL] := complexLorentzTensor.unitTensor Color.upL

The unit δᵃₐ as a complex Lorentz tensor.

abbrev leftDualLeftUnit : ℂT[.upL, .downL] := complexLorentzTensor.unitTensor Color.downL

The unit δ_{dot a}^{dot a} as a complex Lorentz tensor.

abbrev dualRightRightUnit : ℂT[.downR, .upR] := complexLorentzTensor.unitTensor Color.upR

The unit δ^{dot a}_{dot a} as a complex Lorentz tensor.

abbrev rightDualRightUnit : ℂT[.upR, .downR] := complexLorentzTensor.unitTensor Color.downR

Notation

The unit δᵢⁱ as a complex Lorentz tensor.

scoped[complexLorentzTensor] notation "δ'" => coContrUnit

The unit δⁱᵢ as a complex Lorentz tensor.

scoped[complexLorentzTensor] notation "δ" => contrCoUnit

The unit δₐᵃ as a complex Lorentz tensor.

scoped[complexLorentzTensor] notation "δL'" => dualLeftLeftUnit

The unit δᵃₐ as a complex Lorentz tensor.

scoped[complexLorentzTensor] notation "δL" => leftDualLeftUnit

The unit δ_{dot a}^{dot a} as a complex Lorentz tensor.

scoped[complexLorentzTensor] notation "δR'" => dualRightRightUnit

The unit δ^{dot a}_{dot a} as a complex Lorentz tensor.

scoped[complexLorentzTensor] notation "δR" => rightDualRightUnit

Other forms

fromConstPair

              

lemma coContrUnit_eq_fromConstPair : δ' = fromConstPair Lorentz.coContrUnit := by⊢ δ' = fromConstPair Lorentz.coContrUnit
  rw [Lorentz.coContrUnit⊢ δ' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • Lorentz.coContrUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }⊢ δ' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • Lorentz.coContrUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }]⊢ δ' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • Lorentz.coContrUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }
  rflAll goals completed! 🐙

lemma contrCoUnit_eq_fromConstPair : δ = fromConstPair Lorentz.contrCoUnit := by⊢ δ = fromConstPair Lorentz.contrCoUnit
  rw [Lorentz.contrCoUnit⊢ δ =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • Lorentz.contrCoUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }⊢ δ =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • Lorentz.contrCoUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }]⊢ δ =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • Lorentz.contrCoUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }
  rflAll goals completed! 🐙

lemma dualLeftLeftUnit_eq_fromConstPair : δL' = fromConstPair Fermion.dualLeftLeftUnit := by⊢ δL' = fromConstPair Fermion.dualLeftLeftUnit
  rw [Fermion.dualLeftLeftUnit⊢ δL' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • dualLeftLeftUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }⊢ δL' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • dualLeftLeftUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }]⊢ δL' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • dualLeftLeftUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }
  rflAll goals completed! 🐙

lemma leftDualLeftUnit_eq_fromConstPair : δL = fromConstPair Fermion.leftDualLeftUnit := by⊢ δL = fromConstPair Fermion.leftDualLeftUnit
  rw [Fermion.leftDualLeftUnit⊢ δL =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • leftDualLeftUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }⊢ δL =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • leftDualLeftUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }]⊢ δL =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • leftDualLeftUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }
  rflAll goals completed! 🐙

lemma dualRightRightUnit_eq_fromConstPair : δR' = fromConstPair Fermion.dualRightRightUnit := by⊢ δR' = fromConstPair Fermion.dualRightRightUnit
  rw [Fermion.dualRightRightUnit⊢ δR' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • dualRightRightUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }⊢ δR' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • dualRightRightUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }]⊢ δR' =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • dualRightRightUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }
  rflAll goals completed! 🐙

lemma rightDualRightUnit_eq_fromConstPair : δR = fromConstPair Fermion.rightDualRightUnit := by⊢ δR = fromConstPair Fermion.rightDualRightUnit
  rw [Fermion.rightDualRightUnit⊢ δR =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • rightDualRightUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }⊢ δR =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • rightDualRightUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }]⊢ δR =
  fromConstPair
    {
      toFun := fun a =>
        have a' := a;
        a' • rightDualRightUnitVal,
      map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }
  rflAll goals completed! 🐙

fromPairT

              

lemma coContrUnit_eq_fromPairT : δ' = fromPairT (Lorentz.coContrUnitVal) := by⊢ δ' = fromPairT Lorentz.coContrUnitVal
  rw [coContrUnit_eq_fromConstPair,⊢ fromConstPair Lorentz.coContrUnit = fromPairT Lorentz.coContrUnitVal⊢ fromPairT (Lorentz.coContrUnit 1) = fromPairT Lorentz.coContrUnitVal fromConstPair⊢ fromPairT (Lorentz.coContrUnit 1) = fromPairT Lorentz.coContrUnitVal⊢ fromPairT (Lorentz.coContrUnit 1) = fromPairT Lorentz.coContrUnitVal]⊢ fromPairT (Lorentz.coContrUnit 1) = fromPairT Lorentz.coContrUnitVal
  congr 1e_6⊢ Lorentz.coContrUnit 1 = Lorentz.coContrUnitVal
  exact Lorentz.coContrUnit_apply_oneAll goals completed! 🐙

lemma contrCoUnit_eq_fromPairT : δ = fromPairT (Lorentz.contrCoUnitVal) := by⊢ δ = fromPairT Lorentz.contrCoUnitVal
  rw [contrCoUnit_eq_fromConstPair,⊢ fromConstPair Lorentz.contrCoUnit = fromPairT Lorentz.contrCoUnitVal⊢ fromPairT (Lorentz.contrCoUnit 1) = fromPairT Lorentz.contrCoUnitVal fromConstPair⊢ fromPairT (Lorentz.contrCoUnit 1) = fromPairT Lorentz.contrCoUnitVal⊢ fromPairT (Lorentz.contrCoUnit 1) = fromPairT Lorentz.contrCoUnitVal]⊢ fromPairT (Lorentz.contrCoUnit 1) = fromPairT Lorentz.contrCoUnitVal
  congr 1e_6⊢ Lorentz.contrCoUnit 1 = Lorentz.contrCoUnitVal
  exact Lorentz.contrCoUnit_apply_oneAll goals completed! 🐙

lemma dualLeftLeftUnit_eq_fromPairT : δL' = fromPairT (Fermion.dualLeftLeftUnitVal) := by⊢ δL' = fromPairT dualLeftLeftUnitVal
  rw [dualLeftLeftUnit_eq_fromConstPair,⊢ fromConstPair Fermion.dualLeftLeftUnit = fromPairT dualLeftLeftUnitVal⊢ fromPairT (Fermion.dualLeftLeftUnit 1) = fromPairT dualLeftLeftUnitVal fromConstPair⊢ fromPairT (Fermion.dualLeftLeftUnit 1) = fromPairT dualLeftLeftUnitVal⊢ fromPairT (Fermion.dualLeftLeftUnit 1) = fromPairT dualLeftLeftUnitVal]⊢ fromPairT (Fermion.dualLeftLeftUnit 1) = fromPairT dualLeftLeftUnitVal
  congr 1e_6⊢ Fermion.dualLeftLeftUnit 1 = dualLeftLeftUnitVal
  exact Fermion.dualLeftLeftUnit_apply_oneAll goals completed! 🐙

lemma leftDualLeftUnit_eq_fromPairT : δL = fromPairT (Fermion.leftDualLeftUnitVal) := by⊢ δL = fromPairT leftDualLeftUnitVal
  rw [leftDualLeftUnit_eq_fromConstPair,⊢ fromConstPair Fermion.leftDualLeftUnit = fromPairT leftDualLeftUnitVal⊢ fromPairT (Fermion.leftDualLeftUnit 1) = fromPairT leftDualLeftUnitVal fromConstPair⊢ fromPairT (Fermion.leftDualLeftUnit 1) = fromPairT leftDualLeftUnitVal⊢ fromPairT (Fermion.leftDualLeftUnit 1) = fromPairT leftDualLeftUnitVal]⊢ fromPairT (Fermion.leftDualLeftUnit 1) = fromPairT leftDualLeftUnitVal
  congr 1e_6⊢ Fermion.leftDualLeftUnit 1 = leftDualLeftUnitVal
  exact Fermion.leftDualLeftUnit_apply_oneAll goals completed! 🐙

lemma dualRightRightUnit_eq_fromPairT : δR' = fromPairT (Fermion.dualRightRightUnitVal) := by⊢ δR' = fromPairT dualRightRightUnitVal
  rw [dualRightRightUnit_eq_fromConstPair,⊢ fromConstPair Fermion.dualRightRightUnit = fromPairT dualRightRightUnitVal⊢ fromPairT (Fermion.dualRightRightUnit 1) = fromPairT dualRightRightUnitVal fromConstPair⊢ fromPairT (Fermion.dualRightRightUnit 1) = fromPairT dualRightRightUnitVal⊢ fromPairT (Fermion.dualRightRightUnit 1) = fromPairT dualRightRightUnitVal]⊢ fromPairT (Fermion.dualRightRightUnit 1) = fromPairT dualRightRightUnitVal
  congr 1e_6⊢ Fermion.dualRightRightUnit 1 = dualRightRightUnitVal
  exact Fermion.dualRightRightUnit_apply_oneAll goals completed! 🐙

lemma rightDualRightUnit_eq_fromPairT : δR = fromPairT (Fermion.rightDualRightUnitVal) := by⊢ δR = fromPairT rightDualRightUnitVal
  rw [rightDualRightUnit_eq_fromConstPair,⊢ fromConstPair Fermion.rightDualRightUnit = fromPairT rightDualRightUnitVal⊢ fromPairT (Fermion.rightDualRightUnit 1) = fromPairT rightDualRightUnitVal fromConstPair⊢ fromPairT (Fermion.rightDualRightUnit 1) = fromPairT rightDualRightUnitVal⊢ fromPairT (Fermion.rightDualRightUnit 1) = fromPairT rightDualRightUnitVal]⊢ fromPairT (Fermion.rightDualRightUnit 1) = fromPairT rightDualRightUnitVal
  congr 1e_6⊢ Fermion.rightDualRightUnit 1 = rightDualRightUnitVal
  exact Fermion.rightDualRightUnit_apply_oneAll goals completed! 🐙

complexCoBasis etc.

basis

              

lemma coContrUnit_eq_basis : δ' =
    ∑ i, Tensor.basis (S := complexLorentzTensor)
      ![Color.down, Color.up] (fun | 0 => i | 1 => i) := by⊢ δ' =
  ∑ i,
    (Tensor.basis ![Color.down, Color.up]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  rw [coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4⊢ ∑ i, fromPairT (Lorentz.complexCoBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 i) =
  ∑ i,
    (Tensor.basis ![Color.down, Color.up]) fun x =>
      match x with
      | 0 => i
      | 1 => i⊢ ∑ i, fromPairT (Lorentz.complexCoBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 i) =
  ∑ i,
    (Tensor.basis ![Color.down, Color.up]) fun x =>
      match x with
      | 0 => i
      | 1 => i]⊢ ∑ i, fromPairT (Lorentz.complexCoBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 i) =
  ∑ i,
    (Tensor.basis ![Color.down, Color.up]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  conv_lhs =>
    enter [2, x]x:Fin 4| fromPairT (Lorentz.complexCoBasisFin4 x ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 x)
    change fromPairT ((complexLorentzTensor.basis .down x) ⊗ₜ[ℂ]
      (complexLorentzTensor.basis .up _))x:Fin 4| fromPairT ((basis Color.down) x ⊗ₜ[ℂ] (basis Color.up) x)
    rw [fromPairT_apply_basis_repr]x:Fin 4| (Tensor.basis ![Color.down, Color.up]) fun x_1 =>
  match x_1 with
  | 0 => x
  | 1 => x
  rflAll goals completed! 🐙

lemma contrCoUnit_eq_basis : δ =
    ∑ i, Tensor.basis (S := complexLorentzTensor)
      ![Color.up, Color.down] (fun | 0 => i | 1 => i) := by⊢ δ =
  ∑ i,
    (Tensor.basis ![Color.up, Color.down]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  rw [contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4⊢ ∑ i, fromPairT (Lorentz.complexContrBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 i) =
  ∑ i,
    (Tensor.basis ![Color.up, Color.down]) fun x =>
      match x with
      | 0 => i
      | 1 => i⊢ ∑ i, fromPairT (Lorentz.complexContrBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 i) =
  ∑ i,
    (Tensor.basis ![Color.up, Color.down]) fun x =>
      match x with
      | 0 => i
      | 1 => i]⊢ ∑ i, fromPairT (Lorentz.complexContrBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 i) =
  ∑ i,
    (Tensor.basis ![Color.up, Color.down]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  conv_lhs =>
    enter [2, x]x:Fin 4| fromPairT (Lorentz.complexContrBasisFin4 x ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 x)
    change fromPairT ((complexLorentzTensor.basis .up x) ⊗ₜ[ℂ]
      (complexLorentzTensor.basis .down _))x:Fin 4| fromPairT ((basis Color.up) x ⊗ₜ[ℂ] (basis Color.down) x)
    rw [fromPairT_apply_basis_repr]x:Fin 4| (Tensor.basis ![Color.up, Color.down]) fun x_1 =>
  match x_1 with
  | 0 => x
  | 1 => x
  rflAll goals completed! 🐙

lemma dualLeftLeftUnit_eq_tensor_basis : δL' =
    ∑ i, Tensor.basis (S := complexLorentzTensor)
      ![Color.downL, Color.upL] (fun | 0 => i | 1 => i) := by⊢ δL' =
  ∑ i,
    (Tensor.basis ![Color.downL, Color.upL]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  rw [dualLeftLeftUnit_eq_basis⊢ ∑ i, fromPairT (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.downL, Color.upL]) fun x =>
      match x with
      | 0 => i
      | 1 => i⊢ ∑ i, fromPairT (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.downL, Color.upL]) fun x =>
      match x with
      | 0 => i
      | 1 => i]⊢ ∑ i, fromPairT (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.downL, Color.upL]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  conv_lhs =>
    enter [2, x]x:Fin 2| fromPairT (DualLeftHandedWeyl.basis x ⊗ₜ[ℂ] LeftHandedWeyl.basis x)
    change fromPairT ((complexLorentzTensor.basis .downL x) ⊗ₜ[ℂ]
      (complexLorentzTensor.basis .upL _))x:Fin 2| fromPairT ((basis Color.downL) x ⊗ₜ[ℂ] (basis Color.upL) x)
    rw [fromPairT_apply_basis_repr]x:Fin 2| (Tensor.basis ![Color.downL, Color.upL]) fun x_1 =>
  match x_1 with
  | 0 => x
  | 1 => x
  rflAll goals completed! 🐙

lemma leftDualLeftUnit_eq_tensor_basis : δL =
    ∑ i, Tensor.basis (S := complexLorentzTensor)
      ![Color.upL, Color.downL] (fun | 0 => i | 1 => i) := by⊢ δL =
  ∑ i,
    (Tensor.basis ![Color.upL, Color.downL]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  rw [leftDualLeftUnit_eq_basis⊢ ∑ i, fromPairT (LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.upL, Color.downL]) fun x =>
      match x with
      | 0 => i
      | 1 => i⊢ ∑ i, fromPairT (LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.upL, Color.downL]) fun x =>
      match x with
      | 0 => i
      | 1 => i]⊢ ∑ i, fromPairT (LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.upL, Color.downL]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  conv_lhs =>
    enter [2, x]x:Fin 2| fromPairT (LeftHandedWeyl.basis x ⊗ₜ[ℂ] DualLeftHandedWeyl.basis x)
    change fromPairT ((complexLorentzTensor.basis .upL x) ⊗ₜ[ℂ]
      (complexLorentzTensor.basis .downL _))x:Fin 2| fromPairT ((basis Color.upL) x ⊗ₜ[ℂ] (basis Color.downL) x)
    rw [fromPairT_apply_basis_repr]x:Fin 2| (Tensor.basis ![Color.upL, Color.downL]) fun x_1 =>
  match x_1 with
  | 0 => x
  | 1 => x
  rflAll goals completed! 🐙

lemma dualRightRightUnit_eq_tensor_basis : δR' =
    ∑ i, Tensor.basis (S := complexLorentzTensor)
      ![Color.downR, Color.upR] (fun | 0 => i | 1 => i) := by⊢ δR' =
  ∑ i,
    (Tensor.basis ![Color.downR, Color.upR]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  rw [dualRightRightUnit_eq_basis⊢ ∑ i, fromPairT (DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.downR, Color.upR]) fun x =>
      match x with
      | 0 => i
      | 1 => i⊢ ∑ i, fromPairT (DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.downR, Color.upR]) fun x =>
      match x with
      | 0 => i
      | 1 => i]⊢ ∑ i, fromPairT (DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.downR, Color.upR]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  conv_lhs =>
    enter [2, x]x:Fin 2| fromPairT (DualRightHandedWeyl.basis x ⊗ₜ[ℂ] RightHandedWeyl.basis x)
    change fromPairT ((complexLorentzTensor.basis .downR x) ⊗ₜ[ℂ]
      (complexLorentzTensor.basis .upR _))x:Fin 2| fromPairT ((basis Color.downR) x ⊗ₜ[ℂ] (basis Color.upR) x)
    rw [fromPairT_apply_basis_repr]x:Fin 2| (Tensor.basis ![Color.downR, Color.upR]) fun x_1 =>
  match x_1 with
  | 0 => x
  | 1 => x
  rflAll goals completed! 🐙

lemma rightDualRightUnit_eq_tensor_basis : δR =
    ∑ i, Tensor.basis (S := complexLorentzTensor)
      ![Color.upR, Color.downR] (fun | 0 => i | 1 => i) := by⊢ δR =
  ∑ i,
    (Tensor.basis ![Color.upR, Color.downR]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  rw [rightDualRightUnit_eq_basis⊢ ∑ i, fromPairT (RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.upR, Color.downR]) fun x =>
      match x with
      | 0 => i
      | 1 => i⊢ ∑ i, fromPairT (RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.upR, Color.downR]) fun x =>
      match x with
      | 0 => i
      | 1 => i]⊢ ∑ i, fromPairT (RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis i) =
  ∑ i,
    (Tensor.basis ![Color.upR, Color.downR]) fun x =>
      match x with
      | 0 => i
      | 1 => i
  conv_lhs =>
    enter [2, x]x:Fin 2| fromPairT (RightHandedWeyl.basis x ⊗ₜ[ℂ] DualRightHandedWeyl.basis x)
    change fromPairT ((complexLorentzTensor.basis .upR x) ⊗ₜ[ℂ]
      (complexLorentzTensor.basis .downR _))x:Fin 2| fromPairT ((basis Color.upR) x ⊗ₜ[ℂ] (basis Color.downR) x)
    rw [fromPairT_apply_basis_repr]x:Fin 2| (Tensor.basis ![Color.upR, Color.downR]) fun x_1 =>
  match x_1 with
  | 0 => x
  | 1 => x
  rflAll goals completed! 🐙