Physlib.QFT.PerturbationTheory.WickContraction.SubContraction

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.UncontractedList

Sub contractions

@[expose] public section

Given a Wick contraction φsΛ, and a subset of φsΛ.1, the Wick contraction consisting of contracted pairs within that subset.

def subContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
    WickContraction φs.length :=
  ⟨S, by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ ∀ a ∈ S, a.card = 2
    intro i hi𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛi:Finset (Fin φs.length)hi:i ∈ S⊢ i.card = 2
    exact φsΛ.2.1 i (ha hi)All goals completed! 🐙,
    by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ ∀ a ∈ S, ∀ b ∈ S, a = b ∨ Disjoint a b
    intro i hi j hj𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛi:Finset (Fin φs.length)hi:i ∈ Sj:Finset (Fin φs.length)hj:j ∈ S⊢ i = j ∨ Disjoint i j
    exact φsΛ.2.2 i (ha hi) j (ha hj)All goals completed! 🐙⟩

lemma mem_of_mem_subContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    {a : Finset (Fin φs.length)} (ha : a ∈ (φsΛ.subContraction S hs).1) : a ∈ φsΛ.1 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑(subContraction S hs)⊢ a ∈ ↑φsΛ
  exact hs haAll goals completed! 🐙

Given a Wick contraction φsΛ, and a subset S of φsΛ.1, the Wick contraction on the uncontracted list [φsΛ.subContraction S ha]ᵘᶜ consisting of the remaining contracted pairs of φsΛ not in S.

def quotContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
    WickContraction [φsΛ.subContraction S ha]ᵘᶜ.length :=
  ⟨Finset.filter (fun a => Finset.map uncontractedListEmd a ∈ φsΛ.1) Finset.univ,
  by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ ∀ a ∈ {a | Finset.map uncontractedListEmd a ∈ ↑φsΛ}, a.card = 2
    intro a ha'𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha':a ∈ {a | Finset.map uncontractedListEmd a ∈ ↑φsΛ}⊢ a.card = 2
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha'𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha':Finset.map uncontractedListEmd a ∈ ↑φsΛ⊢ a.card = 2
    simpa using φsΛ.2.1 (Finset.map uncontractedListEmd a) ha'All goals completed! 🐙, by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ ∀ a ∈ {a | Finset.map uncontractedListEmd a ∈ ↑φsΛ},
  ∀ b ∈ {a | Finset.map uncontractedListEmd a ∈ ↑φsΛ}, a = b ∨ Disjoint a b
  intro a ha b hb𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:a ∈ {a | Finset.map uncontractedListEmd a ∈ ↑φsΛ}b:Finset (Fin [subContraction S ha]ᵘᶜ.length)hb:b ∈ {a | Finset.map uncontractedListEmd a ∈ ↑φsΛ}⊢ a = b ∨ Disjoint a b
  simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛ⊢ a = b ∨ Disjoint a b
  by_cases hab : a = bpos𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛhab:a = b⊢ a = b ∨ Disjoint a bneg𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛhab:¬a = b⊢ a = b ∨ Disjoint a b
  ·pos𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛhab:a = b⊢ a = b ∨ Disjoint a b simp [hab]All goals completed! 🐙
  ·neg𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛhab:¬a = b⊢ a = b ∨ Disjoint a b simp only [hab, false_or]neg𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛhab:¬a = b⊢ Disjoint a b
    have hx := φsΛ.2.2 (Finset.map uncontractedListEmd a) ha (Finset.map uncontractedListEmd b) hbneg𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha]ᵘᶜ.length)b:Finset (Fin [subContraction S ha]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhb:Finset.map uncontractedListEmd b ∈ ↑φsΛhab:¬a = bhx:Finset.map uncontractedListEmd a = Finset.map uncontractedListEmd b ∨
  Disjoint (Finset.map uncontractedListEmd a) (Finset.map uncontractedListEmd b)⊢ Disjoint a b
    simp_allAll goals completed! 🐙⟩

              lemma mem_of_mem_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    {a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)}
    (ha : a ∈ (quotContraction S hs).1) : Finset.map uncontractedListEmd a ∈ φsΛ.1 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛ
  simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛ⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛ
  exact haAll goals completed! 🐙

