Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder

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.QFT.PerturbationTheory.FieldSpecification.TimeOrder
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute

Time Ordering in the FieldOpFreeAlgebra

@[expose] public section

Time order

For a field specification 𝓕, timeOrderF is the linear map

FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕

defined by its action on the basis ofCrAnListF φs, taking ofCrAnListF φs to

crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs).

That is, timeOrderF time-orders the field operators and multiplies by the sign of the time order.

The notation 𝓣ᶠ(a) is used for timeOrderF a

def timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
  Basis.constr ofCrAnListFBasis ℂ fun φs =>
  crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)

              @[inherit_doc timeOrderF]
scoped[FieldSpecification.FieldOpFreeAlgebra] notation "𝓣ᶠ(" a ")" => timeOrderF a

lemma timeOrderF_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) :
    𝓣ᶠ(ofCrAnListF φs) = crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs) := by𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListF φs) = crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)
  rw [← ofListBasis_eq_ofList𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListFBasis φs) = crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListFBasis φs) = crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)]𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListFBasis φs) = crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)
  simp only [timeOrderF, Basis.constr_basis]All goals completed! 🐙

lemma timeOrderF_timeOrderF_mid (a b c : 𝓕.FieldOpFreeAlgebra) :
    𝓣ᶠ(a * b * c) = 𝓣ᶠ(a * 𝓣ᶠ(b) * c) := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)
  let pc (c : 𝓕.FieldOpFreeAlgebra) (hc : c ∈ Submodule.span ℂ (Set.range ofCrAnListFBasis)) :
    Prop := 𝓣ᶠ(a * b * c) = 𝓣ᶠ(a * 𝓣ᶠ(b) * c)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)
  change pc c (Basis.mem_span _ c)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ pc c ⋯
  apply Submodule.span_inductionmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pc x ⋯zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ pc 0 ⋯add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis))
  (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pc x hx → pc y hy → pc (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pc x hx → pc (a • x) ⋯
  ·mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pc x ⋯ intro x hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)x:𝓕.FieldOpFreeAlgebrahx:x ∈ Set.range ⇑ofCrAnListFBasis⊢ pc x ⋯
    obtain ⟨φs, rfl⟩ := hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOp⊢ pc (ofCrAnListFBasis φs) ⋯
    simp only [ofListBasis_eq_ofList, pc]mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOp⊢ timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)
    let pb (b : 𝓕.FieldOpFreeAlgebra) (hb : b ∈ Submodule.span ℂ (Set.range ofCrAnListFBasis)) :
      Prop := 𝓣ᶠ(a * b * ofCrAnListF φs) = 𝓣ᶠ(a * 𝓣ᶠ(b) * ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)
    change pb b (Basis.mem_span _ b)mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ pb b ⋯
    apply Submodule.span_inductionmem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pb x ⋯mem.zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ pb 0 ⋯add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis))
  (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb y hy → pb (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb (a • x) ⋯
    ·mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pb x ⋯ intro x hxmem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)x:𝓕.FieldOpFreeAlgebrahx:x ∈ Set.range ⇑ofCrAnListFBasis⊢ pb x ⋯
      obtain ⟨φs', rfl⟩ := hxmem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOp⊢ pb (ofCrAnListFBasis φs') ⋯
      simp only [ofListBasis_eq_ofList, pb]mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOp⊢ timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)
      let pa (a : 𝓕.FieldOpFreeAlgebra) (ha : a ∈ Submodule.span ℂ (Set.range ofCrAnListFBasis)) :
        Prop := 𝓣ᶠ(a * ofCrAnListF φs' * ofCrAnListF φs) =
          𝓣ᶠ(a * 𝓣ᶠ(ofCrAnListF φs') * ofCrAnListF φs)mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)
      change pa a (Basis.mem_span _ a)mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ pa a ⋯
      apply Submodule.span_inductionmem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pa x ⋯mem.mem.zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ pa 0 ⋯add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis))
  (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa y hy → pa (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa (a • x) ⋯
      ·mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pa x ⋯ intro x hxmem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)x:𝓕.FieldOpFreeAlgebrahx:x ∈ Set.range ⇑ofCrAnListFBasis⊢ pa x ⋯
        obtain ⟨φs'', rfl⟩ := hxmem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ pa (ofCrAnListFBasis φs'') ⋯
        simp only [ofListBasis_eq_ofList, pa]mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListF φs'' * ofCrAnListF φs' * ofCrAnListF φs) =
  timeOrderF (ofCrAnListF φs'' * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)
        rw [timeOrderF_ofCrAnListFmem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListF φs'' * ofCrAnListF φs' * ofCrAnListF φs) =
  timeOrderF (ofCrAnListF φs'' * crAnTimeOrderSign φs' • ofCrAnListF (crAnTimeOrderList φs') * ofCrAnListF φs)mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListF φs'' * ofCrAnListF φs' * ofCrAnListF φs) =
  timeOrderF (ofCrAnListF φs'' * crAnTimeOrderSign φs' • ofCrAnListF (crAnTimeOrderList φs') * ofCrAnListF φs)]mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListF φs'' * ofCrAnListF φs' * ofCrAnListF φs) =
  timeOrderF (ofCrAnListF φs'' * crAnTimeOrderSign φs' • ofCrAnListF (crAnTimeOrderList φs') * ofCrAnListF φs)
        simp only [← ofCrAnListF_append, Algebra.mul_smul_comm,
          Algebra.smul_mul_assoc, map_smul]mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ timeOrderF (ofCrAnListF (φs'' ++ φs' ++ φs)) =
  crAnTimeOrderSign φs' • timeOrderF (ofCrAnListF (φs'' ++ crAnTimeOrderList φs' ++ φs))
        rw [timeOrderF_ofCrAnListF,mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  crAnTimeOrderSign φs' • timeOrderF (ofCrAnListF (φs'' ++ crAnTimeOrderList φs' ++ φs))mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  (crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs)) •
    ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs)) timeOrderF_ofCrAnListF,mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  crAnTimeOrderSign φs' •
    crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs) •
      ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs))mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  (crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs)) •
    ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs)) smul_smulmem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  (crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs)) •
    ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs))mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  (crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs)) •
    ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs))]mem.mem.mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  (crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs)) •
    ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs))
        congr 1mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) = crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs)mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs))
        ·mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderSign (φs'' ++ φs' ++ φs) = crAnTimeOrderSign φs' * crAnTimeOrderSign (φs'' ++ crAnTimeOrderList φs' ++ φs) simp only [crAnTimeOrderSign, crAnTimeOrderList]mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel (φs'' ++ φs' ++ φs) =
  Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel φs' *
    Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel (φs'' ++ List.insertionSort crAnTimeOrderRel φs' ++ φs)
          rw [Wick.koszulSign_of_append_eq_insertionSort,mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel (φs'' ++ List.insertionSort crAnTimeOrderRel φs' ++ φs) *
    Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel φs' =
  Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel φs' *
    Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel (φs'' ++ List.insertionSort crAnTimeOrderRel φs' ++ φs)All goals completed! 🐙 mul_commmem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel φs' *
    Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel (φs'' ++ List.insertionSort crAnTimeOrderRel φs' ++ φs) =
  Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel φs' *
    Wick.koszulSign 𝓕.crAnStatistics crAnTimeOrderRel (φs'' ++ List.insertionSort crAnTimeOrderRel φs' ++ φs)All goals completed! 🐙]All goals completed! 🐙
        ·mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ ofCrAnListF (crAnTimeOrderList (φs'' ++ φs' ++ φs)) =
  ofCrAnListF (crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs)) congr 1mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ crAnTimeOrderList (φs'' ++ φs' ++ φs) = crAnTimeOrderList (φs'' ++ crAnTimeOrderList φs' ++ φs)
          simp only [crAnTimeOrderList]mem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ List.insertionSort crAnTimeOrderRel (φs'' ++ φs' ++ φs) =
  List.insertionSort crAnTimeOrderRel (φs'' ++ List.insertionSort crAnTimeOrderRel φs' ++ φs)
          rw [insertionSort_append_insertionSort_appendmem.mem.mem.e_a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)φs'':List 𝓕.CrAnFieldOp⊢ List.insertionSort crAnTimeOrderRel (φs'' ++ φs' ++ φs) = List.insertionSort crAnTimeOrderRel (φs'' ++ φs' ++ φs)All goals completed! 🐙]All goals completed! 🐙
      ·mem.mem.zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ pa 0 ⋯ simp [pa]All goals completed! 🐙
      ·add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis))
  (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa y hy → pa (x + y) ⋯ intro x y hx hy h1 h2add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)h1:pa x hxh2:pa y hy⊢ pa (x + y) ⋯
        simp_all [pa, add_mul]All goals completed! 🐙
      ·smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa (a • x) ⋯ intro x hx hsmul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := 
  fun a ha =>
    timeOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = timeOrderF (a * timeOrderF (ofCrAnListF φs') * ofCrAnListF φs)x:ℂhx:𝓕.FieldOpFreeAlgebrah:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)⊢ pa hx h → pa (x • hx) ⋯
        simp_all [pa]All goals completed! 🐙
    ·mem.zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ pb 0 ⋯ simp [pb]All goals completed! 🐙
    ·add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis))
  (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb y hy → pb (x + y) ⋯ intro x y hx hy h1 h2add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)h1:pb x hxh2:pb y hy⊢ pb (x + y) ⋯
      simp_all [pb, mul_add, add_mul]All goals completed! 🐙
    ·smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb (a • x) ⋯ intro x hx hsmul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hb => timeOrderF (a * b * ofCrAnListF φs) = timeOrderF (a * timeOrderF b * ofCrAnListF φs)x:ℂhx:𝓕.FieldOpFreeAlgebrah:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)⊢ pb hx h → pb (x • hx) ⋯
      simp_all [pb]All goals completed! 🐙
  ·zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ pc 0 ⋯ simp [pc]All goals completed! 🐙
  ·add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis))
  (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pc x hx → pc y hy → pc (x + y) ⋯ intro x y hx hy h1 h2add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)h1:pc x hxh2:pc y hy⊢ pc (x + y) ⋯
    simp_all [pc, mul_add]All goals completed! 🐙
  ·smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pc x hx → pc (a • x) ⋯ intro x hx h hpsmul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) → c ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun c hc => timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)x:ℂhx:𝓕.FieldOpFreeAlgebrah:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hp:pc hx h⊢ pc (x • hx) ⋯
    simp_all [pc]All goals completed! 🐙

lemma timeOrderF_timeOrderF_right (a b : 𝓕.FieldOpFreeAlgebra) : 𝓣ᶠ(a * b) = 𝓣ᶠ(a * 𝓣ᶠ(b)) := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b) = timeOrderF (a * timeOrderF b)
  trans 𝓣ᶠ(a * b * 1)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b) = timeOrderF (a * b * 1)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b * 1) = timeOrderF (a * timeOrderF b)
  ·𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b) = timeOrderF (a * b * 1) simpAll goals completed! 🐙
  ·𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b * 1) = timeOrderF (a * timeOrderF b) rw [timeOrderF_timeOrderF_mid𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * timeOrderF b * 1) = timeOrderF (a * timeOrderF b)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * timeOrderF b * 1) = timeOrderF (a * timeOrderF b)]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * timeOrderF b * 1) = timeOrderF (a * timeOrderF b)
    simpAll goals completed! 🐙

