Physlib.QFT.PerturbationTheory.WickContraction.StaticContract

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.WickContraction.InsertAndContract
public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas

Time contractions

@[expose] public section

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a i ≤ φs.length, then the following relation holds:

(φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract

The proof of this result ultimately is a consequence of definitions.


@[simp]
lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
    (φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (φsΛ↩Λφ i none).staticContract = φsΛ.staticContract
  rw [staticContract,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ ∏ a,
    ⟨(superCommute (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract a))))
        (ofFieldOp ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract a))),
      ⋯⟩ =
  φsΛ.staticContract𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ ∏ a,
    ⟨(superCommute
          (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a))))),
      ⋯⟩ =
  φsΛ.staticContract insertAndContract_none_prod_contractions𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ ∏ a,
    ⟨(superCommute
          (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a))))),
      ⋯⟩ =
  φsΛ.staticContract𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ ∏ a,
    ⟨(superCommute
          (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a))))),
      ⋯⟩ =
  φsΛ.staticContract]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ ∏ a,
    ⟨(superCommute
          (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a))))),
      ⋯⟩ =
  φsΛ.staticContract
  congr with ae_f𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succa:↥↑φsΛ⊢ ↑⟨(superCommute
          (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a))))),
      ⋯⟩ =
  ↑⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩
  simpAll goals completed! 🐙

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted, then (φsΛ ↩Λ φ i (some k)).staticContract is equal to the product of

[anPart φ, φs[k]]ₛ if i ≤ k or [anPart φs[k], φ]ₛ if k < i

φsΛ.staticContract.

The proof of this result ultimately is a consequence of definitions.


lemma staticContract_insert_some
    (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
    (φsΛ ↩Λ φ i (some j)).staticContract =
    (if i < i.succAbove j then
      ⟨[anPart φ, ofFieldOp φs[j.1]]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩
    else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) *
    φsΛ.staticContract := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ (φsΛ↩Λφ i some j).staticContract =
  (if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
    else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩) *
    φsΛ.staticContract
  rw [staticContract,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ∏ a,
    ⟨(superCommute (anPart ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract a))))
        (ofFieldOp ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract a))),
      ⋯⟩ =
  (if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
    else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩) *
    φsΛ.staticContract𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))),
      ⋯⟩ *
    ∏ a,
      ⟨(superCommute
            (anPart
              ((φs.insertIdx (↑i) φ).get
                ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
          (ofFieldOp
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
        ⋯⟩ =
  (if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
    else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩) *
    φsΛ.staticContract insertAndContract_some_prod_contractions𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))),
      ⋯⟩ *
    ∏ a,
      ⟨(superCommute
            (anPart
              ((φs.insertIdx (↑i) φ).get
                ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
          (ofFieldOp
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
        ⋯⟩ =
  (if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
    else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩) *
    φsΛ.staticContract𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))),
      ⋯⟩ *
    ∏ a,
      ⟨(superCommute
            (anPart
              ((φs.insertIdx (↑i) φ).get
                ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
          (ofFieldOp
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
        ⋯⟩ =
  (if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
    else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩) *
    φsΛ.staticContract]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))),
      ⋯⟩ *
    ∏ a,
      ⟨(superCommute
            (anPart
              ((φs.insertIdx (↑i) φ).get
                ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
          (ofFieldOp
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
        ⋯⟩ =
  (if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
    else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩) *
    φsΛ.staticContract
  congr 1e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
        (anPart
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))))
      (ofFieldOp
        ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))),
    ⋯⟩ =
  if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
  else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ∏ a,
    ⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
      ⋯⟩ =
  φsΛ.staticContract
  ·e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
        (anPart
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))))
      (ofFieldOp
        ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩)))),
    ⋯⟩ =
  if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑j]), ⋯⟩
  else ⟨(superCommute (anPart φs[↑j])) (ofFieldOp φ), ⋯⟩ simp only [Nat.succ_eq_add_one, insertAndContract_fstFieldOfContract_some_incl, finCongr_apply,
    List.get_eq_getElem, insertAndContract_sndFieldOfContract_some_incl, Fin.getElem_fin]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨(superCommute
        (anPart (φs.insertIdx (↑i) φ)[↑(if i < i.succAbove ↑j then Fin.cast ⋯ i else Fin.cast ⋯ (i.succAbove ↑j))]))
      (ofFieldOp (φs.insertIdx (↑i) φ)[↑(if i < i.succAbove ↑j then Fin.cast ⋯ (i.succAbove ↑j) else Fin.cast ⋯ i)]),
    ⋯⟩ =
  if i < i.succAbove ↑j then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑↑j]), ⋯⟩
  else ⟨(superCommute (anPart φs[↑↑j])) (ofFieldOp φ), ⋯⟩
    splite_a.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:i < i.succAbove ↑j⊢ ⟨(superCommute (anPart (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)]))
      (ofFieldOp (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))]),
    ⋯⟩ =
  ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑↑j]), ⋯⟩e_a.isFalse𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:¬i < i.succAbove ↑j⊢ ⟨(superCommute (anPart (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))]))
      (ofFieldOp (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)]),
    ⋯⟩ =
  ⟨(superCommute (anPart φs[↑↑j])) (ofFieldOp φ), ⋯⟩ <;>e_a.isTrue𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:i < i.succAbove ↑j⊢ ⟨(superCommute (anPart (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)]))
      (ofFieldOp (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))]),
    ⋯⟩ =
  ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑↑j]), ⋯⟩e_a.isFalse𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:¬i < i.succAbove ↑j⊢ ⟨(superCommute (anPart (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))]))
      (ofFieldOp (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)]),
    ⋯⟩ =
  ⟨(superCommute (anPart φs[↑↑j])) (ofFieldOp φ), ⋯⟩ simpAll goals completed! 🐙
  ·e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ∏ a,
    ⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
      ⋯⟩ =
  φsΛ.staticContract congr with ae_a.e_f𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracteda:↥↑φsΛ⊢ ↑⟨(superCommute
          (anPart
            ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))))
        (ofFieldOp
          ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a))))),
      ⋯⟩ =
  ↑⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩
    simpAll goals completed! 🐙