lemma mem_subContraction_or_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    {a : Finset (Fin φs.length)} (ha : a ∈ φsΛ.1) :
    a ∈ (φsΛ.subContraction S hs).1 ∨
    ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ (quotContraction S hs).1 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛ⊢ a ∈ ↑(subContraction S hs) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)
  by_cases h1 : a ∈ (φsΛ.subContraction S hs).1pos𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∈ ↑(subContraction S hs)⊢ a ∈ ↑(subContraction S hs) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ ↑(subContraction S hs)⊢ a ∈ ↑(subContraction S hs) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)
  ·pos𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∈ ↑(subContraction S hs)⊢ a ∈ ↑(subContraction S hs) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs) simp [h1]All goals completed! 🐙
  simp only [h1, false_or]neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ ↑(subContraction S hs)⊢ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)
  simp only [subContraction] at h1neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ S⊢ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)
  have h2 := φsΛ.2.1 a haneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ Sh2:a.card = 2⊢ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)
  rw [@Finset.card_eq_twoneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ Sh2:∃ x y, x ≠ y ∧ a = {x, y}⊢ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ Sh2:∃ x y, x ≠ y ∧ a = {x, y}⊢ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)] at h2neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛh1:a ∉ Sh2:∃ x y, x ≠ y ∧ a = {x, y}⊢ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)
  obtain ⟨i, j, hij, rfl⟩ := h2neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ S⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
  have hi : i ∈ (φsΛ.subContraction S hs).uncontracted := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛ⊢ a ∈ ↑(subContraction S hs) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    rw [mem_uncontracted_iff_not_contracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ S⊢ ∀ p ∈ ↑(subContraction S hs), i ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ S⊢ ∀ p ∈ ↑(subContraction S hs), i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ S⊢ ∀ p ∈ ↑(subContraction S hs), i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    intro p hp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ ↑(subContraction S hs)⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    have hp' : p ∈ φsΛ.1 := hs hp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ ↑(subContraction S hs)hp':p ∈ ↑φsΛ⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    have hp2 := φsΛ.2.2 p hp' {i, j} ha𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ ↑(subContraction S hs)hp':p ∈ ↑φsΛhp2:p = {i, j} ∨ Disjoint p {i, j}⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    simp only [subContraction] at hp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:p = {i, j} ∨ Disjoint p {i, j}⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    rcases hp2 with hp2 | hp2inl𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:p = {i, j}⊢ i ∉ pinr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:Disjoint p {i, j}⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    ·inl𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:p = {i, j}⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs) simp_allAll goals completed! 🐙neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2inr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Sp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:i ∉ p ∧ j ∉ p⊢ i ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    exact hp2.1neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
  have hj : j ∈ (φsΛ.subContraction S hs).uncontracted := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛ⊢ a ∈ ↑(subContraction S hs) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S hs)neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    rw [mem_uncontracted_iff_not_contracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∀ p ∈ ↑(subContraction S hs), j ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∀ p ∈ ↑(subContraction S hs), j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontracted⊢ ∀ p ∈ ↑(subContraction S hs), j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    intro p hp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ ↑(subContraction S hs)⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    have hp' : p ∈ φsΛ.1 := hs hp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ ↑(subContraction S hs)hp':p ∈ ↑φsΛ⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    have hp2 := φsΛ.2.2 p hp' {i, j} ha𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ ↑(subContraction S hs)hp':p ∈ ↑φsΛhp2:p = {i, j} ∨ Disjoint p {i, j}⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    simp only [subContraction] at hp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:p = {i, j} ∨ Disjoint p {i, j}⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    rcases hp2 with hp2 | hp2inl𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:p = {i, j}⊢ j ∉ pinr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:Disjoint p {i, j}⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    ·inl𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:p = {i, j}⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs) simp_allAll goals completed! 🐙neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2inr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedp:Finset (Fin φs.length)hp:p ∈ Shp':p ∈ ↑φsΛhp2:i ∉ p ∧ j ∉ p⊢ j ∉ pneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
    exact hp2.2neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)neg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin φs.lengthj:Fin φs.lengthhij:i ≠ jha:{i, j} ∈ ↑φsΛh1:{i, j} ∉ Shi:i ∈ (subContraction S hs).uncontractedhj:j ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {i, j} ∧ a' ∈ ↑(quotContraction S hs)
  obtain ⟨i, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted i hineg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛj:Fin φs.lengthhj:j ∈ (subContraction S hs).uncontractedi:Fin [subContraction S hs]ᵘᶜ.lengthhij:uncontractedListEmd i ≠ jha:{uncontractedListEmd i, j} ∈ ↑φsΛh1:{uncontractedListEmd i, j} ∉ Shi:uncontractedListEmd i ∈ (subContraction S hs).uncontracted⊢ ∃ a', Finset.map uncontractedListEmd a' = {uncontractedListEmd i, j} ∧ a' ∈ ↑(quotContraction S hs)
  obtain ⟨j, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted j hjneg𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin [subContraction S hs]ᵘᶜ.lengthhi:uncontractedListEmd i ∈ (subContraction S hs).uncontractedj:Fin [subContraction S hs]ᵘᶜ.lengthhj:uncontractedListEmd j ∈ (subContraction S hs).uncontractedhij:uncontractedListEmd i ≠ uncontractedListEmd jha:{uncontractedListEmd i, uncontractedListEmd j} ∈ ↑φsΛh1:{uncontractedListEmd i, uncontractedListEmd j} ∉ S⊢ ∃ a', Finset.map uncontractedListEmd a' = {uncontractedListEmd i, uncontractedListEmd j} ∧ a' ∈ ↑(quotContraction S hs)
  use {i, j}h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin [subContraction S hs]ᵘᶜ.lengthhi:uncontractedListEmd i ∈ (subContraction S hs).uncontractedj:Fin [subContraction S hs]ᵘᶜ.lengthhj:uncontractedListEmd j ∈ (subContraction S hs).uncontractedhij:uncontractedListEmd i ≠ uncontractedListEmd jha:{uncontractedListEmd i, uncontractedListEmd j} ∈ ↑φsΛh1:{uncontractedListEmd i, uncontractedListEmd j} ∉ S⊢ Finset.map uncontractedListEmd {i, j} = {uncontractedListEmd i, uncontractedListEmd j} ∧
  {i, j} ∈ ↑(quotContraction S hs)
  simp only [Finset.map_insert, Finset.map_singleton, quotContraction, Finset.mem_filter,
    Finset.mem_univ, true_and]h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛi:Fin [subContraction S hs]ᵘᶜ.lengthhi:uncontractedListEmd i ∈ (subContraction S hs).uncontractedj:Fin [subContraction S hs]ᵘᶜ.lengthhj:uncontractedListEmd j ∈ (subContraction S hs).uncontractedhij:uncontractedListEmd i ≠ uncontractedListEmd jha:{uncontractedListEmd i, uncontractedListEmd j} ∈ ↑φsΛh1:{uncontractedListEmd i, uncontractedListEmd j} ∉ S⊢ {uncontractedListEmd i, uncontractedListEmd j} ∈ ↑φsΛ
  exact haAll goals completed! 🐙@[simp]