lemma timeOrderF_timeOrderF_left (a b : 𝓕.FieldOpFreeAlgebra) : 𝓣ᶠ(a * b) = 𝓣ᶠ(𝓣ᶠ(a) * b) := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b) = timeOrderF (timeOrderF a * b)
  trans 𝓣ᶠ(1 * a * b)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b) = timeOrderF (1 * a * b)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (1 * a * b) = timeOrderF (timeOrderF a * b)
  ·𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * b) = timeOrderF (1 * a * b) simpAll goals completed! 🐙
  ·𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (1 * a * b) = timeOrderF (timeOrderF a * b) rw [timeOrderF_timeOrderF_mid𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (1 * timeOrderF a * b) = timeOrderF (timeOrderF a * b)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (1 * timeOrderF a * b) = timeOrderF (timeOrderF a * b)]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (1 * timeOrderF a * b) = timeOrderF (timeOrderF a * b)
    simpAll goals completed! 🐙

lemma timeOrderF_ofFieldOpListF (φs : List 𝓕.FieldOp) :
    𝓣ᶠ(ofFieldOpListF φs) = timeOrderSign φs • ofFieldOpListF (timeOrderList φs) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ timeOrderF (ofFieldOpListF φs) = timeOrderSign φs • ofFieldOpListF (timeOrderList φs)
  conv_lhs =>
    rw [ofFieldOpListF_sum, map_sum]𝓕:FieldSpecificationφs:List 𝓕.FieldOp| ∑ x, timeOrderF (ofCrAnListF ↑x)
    enter [2, x]𝓕:FieldSpecificationφs:List 𝓕.FieldOpx:CrAnSection φs| timeOrderF (ofCrAnListF ↑x)
    rw [timeOrderF_ofCrAnListF]𝓕:FieldSpecificationφs:List 𝓕.FieldOpx:CrAnSection φs| crAnTimeOrderSign ↑x • ofCrAnListF (crAnTimeOrderList ↑x)
  simp only [crAnTimeOrderSign_crAnSection]𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, timeOrderSign φs • ofCrAnListF (crAnTimeOrderList ↑x) = timeOrderSign φs • ofFieldOpListF (timeOrderList φs)
  rw [← Finset.smul_sum𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ timeOrderSign φs • ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = timeOrderSign φs • ofFieldOpListF (timeOrderList φs)𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ timeOrderSign φs • ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = timeOrderSign φs • ofFieldOpListF (timeOrderList φs)]𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ timeOrderSign φs • ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = timeOrderSign φs • ofFieldOpListF (timeOrderList φs)
  congre_a𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = ofFieldOpListF (timeOrderList φs)
  rw [ofFieldOpListF_sum,e_a𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = ∑ s, ofCrAnListF ↑se_a𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = ∑ s, ofCrAnListF ↑(crAnSectionTimeOrder φs s) sum_crAnSections_timeOrdere_a𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = ∑ s, ofCrAnListF ↑(crAnSectionTimeOrder φs s)e_a𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = ∑ s, ofCrAnListF ↑(crAnSectionTimeOrder φs s)]e_a𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ x, ofCrAnListF (crAnTimeOrderList ↑x) = ∑ s, ofCrAnListF ↑(crAnSectionTimeOrder φs s)
  rflAll goals completed! 🐙

