Physlib.Relativity.Tensors.RealTensor.Basic

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.RealTensor.Metrics.Pre
public import Physlib.Relativity.Tensors.Contraction.Basis
public import Physlib.Relativity.Tensors.Elab

Real Lorentz tensors

Within this directory Pre is used to denote that the definitions are preliminary and which are used to define realLorentzTensor.

@[expose] public section

The colors associated with complex representations of SL(2, ℂ) of interest to physics.

The color associated with contravariant Lorentz vectors.

The color associated with covariant Lorentz vectors.

              inductive Color  | up : Color  | down : Color
deriving Fintype

Color for complex Lorentz tensors is decidable.

instance : DecidableEq Color := fun x y =>
  match x, y with
  | Color.up, Color.up => isTrue rfl
  | Color.down, Color.down => isTrue rfl
  /- The false -/
  | Color.up, Color.down => isFalse fun h => Color.noConfusion h
  | Color.down, Color.up => isFalse fun h => Color.noConfusion h

The modules associated with each of the different types of real Lorentz vector space.

abbrev modules (d : ℕ) : Color → Type
  | Color.up => Lorentz.ContrMod d
  | Color.down => Lorentz.CoMod d

              instance modulesAddCommGroup (d : ℕ) : ∀ c, AddCommGroup (modules d c)
  | Color.up => inferInstance
  | Color.down => inferInstanceinstance modulesModule (d : ℕ) : ∀ c, Module ℝ (modules d c)
  | Color.up => inferInstance
  | Color.down => inferInstanceTODO "Replace Lorentz.ContrMod and Lorentz.CoMod in the definition of realLorentzTensor
  directly with Lorentz.Vector and Lorentz.Covector, and
  representations defined on them."

Notation for a real Lorentz tensor.

syntax (name := realLorentzTensorSyntax) "ℝT[" term,* "]" : term

macro_rules
  | `(ℝT[$termDim:term, $term:term, $terms:term,*]) =>
      `(((realLorentzTensor $termDim).Tensor (vecCons $term ![$terms,*])))
  | `(ℝT[$termDim:term, $term:term]) =>
    `(((realLorentzTensor $termDim).Tensor (vecCons $term ![])))
  | `(ℝT[$termDim:term]) =>`(((realLorentzTensor $termDim).Tensor (vecEmpty)))
  | `(ℝT[]) =>`(((realLorentzTensor 3).Tensor (vecEmpty)))

Notation for a real Lorentz tensor.

set_option quotPrecheck false in

scoped[realLorentzTensor] notation "ℝT(" d "," c ")" =>
  (realLorentzTensor d).Tensor c

Basis and discrete functor objects

These re-express fields of realLorentzTensor d in terms of Lorentz data.

@[simp]
lemma basisIdxCongr_eq_refl {d : ℕ} {c1 c2 : realLorentzTensor.Color} (h : c1 = c2) :
    TensorSpecies.basisIdxCongr (basisIdx := fun _ => Fin 1 ⊕ Fin d) h = Equiv.refl _ := byd:ℕc1:Colorc2:Colorh:c1 = c2⊢ TensorSpecies.basisIdxCongr h = Equiv.refl (Fin 1 ⊕ Fin d)
  rflAll goals completed! 🐙

lemma basisIdxCongr_apply {d : ℕ} {c1 c2 : realLorentzTensor.Color} (h : c1 = c2)
    (i : Fin 1 ⊕ Fin d) :
    TensorSpecies.basisIdxCongr (basisIdx := fun _ => Fin 1 ⊕ Fin d) h i = i := byd:ℕc1:Colorc2:Colorh:c1 = c2i:Fin 1 ⊕ Fin d⊢ (TensorSpecies.basisIdxCongr h) i = i
  simpAll goals completed! 🐙

Simplifying τ

@[simp]
lemma τ_up_eq_down {d : ℕ} : (realLorentzTensor d).τ Color.up = Color.down := rfl

@[simp]
lemma τ_down_eq_up {d : ℕ} : (realLorentzTensor d).τ Color.down = Color.up := rfl