lemma subContraction_uncontractedList_get {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    {a : Fin [subContraction S hs]ᵘᶜ.length} :
    [subContraction S hs]ᵘᶜ[a] = φs[uncontractedListEmd a] := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Fin [subContraction S hs]ᵘᶜ.length⊢ [subContraction S hs]ᵘᶜ[a] = φs[uncontractedListEmd a]
  erw [← getElem_uncontractedListEmd𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Fin [subContraction S hs]ᵘᶜ.length⊢ φs[↑(uncontractedListEmd a)] = φs[uncontractedListEmd a]]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Fin [subContraction S hs]ᵘᶜ.length⊢ φs[↑(uncontractedListEmd a)] = φs[uncontractedListEmd a]
  rflAll goals completed! 🐙@[simp]
lemma subContraction_fstFieldOfContract {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    (a : (subContraction S hs).1) :
    (subContraction S hs).fstFieldOfContract a =
    φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ (subContraction S hs).fstFieldOfContract a = φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩
  apply eq_fstFieldOfContract_of_mem _ _ _
    (φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩)hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑ahj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑ahij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ < φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩
  ·hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
      ⟨a.1, mem_of_mem_subContraction a.2⟩hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑⟨↑a, ⋯⟩ = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    simp only at hahi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    conv_lhs =>
      rw [ha]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}| {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}
    simpAll goals completed! 🐙
  ·hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
      ⟨a.1, mem_of_mem_subContraction a.2⟩hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑⟨↑a, ⋯⟩ = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    simp only at hahj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    conv_lhs =>
      rw [ha]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}| {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}
    simpAll goals completed! 🐙
  ·hij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ < φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ exact fstFieldOfContract_lt_sndFieldOfContract φsΛ ⟨↑a, mem_of_mem_subContraction a.property⟩All goals completed! 🐙@[simp]