lemma timeOrderF_ofFieldOpListF_nil : timeOrderF (𝓕 := 𝓕) (ofFieldOpListF []) = 1 := by𝓕:FieldSpecification⊢ timeOrderF (ofFieldOpListF []) = 1
  rw [timeOrderF_ofFieldOpListF𝓕:FieldSpecification⊢ timeOrderSign [] • ofFieldOpListF (timeOrderList []) = 1𝓕:FieldSpecification⊢ timeOrderSign [] • ofFieldOpListF (timeOrderList []) = 1]𝓕:FieldSpecification⊢ timeOrderSign [] • ofFieldOpListF (timeOrderList []) = 1
  simp [timeOrderSign, Wick.koszulSign, timeOrderList]All goals completed! 🐙@[simp]
lemma timeOrderF_ofFieldOpListF_singleton (φ : 𝓕.FieldOp) :
    𝓣ᶠ(ofFieldOpListF [φ]) = ofFieldOpListF [φ] := by𝓕:FieldSpecificationφ:𝓕.FieldOp⊢ timeOrderF (ofFieldOpListF [φ]) = ofFieldOpListF [φ]
  simp [timeOrderF_ofFieldOpListF, timeOrderSign, timeOrderList]All goals completed! 🐙

lemma timeOrderF_ofFieldOpF_ofFieldOpF_ordered {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) :
    𝓣ᶠ(ofFieldOpF φ * ofFieldOpF ψ) = ofFieldOpF φ * ofFieldOpF ψ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpF φ * ofFieldOpF ψ) = ofFieldOpF φ * ofFieldOpF ψ
  rw [← ofFieldOpListF_singleton,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpListF [φ] * ofFieldOpF ψ) = ofFieldOpListF [φ] * ofFieldOpF ψ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ]) ← ofFieldOpListF_singleton,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpListF [φ] * ofFieldOpListF [ψ]) = ofFieldOpListF [φ] * ofFieldOpListF [ψ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ]) ← ofFieldOpListF_append,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpListF ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ])𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ])
    timeOrderF_ofFieldOpListF𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ])𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ])]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) = ofFieldOpListF ([φ] ++ [ψ])
  simp only [List.singleton_append]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign [φ, ψ] • ofFieldOpListF (timeOrderList [φ, ψ]) = ofFieldOpListF [φ, ψ]
  rw [timeOrderSign_pair_ordered h,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ 1 • ofFieldOpListF (timeOrderList [φ, ψ]) = ofFieldOpListF [φ, ψ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ 1 • ofFieldOpListF [φ, ψ] = ofFieldOpListF [φ, ψ] timeOrderList_pair_ordered h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ 1 • ofFieldOpListF [φ, ψ] = ofFieldOpListF [φ, ψ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ 1 • ofFieldOpListF [φ, ψ] = ofFieldOpListF [φ, ψ]]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ 1 • ofFieldOpListF [φ, ψ] = ofFieldOpListF [φ, ψ]
  simpAll goals completed! 🐙

lemma timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered {φ ψ : 𝓕.FieldOp} (h : ¬ timeOrderRel φ ψ) :
    𝓣ᶠ(ofFieldOpF φ * ofFieldOpF ψ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • ofFieldOpF ψ * ofFieldOpF φ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpF φ * ofFieldOpF ψ) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ
  rw [← ofFieldOpListF_singleton,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpListF [φ] * ofFieldOpF ψ) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpListF [φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ] ← ofFieldOpListF_singleton,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpListF [φ] * ofFieldOpListF [ψ]) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ]
    ← ofFieldOpListF_append,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpListF ([φ] ++ [ψ])) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ] timeOrderF_ofFieldOpListF𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ]]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign ([φ] ++ [ψ]) • ofFieldOpListF (timeOrderList ([φ] ++ [ψ])) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ] * ofFieldOpListF [φ]
  simp only [List.singleton_append, Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign [φ, ψ] • ofFieldOpListF (timeOrderList [φ, ψ]) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpListF [ψ] * ofFieldOpListF [φ])
  rw [timeOrderSign_pair_not_ordered h,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF (timeOrderList [φ, ψ]) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpListF [ψ] * ofFieldOpListF [φ])𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ, φ] =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpListF [ψ] * ofFieldOpListF [φ]) timeOrderList_pair_not_ordered h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ, φ] =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpListF [ψ] * ofFieldOpListF [φ])𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ, φ] =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpListF [ψ] * ofFieldOpListF [φ])]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpListF [ψ, φ] =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpListF [ψ] * ofFieldOpListF [φ])
  simp [← ofFieldOpListF_append]All goals completed! 🐙