Contractions and to Field

              attribute [-simp] Fintype.sum_sum_typelemma contrPCoeff_basis {d n : ℕ} {c : Fin n → realLorentzTensor.Color} (i j : Fin n)
    (hij : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j)
    (b : ComponentIdx (S := realLorentzTensor d) c) :
    Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i = b j then 1 else 0 := byd:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i = b j then 1 else 0
  simp only [Pure.contrPCoeff, Pure.basisVector]d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ ((realLorentzTensor d).contr (c i))
    ((match c i with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        (b i) ⊗ₜ[ℝ]
      (LinearEquiv.cast ⋯)
        ((match c j with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          (b j))) =
  if b i = b j then 1 else 0
  generalize_proofs h1 h2d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)h2:c j = (realLorentzTensor d).τ (c i)⊢ ((realLorentzTensor d).contr (c i))
    ((match c i with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        (b i) ⊗ₜ[ℝ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          (b j))) =
  if b i = b j then 1 else 0
  generalize b i = b1 at *d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)h2:c j = (realLorentzTensor d).τ (c i)b1:Fin 1 ⊕ Fin d⊢ ((realLorentzTensor d).contr (c i))
    ((match c i with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          (b j))) =
  if b1 = b j then 1 else 0
  generalize b j = b2 at *d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)h2:c j = (realLorentzTensor d).τ (c i)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin d⊢ ((realLorentzTensor d).contr (c i))
    ((match c i with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0
  generalize c i = ci at *d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dci:Colorhij:i ≠ j ∧ (realLorentzTensor d).τ ci = c jh2:c j = (realLorentzTensor d).τ ci⊢ ((realLorentzTensor d).contr ci)
    ((match ci with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0
  generalize c j = cj at *d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dci:Colorcj:Colorhij:i ≠ j ∧ (realLorentzTensor d).τ ci = cjh2:cj = (realLorentzTensor d).τ ci⊢ ((realLorentzTensor d).contr ci)
    ((match ci with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast h2)
        ((match cj with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0
  subst h2d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dci:Colorhij:i ≠ j ∧ (realLorentzTensor d).τ ci = (realLorentzTensor d).τ ci⊢ ((realLorentzTensor d).contr ci)
    ((match ci with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast ⋯)
        ((match (realLorentzTensor d).τ ci with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0
  fin_cases ci«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ ((realLorentzTensor d).contr Color.up)
    ((match Color.up with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast ⋯)
        ((match (realLorentzTensor d).τ Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ ((realLorentzTensor d).contr Color.down)
    ((match Color.down with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast ⋯)
        ((match (realLorentzTensor d).τ Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0
  ·«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ ((realLorentzTensor d).contr Color.up)
    ((match Color.up with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast ⋯)
        ((match (realLorentzTensor d).τ Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0 simp [realLorentzTensor]«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ Lorentz.contrCoContract ((Lorentz.contrBasis d) b1 ⊗ₜ[ℝ] (LinearEquiv.cast ⋯) ((Lorentz.coBasis d) b2)) =
  if b1 = b2 then 1 else 0
    erw [LinearEquiv.cast_apply«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ Lorentz.contrCoContract ((Lorentz.contrBasis d) b1 ⊗ₜ[ℝ] cast ⋯ ((Lorentz.coBasis d) b2)) = if b1 = b2 then 1 else 0]«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ Lorentz.contrCoContract ((Lorentz.contrBasis d) b1 ⊗ₜ[ℝ] cast ⋯ ((Lorentz.coBasis d) b2)) = if b1 = b2 then 1 else 0
    simp only [cast_eq]«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ Lorentz.contrCoContract ((Lorentz.contrBasis d) b1 ⊗ₜ[ℝ] (Lorentz.coBasis d) b2) = if b1 = b2 then 1 else 0
    erw [Lorentz.contrCoContract_basis«0»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.up = (realLorentzTensor d).τ Color.up⊢ (if b1 = b2 then 1 else 0) = if b1 = b2 then 1 else 0]All goals completed! 🐙
  ·«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ ((realLorentzTensor d).contr Color.down)
    ((match Color.down with
        | Color.up => Lorentz.contrBasis d
        | Color.down => Lorentz.coBasis d)
        b1 ⊗ₜ[ℝ]
      (LinearEquiv.cast ⋯)
        ((match (realLorentzTensor d).τ Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)
          b2)) =
  if b1 = b2 then 1 else 0 simp [realLorentzTensor]«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ Lorentz.coContrContract ((Lorentz.coBasis d) b1 ⊗ₜ[ℝ] (LinearEquiv.cast ⋯) ((Lorentz.contrBasis d) b2)) =
  if b1 = b2 then 1 else 0
    erw [LinearEquiv.cast_apply«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ Lorentz.coContrContract ((Lorentz.coBasis d) b1 ⊗ₜ[ℝ] cast ⋯ ((Lorentz.contrBasis d) b2)) = if b1 = b2 then 1 else 0]«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ Lorentz.coContrContract ((Lorentz.coBasis d) b1 ⊗ₜ[ℝ] cast ⋯ ((Lorentz.contrBasis d) b2)) = if b1 = b2 then 1 else 0
    simp only [cast_eq]«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ Lorentz.coContrContract ((Lorentz.coBasis d) b1 ⊗ₜ[ℝ] (Lorentz.contrBasis d) b2) = if b1 = b2 then 1 else 0
    erw [Lorentz.coContrContract_basis«1»d:ℕn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b1:Fin 1 ⊕ Fin db2:Fin 1 ⊕ Fin dhij:i ≠ j ∧ (realLorentzTensor d).τ Color.down = (realLorentzTensor d).τ Color.down⊢ (if b1 = b2 then 1 else 0) = if b1 = b2 then 1 else 0]All goals completed! 🐙

lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n + 1 + 1))
    (h : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (t : ℝT(d, c)) :
    contrT n i j h t = ∑ (μ : Fin 1 ⊕ Fin d), permT id (byn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jt:(realLorentzTensor d).Tensor cμ:Fin 1 ⊕ Fin d⊢ IsReindexing ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove) (c ∘ i.succSuccAbove j) id
      simp [Fin.succSuccAbove_eq_predAbove h.1]All goals completed! 🐙)
      (evalT ((Fin.predAbove 0 i).predAbove j) μ (evalT i μ t)) := byn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jt:(realLorentzTensor d).Tensor c⊢ (contrT n i j h) t = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t))
  induction' t using Tensor.induction_on_basis with b r t h t1 t2 h1 h2hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ (contrT n i j h) ((basis c) b) =
  ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b)))hzeron:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j⊢ (contrT n i j h) 0 = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) 0))hsmuln:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h✝:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jr:ℝt:(realLorentzTensor d).Tensor ch:(contrT n i j h✝) t = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t))⊢ (contrT n i j h✝) (r • t) = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) (r • t)))haddn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jt1:(realLorentzTensor d).Tensor ct2:(realLorentzTensor d).Tensor ch1:(contrT n i j h) t1 = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t1))h2:(contrT n i j h) t2 = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t2))⊢ (contrT n i j h) (t1 + t2) = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) (t1 + t2)))
  ·hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ (contrT n i j h) ((basis c) b) =
  ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b))) rw [contrT_basishn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ Pure.contrPCoeff i j h (Pure.basisVector c b) • (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b)))hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ Pure.contrPCoeff i j h (Pure.basisVector c b) • (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b)))]hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ Pure.contrPCoeff i j h (Pure.basisVector c b) • (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b)))
    simp only [contrPCoeff_basis, ite_smul, one_smul, zero_smul]hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b)))
    conv_rhs =>
      enter [2, μ]n:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx cμ:Fin 1 ⊕ Fin d| (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) ((basis c) b)));
      simp only [evalT_basis, Fin.zero_succAbove, apply_ite, Fin.succ_zero_eq_one, map_zero]n:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx cμ:Fin 1 ⊕ Fin d| if b i = μ then
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = μ then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
else 0
    simp only [Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx c⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
    have h0 : i.succAbove ((Fin.predAbove 0 i).predAbove j) = j := byn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jt:(realLorentzTensor d).Tensor c⊢ (contrT n i j h) t = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t))hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
      rcases i.eq_zero_or_eq_succ with rfl | ⟨k, rfl⟩inln:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ch:0 ≠ j ∧ (realLorentzTensor d).τ (c 0) = c j⊢ Fin.succAbove 0 ((Fin.predAbove 0 0).predAbove j) = jinrn:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ck:Fin (n + 1)h:k.succ ≠ j ∧ (realLorentzTensor d).τ (c k.succ) = c j⊢ k.succ.succAbove ((Fin.predAbove 0 k.succ).predAbove j) = jhn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
      ·inln:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ch:0 ≠ j ∧ (realLorentzTensor d).τ (c 0) = c j⊢ Fin.succAbove 0 ((Fin.predAbove 0 0).predAbove j) = jhn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0 exact Fin.succAbove_predAbove (Ne.symm h.1)All goals completed! 🐙hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
      ·inrn:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ck:Fin (n + 1)h:k.succ ≠ j ∧ (realLorentzTensor d).τ (c k.succ) = c j⊢ k.succ.succAbove ((Fin.predAbove 0 k.succ).predAbove j) = jhn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0 rw [Fin.predAbove_zero_succinrn:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ck:Fin (n + 1)h:k.succ ≠ j ∧ (realLorentzTensor d).τ (c k.succ) = c j⊢ k.succ.succAbove (k.predAbove j) = jinrn:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ck:Fin (n + 1)h:k.succ ≠ j ∧ (realLorentzTensor d).τ (c k.succ) = c j⊢ k.succ.succAbove (k.predAbove j) = jhn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0]inrn:ℕd:ℕc:Fin (n + 1 + 1) → Colorj:Fin (n + 1 + 1)b:ComponentIdx ck:Fin (n + 1)h:k.succ ≠ j ∧ (realLorentzTensor d).τ (c k.succ) = c j⊢ k.succ.succAbove (k.predAbove j) = jhn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
        exact Fin.succ_succAbove_predAbove (Ne.symm h.1)hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b (i.succAbove ((Fin.predAbove 0 i).predAbove j)) = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
    rw [h0hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b j = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b j = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0]hn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = j⊢ (if b i = b j then (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) else 0) =
  if b j = b i then
    (permT id ⋯)
      ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
        b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))
  else 0
    split_ifs with h₁ _ h₂posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  (permT id ⋯)
    ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
      b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))negn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:¬b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) = 0posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:¬b i = b jh₂:b j = b i⊢ 0 =
  (permT id ⋯)
    ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
      b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1)))negn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:¬b i = b jh₂:¬b j = b i⊢ 0 = 0
    ·posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  (permT id ⋯)
    ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
      b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1))) rw [permT_basisposn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  (basis (c ∘ i.succSuccAbove j)) fun i_1 =>
    (basisIdxCongr ⋯) (b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove (id i_1))))posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  (basis (c ∘ i.succSuccAbove j)) fun i_1 =>
    (basisIdxCongr ⋯) (b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove (id i_1))))]posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) =
  (basis (c ∘ i.succSuccAbove j)) fun i_1 =>
    (basisIdxCongr ⋯) (b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove (id i_1))))
      congrpos.e_6n:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b i⊢ ComponentIdx.dropPair i j b = fun i_1 =>
  (basisIdxCongr ⋯) (b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove (id i_1))))
      ext xpos.e_6n:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b ix:Fin n⊢ ComponentIdx.dropPair i j b x = (basisIdxCongr ⋯) (b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove (id x))))
      simp only [Function.comp_apply, ComponentIdx.dropPair, id_eq, basisIdxCongr_eq_refl,
        Equiv.refl_apply]pos.e_6n:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b ix:Fin n⊢ b (i.succSuccAbove j x) = b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove x))
      rw [Fin.succSuccAbove_eq_predAbove h.1pos.e_6n:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:b j = b ix:Fin n⊢ b ((fun x => i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove x)) x) =
  b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove x))All goals completed! 🐙]All goals completed! 🐙
    ·negn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b i = b j_:¬b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) = 0 symm at h₁negn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:b j = b i_:¬b j = b i⊢ (basis (c ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j b) = 0; contradictionAll goals completed! 🐙
    ·posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:¬b i = b jh₂:b j = b i⊢ 0 =
  (permT id ⋯)
    ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
      b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1))) symm at h₂posn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:¬b i = b jh₂:b i = b j⊢ 0 =
  (permT id ⋯)
    ((basis ((c ∘ i.succAbove) ∘ ((Fin.predAbove 0 i).predAbove j).succAbove)) fun j_1 =>
      b (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove j_1))); contradictionAll goals completed! 🐙
    ·negn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jb:ComponentIdx ch0:i.succAbove ((Fin.predAbove 0 i).predAbove j) = jh₁:¬b i = b jh₂:¬b j = b i⊢ 0 = 0 rflAll goals completed! 🐙
  ·hzeron:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j⊢ (contrT n i j h) 0 = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) 0)) simpAll goals completed! 🐙
  ·hsmuln:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h✝:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jr:ℝt:(realLorentzTensor d).Tensor ch:(contrT n i j h✝) t = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t))⊢ (contrT n i j h✝) (r • t) = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) (r • t))) simp [Finset.smul_sum, h]All goals completed! 🐙
  ·haddn:ℕd:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ (realLorentzTensor d).τ (c i) = c jt1:(realLorentzTensor d).Tensor ct2:(realLorentzTensor d).Tensor ch1:(contrT n i j h) t1 = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t1))h2:(contrT n i j h) t2 = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) t2))⊢ (contrT n i j h) (t1 + t2) = ∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 i).predAbove j) μ) ((evalT i μ) (t1 + t2))) simp [h1, h2, Finset.sum_add_distrib]All goals completed! 🐙

