Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions

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

Normal ordering with relation to Wick contractions

@[expose] public section

Normal order of uncontracted terms within proto-algebra.

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]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)

where s is the exchange sign for φ and the uncontracted fields in φ₀…φᵢ₋₁.

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


lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
    𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ)
    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
    𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) •
    normalOrder (ofFieldOpList (φ :: [φsΛ]ᵘᶜ))
  simp only [Nat.succ_eq_add_one]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) •
    normalOrder (ofFieldOpList (φ :: [φsΛ]ᵘᶜ))
  rw [ofFieldOpList_normalOrder_insert φ [φsΛ]ᵘᶜ
    ⟨(φsΛ.uncontractedListOrderPos i), by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ φsΛ.uncontractedListOrderPos i < [φsΛ]ᵘᶜ.length.succ𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))) •
    normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ)) simp [uncontractedListGet]All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))) •
    normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))⟩,
    smul_smul𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))) •
    normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))) •
    normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))) •
    normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  refine (one_smul ℂ _).symm.trans ?_𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 • normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))) •
    normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  congr 1e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take ↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩ [φsΛ]ᵘᶜ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  simp only [uncontractedListGet]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.take (φsΛ.uncontractedListOrderPos i) (List.map φs.get φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  rw [← List.map_take,e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.take (φsΛ.uncontractedListOrderPos i) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ)) take_uncontractedListOrderPos_eq_filtere_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  have h1 : (𝓕 |>ₛ List.map φs.get (List.filter (fun x => decide (↑x < i.1)) φsΛ.uncontractedList))
        = 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x.val < i.1))⟩ := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) •
    normalOrder (ofFieldOpList (φ :: [φsΛ]ᵘᶜ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      simp only [Nat.succ_eq_add_one, ofFinset]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofList 𝓕.fieldOpStatistic (List.map φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      congre_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      rw [uncontractedList_eq_sorte_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      have hdup : (List.filter (fun x => decide (x.1 < i.1))
          (φsΛ.uncontracted.sort (fun x1 x2 => x1 ≤ x2))).Nodup :=
        List.Nodup.filter _ (φsΛ.uncontracted.sort_nodup (fun x1 x2 => x1 ≤ x2))e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Nodup⊢ List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      have hsort : (List.filter (fun x => decide (x.1 < i.1))
          (φsΛ.uncontracted.sort (fun x1 x2 => x1 ≤ x2))).Pairwise (· ≤ ·) :=
        List.Pairwise.filter _ (φsΛ.uncontracted.pairwise_sort (fun x1 x2 => x1 ≤ x2))e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Noduphsort:List.Pairwise (fun x1 x2 => x1 ≤ x2)
  (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2))⊢ List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      rw [← (List.toFinset_sort (· ≤ ·) hdup).mpr hsorte_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Noduphsort:List.Pairwise (fun x1 x2 => x1 ≤ x2)
  (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2))⊢ ((List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).toFinset.sort fun x1 x2 =>
    x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Noduphsort:List.Pairwise (fun x1 x2 => x1 ≤ x2)
  (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2))⊢ ((List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).toFinset.sort fun x1 x2 =>
    x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]e_φs.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Noduphsort:List.Pairwise (fun x1 x2 => x1 ≤ x2)
  (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2))⊢ ((List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).toFinset.sort fun x1 x2 =>
    x1 ≤ x2) =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      congre_φs.e_l.e_s𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Noduphsort:List.Pairwise (fun x1 x2 => x1 ≤ x2)
  (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2))⊢ (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).toFinset =
  {x ∈ φsΛ.uncontracted | ↑x < ↑i}e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      ext ae_φs.e_l.e_s𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhdup:(List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).Noduphsort:List.Pairwise (fun x1 x2 => x1 ≤ x2)
  (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2))a:Fin φs.length⊢ a ∈ (List.filter (fun x => decide (↑x < ↑i)) (φsΛ.uncontracted.sort fun x1 x2 => x1 ≤ x2)).toFinset ↔
  a ∈ {x ∈ φsΛ.uncontracted | ↑x < ↑i}e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
      simpe_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ))
      (ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  rw [h1e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  simp only [Nat.succ_eq_add_one]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  have h2 : (Finset.filter (fun x => x.1 < i.1) φsΛ.uncontracted) =
    (Finset.filter (fun x => i.succAbove x < i) φsΛ.uncontracted) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) •
    normalOrder (ofFieldOpList (φ :: [φsΛ]ᵘᶜ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
    refine Finset.filter_congr fun a _ => ?_𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})a:Fin φs.lengthx✝:a ∈ φsΛ.uncontracted⊢ ↑a < ↑i ↔ i.succAbove a < ie_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
    rw [Fin.succAbove_lt_iff_castSucc_lt,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})a:Fin φs.lengthx✝:a ∈ φsΛ.uncontracted⊢ ↑a < ↑i ↔ a.castSucc < ie_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ)) Fin.lt_def,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})a:Fin φs.lengthx✝:a ∈ φsΛ.uncontracted⊢ ↑a < ↑i ↔ ↑a.castSucc < ↑ie_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ)) Fin.val_castSucc𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})a:Fin φs.lengthx✝:a ∈ φsΛ.uncontracted⊢ ↑a < ↑i ↔ ↑a < ↑ie_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  rw [h2e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthh1:ofList 𝓕.fieldOpStatistic (List.map φs.get (List.filter (fun x => decide (↑x < ↑i)) φsΛ.uncontractedList)) =
  ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | ↑x < ↑i})h2:{x ∈ φsΛ.uncontracted | ↑x < ↑i} = {x ∈ φsΛ.uncontracted | i.succAbove x < i}⊢ 1 =
  (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i})) *
    (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | i.succAbove x < i}))e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  simp only [exchangeSign_mul_self]e_a𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) =
  normalOrder (ofFieldOpList ([φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ))
  congre_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ [φsΛ↩Λφ i none]ᵘᶜ = [φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φ
  rw [insertAndContract_uncontractedList_none_mape_a.e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.length⊢ [φsΛ]ᵘᶜ.insertIdx (φsΛ.uncontractedListOrderPos i) φ = [φsΛ]ᵘᶜ.insertIdx (↑⟨φsΛ.uncontractedListOrderPos i, ⋯⟩) φAll goals completed! 🐙]All 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)]ᵘᶜ) is equal to the normal ordering of [φsΛ]ᵘᶜ with the 𝓕.FieldOp corresponding to k removed.

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