lemma timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF {φ ψ : 𝓕.FieldOp}
    (h : ¬ timeOrderRel φ ψ) :
    𝓣ᶠ(ofFieldOpF φ * ofFieldOpF ψ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • 𝓣ᶠ(ofFieldOpF ψ * ofFieldOpF φ) := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderF (ofFieldOpF φ * ofFieldOpF ψ) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrderF (ofFieldOpF ψ * ofFieldOpF φ)
  rw [timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrderF (ofFieldOpF ψ * ofFieldOpF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrderF (ofFieldOpF ψ * ofFieldOpF φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrderF (ofFieldOpF ψ * ofFieldOpF φ)
  rw [timeOrderF_ofFieldOpF_ofFieldOpF_ordered𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpF ψ * ofFieldOpF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpF ψ * ofFieldOpF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (ofFieldOpF ψ * ofFieldOpF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
  simp only [Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
  have hx := Std.Total.total (r := timeOrderRel) ψ φ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψhx:timeOrderRel ψ φ ∨ timeOrderRel φ ψ⊢ timeOrderRel ψ φ
  simp_allAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel
    {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) :
    𝓣ᶠ([ofCrAnOpF φ, ofCrAnOpF ψ]ₛF) = 0 := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0
  rw [superCommuteF_ofCrAnOpF_ofCrAnOpF𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF
    (ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF
    (ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ) =
  0]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF
    (ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ) =
  0
  simp only [Algebra.smul_mul_assoc, map_sub, map_smul]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF (ofCrAnOpF φ * ofCrAnOpF ψ) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnOpF ψ * ofCrAnOpF φ) =
  0
  rw [← ofCrAnListF_singleton,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF (ofCrAnListF [φ] * ofCrAnOpF ψ) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnOpF ψ * ofCrAnListF [φ]) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0 ← ofCrAnListF_singleton,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF (ofCrAnListF [φ] * ofCrAnListF [ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF [ψ] * ofCrAnListF [φ]) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0
    ← ofCrAnListF_append,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF (ofCrAnListF ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF [ψ] * ofCrAnListF [φ]) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0 ← ofCrAnListF_append,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ timeOrderF (ofCrAnListF ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF ([ψ] ++ [φ])) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0 timeOrderF_ofCrAnListF,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF ([ψ] ++ [φ])) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0 timeOrderF_ofCrAnListF𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  0
  simp only [List.singleton_append]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign [φ, ψ] • ofCrAnListF (crAnTimeOrderList [φ, ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  0
  rw [crAnTimeOrderSign_pair_not_ordered h,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF (crAnTimeOrderList [φ, ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  0 crAnTimeOrderList_pair_not_ordered h𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  0]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  0
  rw [sub_eq_zero,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] =
  (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
    crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] =
  ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ]) •
    ofCrAnListF (crAnTimeOrderList [ψ, φ]) smul_smul𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] =
  ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ]) •
    ofCrAnListF (crAnTimeOrderList [ψ, φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] =
  ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ]) •
    ofCrAnListF (crAnTimeOrderList [ψ, φ])]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] =
  ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ]) •
    ofCrAnListF (crAnTimeOrderList [ψ, φ])
  have h1 := Std.Total.total (r := crAnTimeOrderRel) φ ψ𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] =
  ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ]) •
    ofCrAnListF (crAnTimeOrderList [ψ, φ])
  congre_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) =
  (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ]e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ [ψ, φ] = crAnTimeOrderList [ψ, φ]
  ·e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) =
  (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * crAnTimeOrderSign [ψ, φ] rw [crAnTimeOrderSign_pair_ordered,e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) = (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) * 1e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φe_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) = (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) * 1e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φ exchangeSign_symme_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) = (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) * 1e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φe_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) = (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) * 1e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φ]e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) = (exchangeSign (𝓕.crAnStatistics ψ)) (𝓕.crAnStatistics φ) * 1e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φ
    simp only [mul_one]e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φ
    simp_allAll goals completed! 🐙
  ·e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ [ψ, φ] = crAnTimeOrderList [ψ, φ] rw [crAnTimeOrderList_pair_orderede_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ [ψ, φ] = [ψ, φ]e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φe_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φ]e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψh1:crAnTimeOrderRel φ ψ ∨ crAnTimeOrderRel ψ φ⊢ crAnTimeOrderRel ψ φ
    simp_allAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right
    {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) (a : 𝓕.FieldOpFreeAlgebra) :
    𝓣ᶠ(a * [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF) = 0 := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0
  rw [timeOrderF_timeOrderF_right,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ))) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0) = 0
    timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel h𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0) = 0]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0) = 0
  simpAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left
    {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) (a : 𝓕.FieldOpFreeAlgebra) :
    𝓣ᶠ([ofCrAnOpF φ, ofCrAnOpF ψ]ₛF * a) = 0 := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * a) = 0
  rw [timeOrderF_timeOrderF_left,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * a) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (0 * a) = 0
    timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel h𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (0 * a) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (0 * a) = 0]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (0 * a) = 0
  simpAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid
    {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) (a b : 𝓕.FieldOpFreeAlgebra) :
    𝓣ᶠ(a * [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF * b) = 0 := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b) = 0
  rw [timeOrderF_timeOrderF_mid,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * b) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0 * b) = 0
    timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel h𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0 * b) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0 * b) = 0]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (a * 0 * b) = 0
  simpAll goals completed! 🐙