lemma contrT_toField {d} (c : Fin 2 → Color)
    (h : 0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1) (t : ℝT(d, c)) :
    (contrT 0 0 1 h t).toField = ∑ (μ : Fin 1 ⊕ Fin d), {t | [μ] [μ]}ᵀ.toField := byd:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ toField ((contrT 0 0 1 h) t) = ∑ μ, toField ((evalT 0 μ) ((evalT 0 μ) t))
  rw [contrT_eq_sum_evalT,d:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ toField (∑ μ, (permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) μ) ((evalT 0 μ) t))) =
  ∑ μ, toField ((evalT 0 μ) ((evalT 0 μ) t))d:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ ∑ x, toField ((permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) x) ((evalT 0 x) t))) =
  ∑ μ, toField ((evalT 0 μ) ((evalT 0 μ) t)) map_sumd:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ ∑ x, toField ((permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) x) ((evalT 0 x) t))) =
  ∑ μ, toField ((evalT 0 μ) ((evalT 0 μ) t))d:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ ∑ x, toField ((permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) x) ((evalT 0 x) t))) =
  ∑ μ, toField ((evalT 0 μ) ((evalT 0 μ) t))]d:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ ∑ x, toField ((permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) x) ((evalT 0 x) t))) =
  ∑ μ, toField ((evalT 0 μ) ((evalT 0 μ) t))
  congre_fd:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor c⊢ (fun x => toField ((permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) x) ((evalT 0 x) t)))) = fun μ =>
  toField ((evalT 0 μ) ((evalT 0 μ) t))
  ext μe_fd:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor cμ:Fin 1 ⊕ Fin d⊢ toField ((permT id ⋯) ((evalT ((Fin.predAbove 0 0).predAbove 1) μ) ((evalT 0 μ) t))) =
  toField ((evalT 0 μ) ((evalT 0 μ) t))
  simp only [toField_permT]e_fd:ℕc:Fin 2 → Colorh:0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1t:(realLorentzTensor d).Tensor cμ:Fin 1 ⊕ Fin d⊢ toField ((evalT ((Fin.predAbove 0 0).predAbove 1) μ) ((evalT 0 μ) t)) = toField ((evalT 0 μ) ((evalT 0 μ) t))
  rflAll goals completed! 🐙