set_option backward.isDefEq.respectTransparency false in
lemma staticContract_insert_some_of_lt
    (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
    (hik : i < i.succAbove k) :
    (φsΛ ↩Λ φ i (some k)).staticContract =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
    • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *
      φsΛ.staticContract) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑(φsΛ↩Λφ i some k).staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)
  rw [staticContract_insert_some𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑((if i < i.succAbove ↑k then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑k]), ⋯⟩
      else ⟨(superCommute (anPart φs[↑k])) (ofFieldOp φ), ⋯⟩) *
      φsΛ.staticContract) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑((if i < i.succAbove ↑k then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑k]), ⋯⟩
      else ⟨(superCommute (anPart φs[↑k])) (ofFieldOp φ), ⋯⟩) *
      φsΛ.staticContract) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑((if i < i.succAbove ↑k then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑k]), ⋯⟩
      else ⟨(superCommute (anPart φs[↑k])) (ofFieldOp φ), ⋯⟩) *
      φsΛ.staticContract) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)
  simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul,
    contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
    Equiv.coe_trans, Option.map_some, Function.comp_apply, finCongr_apply, Fin.val_cast,
    List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
    Algebra.smul_mul_assoc, uncontractedListGet]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑(if i < i.succAbove ↑k then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑↑k]), ⋯⟩ * φsΛ.staticContract
    else ⟨(superCommute (anPart φs[↑↑k])) (ofFieldOp φ), ⋯⟩ * φsΛ.staticContract) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
  ·𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑(if i < i.succAbove ↑k then ⟨(superCommute (anPart φ)) (ofFieldOp φs[↑↑k]), ⋯⟩ * φsΛ.staticContract
    else ⟨(superCommute (anPart φs[↑↑k])) (ofFieldOp φ), ⋯⟩ * φsΛ.staticContract) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract) simp only [hik, ↓reduceIte, MulMemClass.coe_mul]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
    have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
        (List.map φs.get φsΛ.uncontractedList))
        = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ↑(φsΛ↩Λφ i some k).staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
      simp only [ofFinset]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofList 𝓕.fieldOpStatistic (List.map φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
      congre_φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList) =
  List.map φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
      rw [← List.map_takee_φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ List.map φs.get (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) φsΛ.uncontractedList) =
  List.map φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2)e_φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ List.map φs.get (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) φsΛ.uncontractedList) =
  List.map φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)]e_φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ List.map φs.get (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) φsΛ.uncontractedList) =
  List.map φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
      congre_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) φsΛ.uncontractedList =
  {x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
      rw [take_uncontractedIndexEquiv_symm,e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ List.filter (fun i => decide (i < ↑k)) φsΛ.uncontractedList = {x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract) filter_uncontractedListe_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑k⊢ ({i ∈ φsΛ.uncontracted | i < ↑k}.sort fun x1 x2 => x1 ≤ x2) = {x ∈ φsΛ.uncontracted | x < ↑k}.sort fun x1 x2 => x1 ≤ x2𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ))
        (ofList 𝓕.fieldOpStatistic
          (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList))) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)
    rw [h1,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) •
      ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)All goals completed! 🐙 smul_smul,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) *
      (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}))) •
    ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)All goals completed! 🐙 exchangeSign_mul_self,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  1 • ((superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract)All goals completed! 🐙 one_smul𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedhik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContract =
  (superCommute (anPart φ)) (ofFieldOp φs[↑↑k]) * ↑φsΛ.staticContractAll goals completed! 🐙]All goals completed! 🐙



lemma staticContract_of_not_gradingCompliant (φs : List 𝓕.FieldOp)
    (φsΛ : WickContraction φs.length) (h : ¬ GradingCompliant φs φsΛ) :
    φsΛ.staticContract = 0 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:¬GradingCompliant φs φsΛ⊢ φsΛ.staticContract = 0
  rw [staticContract𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:¬GradingCompliant φs φsΛ⊢ ∏ a, ⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩ =
  0𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:¬GradingCompliant φs φsΛ⊢ ∏ a, ⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩ =
  0]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:¬GradingCompliant φs φsΛ⊢ ∏ a, ⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩ =
  0
  simp only [GradingCompliant, Subtype.forall, not_forall] at h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:∃ x, ∃ (x_1 : x ∈ ↑φsΛ), ¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨x, x_1⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨x, x_1⟩)]⊢ ∏ a, ⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩ =
  0
  obtain ⟨a, ha, ha2⟩ := h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ ∏ a, ⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract a)))) (ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))), ⋯⟩ =
  0
  refine Finset.prod_eq_zero (Finset.mem_univ ⟨a, ha⟩) (Subtype.ext ?_)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ ↑⟨(superCommute (anPart (φs.get (φsΛ.fstFieldOfContract ⟨a, ha⟩))))
        (ofFieldOp (φs.get (φsΛ.sndFieldOfContract ⟨a, ha⟩))),
      ⋯⟩ =
  ↑0
  exact superCommute_anPart_ofFieldOpF_diff_grade_zero _ _ ha2All goals completed! 🐙