lemma timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel
    {φ1 φ2 : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ1 φ2) (a : 𝓕.FieldOpFreeAlgebra) :
    𝓣ᶠ([a, [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF]ₛF) = 0 := by𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF a) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) = 0
  rw [← bosonicProjF_add_fermionicProjF a𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF (↑(bosonicProjF a) + ↑(fermionicProjF a))) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF (↑(bosonicProjF a) + ↑(fermionicProjF a))) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF (↑(bosonicProjF a) + ↑(fermionicProjF a))) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0
  simp only [map_add, LinearMap.add_apply]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(bosonicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0
  rw [bosonic_superCommuteF (Submodule.coe_mem (bosonicProjF a))𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF
      (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) -
        (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * ↑(bosonicProjF a)) +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF
      (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) -
        (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * ↑(bosonicProjF a)) +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF
      (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) -
        (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * ↑(bosonicProjF a)) +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0
  simp only [map_sub]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) -
      timeOrderF ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * ↑(bosonicProjF a)) +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0
  rw [timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left h𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - 0 +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - 0 +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF (↑(bosonicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - 0 +
    timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) =
  0
  rw [timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right h𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ 0 - 0 + timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ 0 - 0 + timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) = 0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ 0 - 0 + timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) = 0
  simp only [sub_self, zero_add]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) = 0
  rw [← ofCrAnListF_singleton,𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnOpF φ2))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0 ← ofCrAnListF_singleton𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebra⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0
  rcases superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic [φ1] [φ2] with h' | h'inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0
  ·inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0 rw [superCommuteF_bonsonic h'inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF
    (↑(fermionicProjF a) * (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) -
      (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) * ↑(fermionicProjF a)) =
  0inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF
    (↑(fermionicProjF a) * (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) -
      (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) * ↑(fermionicProjF a)) =
  0]inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF
    (↑(fermionicProjF a) * (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) -
      (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) * ↑(fermionicProjF a)) =
  0
    simp only [ofCrAnListF_singleton, map_sub]inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) -
    timeOrderF ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * ↑(fermionicProjF a)) =
  0
    rw [timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left hinl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - 0 = 0inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - 0 = 0]inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - 0 = 0
    rw [timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right hinl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ 0 - 0 = 0inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ 0 - 0 = 0]inl𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule bosonic⊢ 0 - 0 = 0
    simpAll goals completed! 🐙
  ·inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF ((superCommuteF ↑(fermionicProjF a)) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0 rw [superCommuteF_fermionic_fermionic (Submodule.coe_mem (fermionicProjF a)) h'inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF
    (↑(fermionicProjF a) * (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) +
      (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) * ↑(fermionicProjF a)) =
  0inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF
    (↑(fermionicProjF a) * (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) +
      (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) * ↑(fermionicProjF a)) =
  0]inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF
    (↑(fermionicProjF a) * (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) +
      (superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) * ↑(fermionicProjF a)) =
  0
    simp only [ofCrAnListF_singleton, map_add]inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) +
    timeOrderF ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * ↑(fermionicProjF a)) =
  0
    rw [timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left hinr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) + 0 = 0inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) + 0 = 0]inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ timeOrderF (↑(fermionicProjF a) * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) + 0 = 0
    rw [timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right hinr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ 0 + 0 = 0inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ 0 + 0 = 0]inr𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ1 φ2a:𝓕.FieldOpFreeAlgebrah':(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ 0 + 0 = 0
    simpAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel
    {φ1 φ2 φ3 : 𝓕.CrAnFieldOp} (h12 : ¬ crAnTimeOrderRel φ1 φ2)
    (h13 : ¬ crAnTimeOrderRel φ1 φ3) :
    𝓣ᶠ([ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF) = 0 := by𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  rw [← ofCrAnListF_singleton,𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0 ← ofCrAnListF_singleton,𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnOpF φ3))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0 ← ofCrAnListF_singleton𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0
  rw [summerCommute_jacobi_ofCrAnListF𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3]) •
      (-(exchangeSign (ofList 𝓕.crAnStatistics [φ2])) (ofList 𝓕.crAnStatistics [φ3]) •
          (superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2])) -
        (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2]) •
          (superCommuteF (ofCrAnListF [φ2])) ((superCommuteF (ofCrAnListF [φ3])) (ofCrAnListF [φ1])))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3]) •
      (-(exchangeSign (ofList 𝓕.crAnStatistics [φ2])) (ofList 𝓕.crAnStatistics [φ3]) •
          (superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2])) -
        (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2]) •
          (superCommuteF (ofCrAnListF [φ2])) ((superCommuteF (ofCrAnListF [φ3])) (ofCrAnListF [φ1])))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3]) •
      (-(exchangeSign (ofList 𝓕.crAnStatistics [φ2])) (ofList 𝓕.crAnStatistics [φ3]) •
          (superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2])) -
        (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2]) •
          (superCommuteF (ofCrAnListF [φ2])) ((superCommuteF (ofCrAnListF [φ3])) (ofCrAnListF [φ1])))) =
  0
  simp only [ofList_singleton, ofCrAnListF_singleton, neg_smul, map_smul,
    map_sub, map_neg, smul_eq_zero]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ3) = 0 ∨
  -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
          timeOrderF ((superCommuteF (ofCrAnOpF φ3)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)))) -
      (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
        timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
    0
  right𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
        timeOrderF ((superCommuteF (ofCrAnOpF φ3)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)))) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0
  rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel h12𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • 0) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • 0) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • 0) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0
  rw [superCommuteF_ofCrAnOpF_ofCrAnOpF_symm φ3𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • 0) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF
        ((superCommuteF (ofCrAnOpF φ2))
          (-(exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) •
            (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ3))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • 0) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF
        ((superCommuteF (ofCrAnOpF φ2))
          (-(exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) •
            (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ3))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • 0) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF
        ((superCommuteF (ofCrAnOpF φ2))
          (-(exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) •
            (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ3))) =
  0
  simp only [smul_zero, neg_zero, neg_smul, map_neg, map_smul, smul_neg,
    sub_neg_eq_add, zero_add, smul_eq_zero]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨
  (exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) = 0 ∨
    timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ3))) = 0
  rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel h13𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨
  (exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) = 0 ∨ 0 = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨
  (exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) = 0 ∨ 0 = 0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨
  (exchangeSign (𝓕.crAnStatistics φ3)) (𝓕.crAnStatistics φ1) = 0 ∨ 0 = 0
  simpAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel'
    {φ1 φ2 φ3 : 𝓕.CrAnFieldOp} (h12 : ¬ crAnTimeOrderRel φ2 φ1)
    (h13 : ¬ crAnTimeOrderRel φ3 φ1) :
    𝓣ᶠ([ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF) = 0 := by𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  rw [← ofCrAnListF_singleton,𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0 ← ofCrAnListF_singleton,𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnOpF φ3))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0 ← ofCrAnListF_singleton𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnListF [φ1])) ((superCommuteF (ofCrAnListF [φ2])) (ofCrAnListF [φ3]))) = 0
  rw [summerCommute_jacobi_ofCrAnListF𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3]) •
      (-(exchangeSign (ofList 𝓕.crAnStatistics [φ2])) (ofList 𝓕.crAnStatistics [φ3]) •
          (superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2])) -
        (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2]) •
          (superCommuteF (ofCrAnListF [φ2])) ((superCommuteF (ofCrAnListF [φ3])) (ofCrAnListF [φ1])))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3]) •
      (-(exchangeSign (ofList 𝓕.crAnStatistics [φ2])) (ofList 𝓕.crAnStatistics [φ3]) •
          (superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2])) -
        (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2]) •
          (superCommuteF (ofCrAnListF [φ2])) ((superCommuteF (ofCrAnListF [φ3])) (ofCrAnListF [φ1])))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3]) •
      (-(exchangeSign (ofList 𝓕.crAnStatistics [φ2])) (ofList 𝓕.crAnStatistics [φ3]) •
          (superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2])) -
        (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2]) •
          (superCommuteF (ofCrAnListF [φ2])) ((superCommuteF (ofCrAnListF [φ3])) (ofCrAnListF [φ1])))) =
  0
  simp only [ofList_singleton, ofCrAnListF_singleton, neg_smul, map_smul,
    map_sub, map_neg, smul_eq_zero]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ3) = 0 ∨
  -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
          timeOrderF ((superCommuteF (ofCrAnOpF φ3)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)))) -
      (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
        timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
    0
  right𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
        timeOrderF ((superCommuteF (ofCrAnOpF φ3)) ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)))) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0
  rw [superCommuteF_ofCrAnOpF_ofCrAnOpF_symm φ1𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
        timeOrderF
          ((superCommuteF (ofCrAnOpF φ3))
            (-(exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
              (superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ1)))) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
        timeOrderF
          ((superCommuteF (ofCrAnOpF φ3))
            (-(exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
              (superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ1)))) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ -((exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
        timeOrderF
          ((superCommuteF (ofCrAnOpF φ3))
            (-(exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
              (superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ1)))) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0
  simp only [neg_smul, map_neg, map_smul, smul_neg, neg_neg]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
      (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
        timeOrderF ((superCommuteF (ofCrAnOpF φ3)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ1))) -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0
  rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel h12𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
      (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) • 0 -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
      (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) • 0 -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) •
      (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) • 0 -
    (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) •
      timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) =
  0
  simp only [smul_zero, zero_sub, neg_eq_zero, smul_eq_zero]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨
  timeOrderF ((superCommuteF (ofCrAnOpF φ2)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ1))) = 0
  rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel h13𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨ 0 = 0𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨ 0 = 0]𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph12:¬crAnTimeOrderRel φ2 φ1h13:¬crAnTimeOrderRel φ3 φ1⊢ (exchangeSign (𝓕.crAnStatistics φ1)) (𝓕.crAnStatistics φ2) = 0 ∨ 0 = 0
  simpAll goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel
    (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) (h : ¬
      (crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧
      crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧
      crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2)) :
    𝓣ᶠ([ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF) = 0 := by𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:¬(crAnTimeOrderRel φ1 φ2 ∧
    crAnTimeOrderRel φ1 φ3 ∧
      crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2)⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  simp only [not_and] at h𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 →
    crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ2 φ3 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  by_cases h23 : ¬ crAnTimeOrderRel φ2 φ3pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 →
    crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ2 φ3 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:¬crAnTimeOrderRel φ2 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 →
    crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ2 φ3 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:¬¬crAnTimeOrderRel φ2 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  ·pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 →
    crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ2 φ3 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:¬crAnTimeOrderRel φ2 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0 simp_all only [IsEmpty.forall_iff, implies_true]pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:¬crAnTimeOrderRel φ2 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
    rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel h23pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:¬crAnTimeOrderRel φ2 φ3⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙
  simp_all only [Decidable.not_not, forall_const]neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:crAnTimeOrderRel φ2 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  by_cases h32 : ¬ crAnTimeOrderRel φ3 φ2pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:crAnTimeOrderRel φ2 φ3h32:¬¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  ·pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 →
  crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → crAnTimeOrderRel φ3 φ1 → ¬crAnTimeOrderRel φ3 φ2h23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0 simp_all only [not_false_eq_true, implies_true]pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
    rw [superCommuteF_ofCrAnOpF_ofCrAnOpF_symmpos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF
    ((superCommuteF (ofCrAnOpF φ1))
      (-(exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • (superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ2))) =
  0pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF
    ((superCommuteF (ofCrAnOpF φ1))
      (-(exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • (superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ2))) =
  0]pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ timeOrderF
    ((superCommuteF (ofCrAnOpF φ1))
      (-(exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • (superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ2))) =
  0
    simp only [neg_smul, map_neg, map_smul, neg_eq_zero, smul_eq_zero]pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) = 0 ∨
  timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ3)) (ofCrAnOpF φ2))) = 0
    rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel h32pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) = 0 ∨ 0 = 0pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) = 0 ∨ 0 = 0]pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:¬crAnTimeOrderRel φ3 φ2⊢ (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) = 0 ∨ 0 = 0
    simpAll goals completed! 🐙
  simp_all only [imp_false, Decidable.not_not]neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  by_cases h12 : ¬ crAnTimeOrderRel φ1 φ2pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬¬crAnTimeOrderRel φ1 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  ·pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0 have h13 : ¬ crAnTimeOrderRel φ1 φ3 := by
      intro h13𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3⊢ Falsepos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
      apply h12𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3⊢ crAnTimeOrderRel φ1 φ2pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
      exact IsTrans.trans φ1 φ3 φ2 h13 h32pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
    rw [timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel h12 h13pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 → crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:¬crAnTimeOrderRel φ1 φ2h13:¬crAnTimeOrderRel φ1 φ3⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙
  simp_all only [Decidable.not_not, forall_const]neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  have h13 : crAnTimeOrderRel φ1 φ3 := IsTrans.trans φ1 φ2 φ3 h12 h23neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ3 → crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  simp_all only [forall_const]neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  by_cases h21 : ¬ crAnTimeOrderRel φ2 φ1pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬¬crAnTimeOrderRel φ2 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  ·pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:crAnTimeOrderRel φ2 φ1 → ¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0 simp_all only [IsEmpty.forall_iff]pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
    have h31 : ¬ crAnTimeOrderRel φ3 φ1 := by
      intro h31𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:crAnTimeOrderRel φ3 φ1⊢ Falsepos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
      apply h21𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:crAnTimeOrderRel φ3 φ1⊢ crAnTimeOrderRel φ2 φ1pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
      exact IsTrans.trans φ2 φ3 φ1 h23 h31pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:¬crAnTimeOrderRel φ3 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
    rw [timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel' h21 h31pos𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:¬crAnTimeOrderRel φ2 φ1h31:¬crAnTimeOrderRel φ3 φ1⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙
  simp_all only [Decidable.not_not, forall_const]neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:crAnTimeOrderRel φ2 φ1⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0
  refine False.elim (h ?_)neg𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ3 φ1h23:crAnTimeOrderRel φ2 φ3h32:crAnTimeOrderRel φ3 φ2h12:crAnTimeOrderRel φ1 φ2h13:crAnTimeOrderRel φ1 φ3h21:crAnTimeOrderRel φ2 φ1⊢ crAnTimeOrderRel φ3 φ1
  exact IsTrans.trans φ3 φ2 φ1 h32 h21All goals completed! 🐙

lemma timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time
    {φ ψ : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) :
    𝓣ᶠ([ofCrAnOpF φ, ofCrAnOpF ψ]ₛF) = [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)
  rw [superCommuteF_ofCrAnOpF_ofCrAnOpF𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF
    (ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ) =
  ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF
    (ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ) =
  ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF
    (ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ) =
  ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnOpF ψ * ofCrAnOpF φ
  simp only [Algebra.smul_mul_assoc, map_sub, map_smul]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF (ofCrAnOpF φ * ofCrAnOpF ψ) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnOpF ψ * ofCrAnOpF φ) =
  ofCrAnOpF φ * ofCrAnOpF ψ - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • (ofCrAnOpF ψ * ofCrAnOpF φ)
  rw [← ofCrAnListF_singleton,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF (ofCrAnListF [φ] * ofCrAnOpF ψ) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnOpF ψ * ofCrAnListF [φ]) =
  ofCrAnListF [φ] * ofCrAnOpF ψ -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • (ofCrAnOpF ψ * ofCrAnListF [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ]) ← ofCrAnListF_singleton,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF (ofCrAnListF [φ] * ofCrAnListF [ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF [ψ] * ofCrAnListF [φ]) =
  ofCrAnListF [φ] * ofCrAnListF [ψ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • (ofCrAnListF [ψ] * ofCrAnListF [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ])
    ← ofCrAnListF_append,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF (ofCrAnListF ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF [ψ] * ofCrAnListF [φ]) =
  ofCrAnListF ([φ] ++ [ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • (ofCrAnListF [ψ] * ofCrAnListF [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ]) ← ofCrAnListF_append,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ timeOrderF (ofCrAnListF ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ]) timeOrderF_ofCrAnListF,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • timeOrderF (ofCrAnListF ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ]) timeOrderF_ofCrAnListF𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ])]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign ([φ] ++ [ψ]) • ofCrAnListF (crAnTimeOrderList ([φ] ++ [ψ])) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign ([ψ] ++ [φ]) • ofCrAnListF (crAnTimeOrderList ([ψ] ++ [φ])) =
  ofCrAnListF ([φ] ++ [ψ]) - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF ([ψ] ++ [φ])
  simp only [List.singleton_append]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ crAnTimeOrderSign [φ, ψ] • ofCrAnListF (crAnTimeOrderList [φ, ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]
  rw [crAnTimeOrderSign_pair_ordered h1,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF (crAnTimeOrderList [φ, ψ]) -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF [ψ, φ] =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] crAnTimeOrderList_pair_ordered h1,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) •
      crAnTimeOrderSign [ψ, φ] • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF [ψ, φ] =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]
    crAnTimeOrderSign_pair_ordered h2,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] -
    (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF (crAnTimeOrderList [ψ, φ]) =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF [ψ, φ] =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ] crAnTimeOrderList_pair_ordered h2𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF [ψ, φ] =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF [ψ, φ] =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φ⊢ 1 • ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • 1 • ofCrAnListF [ψ, φ] =
  ofCrAnListF [φ, ψ] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • ofCrAnListF [ψ, φ]
  simpAll goals completed! 🐙