lemma subContraction_sndFieldOfContract {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    (a : (subContraction S hs).1) :
    (subContraction S hs).sndFieldOfContract a =
    φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ (subContraction S hs).sndFieldOfContract a = φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩
  apply eq_sndFieldOfContract_of_mem _ _
    (φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩)hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑ahj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑ahij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ < φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩
  ·hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
      ⟨a.1, mem_of_mem_subContraction a.2⟩hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑⟨↑a, ⋯⟩ = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    simp only at hahi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    conv_lhs =>
      rw [ha]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}| {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}
    simpAll goals completed! 🐙
  ·hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
      ⟨a.1, mem_of_mem_subContraction a.2⟩hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑⟨↑a, ⋯⟩ = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    simp only at hahj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}⊢ φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ ∈ ↑a
    conv_lhs =>
      rw [ha]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)ha:↑a = {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}| {φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩, φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩}
    simpAll goals completed! 🐙
  ·hij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(subContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩ < φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩ exact fstFieldOfContract_lt_sndFieldOfContract φsΛ ⟨↑a, mem_of_mem_subContraction a.property⟩All goals completed! 🐙@[simp]
lemma quotContraction_fstFieldOfContract_uncontractedListEmd {S : Finset (Finset (Fin φs.length))}
    {hs : S ⊆ φsΛ.1} (a : (quotContraction S hs).1) :
    uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) =
    (φsΛ.fstFieldOfContract
    ⟨Finset.map uncontractedListEmd a.1, mem_of_mem_quotContraction a.2⟩) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) =
  φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩
  symm𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩ =
  uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a)
  apply eq_fstFieldOfContract_of_mem _ _ _
    (uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a))hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩hij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) <
  uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a)
  ·hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩ simp only [Finset.mem_map', fstFieldOfContract_mem]All goals completed! 🐙
  ·hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩ simpAll goals completed! 🐙
  ·hij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) <
  uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) apply uncontractedListEmd_strictMonohij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ (quotContraction S hs).fstFieldOfContract a < (quotContraction S hs).sndFieldOfContract a
    exact fstFieldOfContract_lt_sndFieldOfContract (quotContraction S hs) aAll goals completed! 🐙@[simp]