lemma normalOrder_uncontracted_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :
    𝓝(ofFieldOpList [φsΛ ↩Λ φ i (some k)]ᵘᶜ)
    = 𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedFieldOpEquiv φs φsΛ) k))) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ normalOrder (ofFieldOpList [φsΛ↩Λφ i some k]ᵘᶜ) =
  normalOrder (ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedFieldOpEquiv φs φsΛ) (some k))))
  simp only [Nat.succ_eq_add_one, insertAndContract, optionEraseZ, uncontractedFieldOpEquiv,
    uncontractedListGet]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ normalOrder
    (ofFieldOpList
      (List.map (φs.insertIdx (↑i) φ).get
        ((WickContraction.congr ⋯) (φsΛ.insertAndContractNat i (some k))).uncontractedList)) =
  normalOrder
    (ofFieldOpList
      (match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
      | none => φ :: List.map φs.get φsΛ.uncontractedList
      | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i))
  congre_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map (φs.insertIdx (↑i) φ).get ((WickContraction.congr ⋯) (φsΛ.insertAndContractNat i (some k))).uncontractedList =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i
  rw [congr_uncontractedListe_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map (φs.insertIdx (↑i) φ).get (List.map (⇑(finCongr ⋯)) (φsΛ.insertAndContractNat i (some k)).uncontractedList) =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑ie_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map (φs.insertIdx (↑i) φ).get (List.map (⇑(finCongr ⋯)) (φsΛ.insertAndContractNat i (some k)).uncontractedList) =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i]e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map (φs.insertIdx (↑i) φ).get (List.map (⇑(finCongr ⋯)) (φsΛ.insertAndContractNat i (some k)).uncontractedList) =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i
  erw [uncontractedList_extractEquiv_symm_somee_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map (φs.insertIdx (↑i) φ).get
    (List.map (⇑(finCongr ⋯))
      ((List.map (⇑i.succAboveEmb) φsΛ.uncontractedList).eraseIdx ↑(φsΛ.uncontractedIndexEquiv.symm k))) =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i]e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map (φs.insertIdx (↑i) φ).get
    (List.map (⇑(finCongr ⋯))
      ((List.map (⇑i.succAboveEmb) φsΛ.uncontractedList).eraseIdx ↑(φsΛ.uncontractedIndexEquiv.symm k))) =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i
  simp only [Fin.coe_succAboveEmb, List.map_eraseIdx, List.map_map]e_6𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ (List.map ((φs.insertIdx (↑i) φ).get ∘ ⇑(finCongr ⋯) ∘ i.succAbove) φsΛ.uncontractedList).eraseIdx
    ↑(φsΛ.uncontractedIndexEquiv.symm k) =
  match (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr (some k) with
  | none => φ :: List.map φs.get φsΛ.uncontractedList
  | some i => (List.map φs.get φsΛ.uncontractedList).eraseIdx ↑i
  congr 1e_6.e_l𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted⊢ List.map ((φs.insertIdx (↑i) φ).get ∘ ⇑(finCongr ⋯) ∘ i.succAbove) φsΛ.uncontractedList =
  List.map φs.get φsΛ.uncontractedList
  conv_rhs => rw [get_eq_insertIdx_succAbove φ φs i]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontracted| List.map ((φs.insertIdx (↑i) φ).get ∘ ⇑(finCongr ⋯) ∘ i.succAbove) φsΛ.uncontractedList