Interaction with maxTimeField

In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ) where φᵢ is the state which has maximum time and s is the exchange sign of φᵢ and φ₀φ₁…φᵢ₋₁.


lemma timeOrderF_eq_maxTimeField_mul (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
    𝓣ᶠ(ofFieldOpListF (φ :: φs)) =
    𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ (φ :: φs).take (maxTimeFieldPos φ φs)) •
    ofFieldOpF (maxTimeField φ φs) * 𝓣ᶠ(ofFieldOpListF (eraseMaxTimeField φ φs)) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderF (ofFieldOpListF (φ :: φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))
  rw [timeOrderF_ofFieldOpListF,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • ofFieldOpListF (timeOrderList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • ofFieldOpListF (maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs)) timeOrderList_eq_maxTimeField_timeOrderList𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • ofFieldOpListF (maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • ofFieldOpListF (maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • ofFieldOpListF (maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))
  rw [ofFieldOpListF_cons,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderSign (eraseMaxTimeField φ φs) • ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs)) timeOrderF_ofFieldOpListF𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderSign (eraseMaxTimeField φ φs) • ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderSign (eraseMaxTimeField φ φs) • ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderSign (eraseMaxTimeField φ φs) • ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))
  simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) • (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs))) =
  (timeOrderSign (eraseMaxTimeField φ φs) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs)))) •
    (ofFieldOpF (maxTimeField φ φs) * ofFieldOpListF (timeOrderList (eraseMaxTimeField φ φs)))
  congre_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) =
  timeOrderSign (eraseMaxTimeField φ φs) *
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs)))
  rw [timerOrderSign_of_eraseMaxTimeField,e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) =
  timeOrderSign (φ :: φs) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) *
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) =
  timeOrderSign (φ :: φs) *
    ((exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs)))) mul_assoce_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) =
  timeOrderSign (φ :: φs) *
    ((exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) =
  timeOrderSign (φ :: φs) *
    ((exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))))]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) =
  timeOrderSign (φ :: φs) *
    ((exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))))
  simpAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in