lemma quotContraction_sndFieldOfContract_uncontractedListEmd {S : Finset (Finset (Fin φs.length))}
    {hs : S ⊆ φsΛ.1} (a : (quotContraction S hs).1) :
    uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) =
    (φsΛ.sndFieldOfContract
      ⟨Finset.map uncontractedListEmd a.1, mem_of_mem_quotContraction a.2⟩) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) =
  φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩
  symm𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩ =
  uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a)
  apply eq_sndFieldOfContract_of_mem _ _
    (uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a))hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩hij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) <
  uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a)
  ·hi𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩ simp only [Finset.mem_map', fstFieldOfContract_mem]All goals completed! 🐙
  ·hj𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) ∈ ↑⟨Finset.map uncontractedListEmd ↑a, ⋯⟩ simpAll goals completed! 🐙
  ·hij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) <
  uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) apply uncontractedListEmd_strictMonohij𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:↥↑(quotContraction S hs)⊢ (quotContraction S hs).fstFieldOfContract a < (quotContraction S hs).sndFieldOfContract a
    exact fstFieldOfContract_lt_sndFieldOfContract (quotContraction S hs) aAll goals completed! 🐙lemma quotContraction_gradingCompliant {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    (hsΛ : φsΛ.GradingCompliant) :
    GradingCompliant [φsΛ.subContraction S hs]ᵘᶜ (quotContraction S hs) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛ⊢ GradingCompliant [subContraction S hs]ᵘᶜ (quotContraction S hs)
  simp only [GradingCompliant, Subtype.forall]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛ⊢ ∀ (a : Finset (Fin [subContraction S hs]ᵘᶜ.length)) (b : a ∈ ↑(quotContraction S hs)),
  (𝓕|>ₛ[subContraction S hs]ᵘᶜ[↑((quotContraction S hs).fstFieldOfContract ⟨a, b⟩)]) =
    𝓕|>ₛ[subContraction S hs]ᵘᶜ[↑((quotContraction S hs).sndFieldOfContract ⟨a, b⟩)]
  intro a ha𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ (𝓕|>ₛ[subContraction S hs]ᵘᶜ[↑((quotContraction S hs).fstFieldOfContract ⟨a, ha⟩)]) =
  𝓕|>ₛ[subContraction S hs]ᵘᶜ[↑((quotContraction S hs).sndFieldOfContract ⟨a, ha⟩)]
  erw [subContraction_uncontractedList_get𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ (𝓕|>ₛφs[uncontractedListEmd ((quotContraction S hs).fstFieldOfContract ⟨a, ha⟩)]) =
  𝓕|>ₛ[subContraction S hs]ᵘᶜ[↑((quotContraction S hs).sndFieldOfContract ⟨a, ha⟩)]]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ (𝓕|>ₛφs[uncontractedListEmd ((quotContraction S hs).fstFieldOfContract ⟨a, ha⟩)]) =
  𝓕|>ₛ[subContraction S hs]ᵘᶜ[↑((quotContraction S hs).sndFieldOfContract ⟨a, ha⟩)]
  erw [subContraction_uncontractedList_get𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ (𝓕|>ₛφs[uncontractedListEmd ((quotContraction S hs).fstFieldOfContract ⟨a, ha⟩)]) =
  𝓕|>ₛφs[uncontractedListEmd ((quotContraction S hs).sndFieldOfContract ⟨a, ha⟩)]]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ (𝓕|>ₛφs[uncontractedListEmd ((quotContraction S hs).fstFieldOfContract ⟨a, ha⟩)]) =
  𝓕|>ₛφs[uncontractedListEmd ((quotContraction S hs).sndFieldOfContract ⟨a, ha⟩)]
  simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
    quotContraction_sndFieldOfContract_uncontractedListEmd]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛhsΛ:GradingCompliant φs φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S hs)⊢ (𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)]) =
  𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)]
  apply hsΛAll goals completed! 🐙lemma mem_quotContraction_iff {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
    {a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)} :
    a ∈ (quotContraction S hs).1 ↔ a.map uncontractedListEmd ∈ φsΛ.1
    ∧ a.map uncontractedListEmd ∉ (subContraction S hs).1 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)⊢ a ∈ ↑(quotContraction S hs) ↔
  Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs)
  apply Iff.intromp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)⊢ a ∈ ↑(quotContraction S hs) →
  Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs)mpr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs) →
  a ∈ ↑(quotContraction S hs)
  ·mp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)⊢ a ∈ ↑(quotContraction S hs) →
  Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs) intro hmp𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:a ∈ ↑(quotContraction S hs)⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs)
    apply And.intromp.left𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:a ∈ ↑(quotContraction S hs)⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛmp.right𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:a ∈ ↑(quotContraction S hs)⊢ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs)
    ·mp.left𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:a ∈ ↑(quotContraction S hs)⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛ exact mem_of_mem_quotContraction hAll goals completed! 🐙
    ·mp.right𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:a ∈ ↑(quotContraction S hs)⊢ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs) exact uncontractedListEmd_finset_not_mem _All goals completed! 🐙
  ·mpr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)⊢ Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs) →
  a ∈ ↑(quotContraction S hs) intro hmpr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs)⊢ a ∈ ↑(quotContraction S hs)
    have h2 := mem_subContraction_or_quotContraction (S := S) (hs := hs) h.1mpr𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))hs:S ⊆ ↑φsΛa:Finset (Fin [subContraction S hs]ᵘᶜ.length)h:Finset.map uncontractedListEmd a ∈ ↑φsΛ ∧ Finset.map uncontractedListEmd a ∉ ↑(subContraction S hs)h2:Finset.map uncontractedListEmd a ∈ ↑(subContraction S hs) ∨
  ∃ a', Finset.map uncontractedListEmd a' = Finset.map uncontractedListEmd a ∧ a' ∈ ↑(quotContraction S hs)⊢ a ∈ ↑(quotContraction S hs)
    simp_allAll goals completed! 🐙