lemma timeOrderF_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
    𝓣ᶠ(ofFieldOpListF (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
      (Finset.filter (fun x =>
        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •
      ofFieldOpF (maxTimeField φ φs) * 𝓣ᶠ(ofFieldOpListF (eraseMaxTimeField φ φs)) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderF (ofFieldOpListF (φ :: φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))
  rw [timeOrderF_eq_maxTimeField_mul𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs)) =
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ofFieldOpF (maxTimeField φ φs) *
    timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))
  congr 3e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs)) =
  ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
    {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}
  apply FieldStatistic.ofList_perme_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (φ :: φs)).Perm
  (List.map (eraseMaxTimeField φ φs).get
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))
  nth_rewrite 1 [← List.map_get_finRange (φ :: φs)]e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (List.map (φ :: φs).get (List.finRange (φ :: φs).length))).Perm
  (List.map (eraseMaxTimeField φ φs).get
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))
  simp only [List.length_cons, eraseMaxTimeField, insertionSortDropMinPos]e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (List.map (φ :: φs).get (List.finRange (φs.length + 1)))).Perm
  (List.map ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).get
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))
  rw [eraseIdx_get,e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (List.map (φ :: φs).get (List.finRange (φs.length + 1)))).Perm
  (List.map ((φ :: φs).get ∘ Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (φ :: φs).get (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)))).Perm
  (List.map (φ :: φs).get
    (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
      ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))) ← List.map_take,e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (φ :: φs).get (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)))).Perm
  (List.map ((φ :: φs).get ∘ Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (φ :: φs).get (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)))).Perm
  (List.map (φ :: φs).get
    (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
      ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))) ← List.map_mape_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (φ :: φs).get (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)))).Perm
  (List.map (φ :: φs).get
    (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
      ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)))e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (φ :: φs).get (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)))).Perm
  (List.map (φ :: φs).get
    (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
      ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)))]e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (φ :: φs).get (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)))).Perm
  (List.map (φ :: φs).get
    (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
      ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)))
  refine List.Perm.map (φ :: φs).get ?_e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1))).Perm
  (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2))
  apply (List.perm_ext_iff_of_nodup _ _).mpre_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ∀ (a : Fin (φ :: φs).length),
  a ∈ List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)) ↔
    a ∈
      List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
        ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1))).Nodup𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)).Nodup
  ·e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ∀ (a : Fin (φ :: φs).length),
  a ∈ List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)) ↔
    a ∈
      List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
        ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2) intro ie_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).length⊢ i ∈ List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1)) ↔
  i ∈
    List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
      ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)
    simp only [List.length_cons, maxTimeFieldPos, mem_take_finrange, Fin.val_fin_lt, List.mem_map,
      Finset.mem_sort, Finset.mem_filter, Finset.mem_univ, true_and, Function.comp_apply]e_a.e_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).length⊢ i < insertionSortMinPos timeOrderRel φ φs ↔
  ∃ a,
    (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
      Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = i
    refine Iff.intro (fun hi => ?_) (fun h => ?_)e_a.e_a.e_6.refine_1𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φs⊢ ∃ a,
  (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
    Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = ie_a.e_a.e_6.refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthh:∃ a,
  (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
    Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = i⊢ i < insertionSortMinPos timeOrderRel φ φs
    ·e_a.e_a.e_6.refine_1𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φs⊢ ∃ a,
  (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
    Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = i have h2 := (maxTimeFieldPosFin φ φs).2e_a.e_a.e_6.refine_1𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(maxTimeFieldPosFin φ φs) < (eraseMaxTimeField φ φs).length.succ⊢ ∃ a,
  (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
    Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = i
      simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,
        maxTimeFieldPosFin, insertionSortMinPosFin] at h2e_a.e_a.e_6.refine_1𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ ∃ a,
  (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
    Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = i
      use ⟨i, by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ ↑i < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length omegaAll goals completed! 🐙⟩
      apply And.introh.left𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ (maxTimeFieldPosFin φ φs).succAbove ⟨↑i, ⋯⟩ < maxTimeFieldPosFin φ φsh.right𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove ⟨↑i, ⋯⟩) = i
      ·h.left𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ (maxTimeFieldPosFin φ φs).succAbove ⟨↑i, ⋯⟩ < maxTimeFieldPosFin φ φs simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, maxTimeFieldPosFin,
        insertionSortMinPosFin, Nat.succ_eq_add_one, Fin.mk_lt_mk, Fin.val_fin_lt, Fin.succ_mk]h.left𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ (if i < insertionSortMinPos timeOrderRel φ φs then ⟨↑i, ⋯⟩ else ⟨↑i + 1, ⋯⟩) <
  ⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩
        rw [Fin.lt_defh.left𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ ↑(if i < insertionSortMinPos timeOrderRel φ φs then ⟨↑i, ⋯⟩ else ⟨↑i + 1, ⋯⟩) <
  ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩h.left𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ ↑(if i < insertionSortMinPos timeOrderRel φ φs then ⟨↑i, ⋯⟩ else ⟨↑i + 1, ⋯⟩) <
  ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩]h.left𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ ↑(if i < insertionSortMinPos timeOrderRel φ φs then ⟨↑i, ⋯⟩ else ⟨↑i + 1, ⋯⟩) <
  ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩
        splith.left.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:i < insertionSortMinPos timeOrderRel φ φs⊢ ↑⟨↑i, ⋯⟩ < ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩h.left.isFalse𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:¬i < insertionSortMinPos timeOrderRel φ φs⊢ ↑⟨↑i, ⋯⟩ < ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩
        ·h.left.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:i < insertionSortMinPos timeOrderRel φ φs⊢ ↑⟨↑i, ⋯⟩ < ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩ simp only [Fin.val_fin_lt]h.left.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:i < insertionSortMinPos timeOrderRel φ φs⊢ i < insertionSortMinPos timeOrderRel φ φs
          omegaAll goals completed! 🐙
        ·h.left.isFalse𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:¬i < insertionSortMinPos timeOrderRel φ φs⊢ ↑⟨↑i, ⋯⟩ < ↑⟨↑(insertionSortMinPos timeOrderRel φ φs), ⋯⟩ omegaAll goals completed! 🐙
      ·h.right𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove ⟨↑i, ⋯⟩) = i simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, Fin.succ_mk, Fin.ext_iff,
        Fin.val_cast]h.right𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1⊢ ↑(if ⟨↑i, ⋯⟩ < Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs) then ⟨↑i, ⋯⟩ else ⟨↑i + 1, ⋯⟩) = ↑i
        splith.right.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:⟨↑i, ⋯⟩ < Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)⊢ ↑⟨↑i, ⋯⟩ = ↑ih.right.isFalse𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:¬⟨↑i, ⋯⟩ < Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)⊢ ↑⟨↑i + 1, ⋯⟩ = ↑i
        ·h.right.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:⟨↑i, ⋯⟩ < Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)⊢ ↑⟨↑i, ⋯⟩ = ↑i simpAll goals completed! 🐙
        ·h.right.isFalse𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthhi:i < insertionSortMinPos timeOrderRel φ φsh2:↑(insertionSortMinPos timeOrderRel φ φs) < ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).length + 1h✝:¬⟨↑i, ⋯⟩ < Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)⊢ ↑⟨↑i + 1, ⋯⟩ = ↑i simp_all [Fin.lt_def]All goals completed! 🐙
    ·e_a.e_a.e_6.refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthh:∃ a,
  (maxTimeFieldPosFin φ φs).succAbove a < maxTimeFieldPosFin φ φs ∧
    Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove a) = i⊢ i < insertionSortMinPos timeOrderRel φ φs obtain ⟨j, h1, h2⟩ := he_a.e_a.e_6.refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin (φ :: φs).lengthj:Fin ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).lengthh1:(maxTimeFieldPosFin φ φs).succAbove j < maxTimeFieldPosFin φ φsh2:Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove j) = i⊢ i < insertionSortMinPos timeOrderRel φ φs
      subst h2e_a.e_a.e_6.refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpj:Fin ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).lengthh1:(maxTimeFieldPosFin φ φs).succAbove j < maxTimeFieldPosFin φ φs⊢ Fin.cast ⋯ ((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove j) < insertionSortMinPos timeOrderRel φ φs
      simp only [Fin.lt_def, Fin.val_cast]e_a.e_a.e_6.refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpj:Fin ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).lengthh1:(maxTimeFieldPosFin φ φs).succAbove j < maxTimeFieldPosFin φ φs⊢ ↑((Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove j) < ↑(insertionSortMinPos timeOrderRel φ φs)
      exact h1All goals completed! 🐙
  ·𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.take (maxTimeFieldPos φ φs) (List.finRange (φs.length + 1))).Nodup exact List.Sublist.nodup (List.take_sublist _ _) <|
      List.nodup_finRange (φs.length + 1)All goals completed! 🐙
  ·𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (List.map (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)
    ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2)).Nodup refine List.Nodup.map ?_ ?_refine_1𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Function.Injective (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove)refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2).Nodup
    ·refine_1𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Function.Injective (Fin.cast ⋯ ∘ (Fin.cast ⋯ (insertionSortMinPos timeOrderRel φ φs)).succAbove) refine Function.Injective.comp ?hf.hg Fin.succAbove_right_injectivehf.hg𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Function.Injective (Fin.cast ⋯)
      exact Fin.cast_injective (eraseIdx_length (φ :: φs) (insertionSortMinPos timeOrderRel φ φs))All goals completed! 🐙
    ·refine_2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ({x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}.sort fun x1 x2 => x1 ≤ x2).Nodup exact Finset.sort_nodup
        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)
          Finset.univ) (fun x1 x2 => x1 ≤ x2)All goals completed! 🐙