Physlib.QFT.PerturbationTheory.WickContraction.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.PerturbationTheory.FieldSpecification.Basic

Wick contractions

@[expose] public section

Given a natural number n, which will correspond to the number of fields needing contracting, a Wick contraction is a finite set of pairs of Fin n (numbers 0, ..., n-1), such that no element of Fin n occurs in more than one pair. The pairs are the positions of fields we 'contract' together.

def WickContraction (n : ℕ) : Type :=
  {f : Finset ((Finset (Fin n))) // (∀ a ∈ f, a.card = 2) ∧
    (∀ a ∈ f, ∀ b ∈ f, a = b ∨ Disjoint a b)}

Wick contractions are decidable.

instance : DecidableEq (WickContraction n) := Subtype.instDecidableEq

The contraction consisting of no contracted pairs.

def empty : WickContraction n := ⟨∅, by𝓕:FieldSpecificationn:ℕc:WickContraction n⊢ ∀ a ∈ ∅, a.card = 2 simpAll goals completed! 🐙, by𝓕:FieldSpecificationn:ℕc:WickContraction n⊢ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b ∨ Disjoint a b simpAll goals completed! 🐙⟩



set_option backward.isDefEq.respectTransparency false in
lemma card_zero_iff_empty (c : WickContraction n) : c.1.card = 0 ↔ c = empty := byn:ℕc:WickContraction n⊢ (↑c).card = 0 ↔ c = empty
  rw [Subtype.ext_iff,n:ℕc:WickContraction n⊢ (↑c).card = 0 ↔ ↑c = ↑emptyAll goals completed! 🐙 Finset.card_eq_zero,n:ℕc:WickContraction n⊢ ↑c = ∅ ↔ ↑c = ↑emptyAll goals completed! 🐙 emptyn:ℕc:WickContraction n⊢ ↑c = ∅ ↔ ↑c = ↑⟨∅, ⋯⟩All goals completed! 🐙]All goals completed! 🐙

lemma exists_pair_of_not_eq_empty (c : WickContraction n) (h : c ≠ empty) :
    ∃ i j, {i, j} ∈ c.1 := byn:ℕc:WickContraction nh:c ≠ empty⊢ ∃ i j, {i, j} ∈ ↑c
  obtain ⟨a, ha⟩ := Finset.nonempty_iff_ne_empty.mpr fun hc => h (Subtype.ext hc)n:ℕc:WickContraction nh:c ≠ emptya:Finset (Fin n)ha:a ∈ ↑c⊢ ∃ i j, {i, j} ∈ ↑c
  obtain ⟨i, j, -, rfl⟩ := Finset.card_eq_two.mp (c.2.1 a ha)n:ℕc:WickContraction nh:c ≠ emptyi:Fin nj:Fin nha:{i, j} ∈ ↑c⊢ ∃ i j, {i, j} ∈ ↑c
  exact ⟨i, j, ha⟩All goals completed! 🐙

The equivalence between WickContraction n and WickContraction m derived from a propositional equality of n and m.

def congr : {n m : ℕ} → (h : n = m) → WickContraction n ≃ WickContraction m
  | n, .(n), rfl => Equiv.refl _

              @[simp]
lemma congr_refl : c.congr rfl = c := rfl@[simp]
lemma card_congr {n m : ℕ} (h : n = m) (c : WickContraction n) :
    (congr h c).1.card = c.1.card := byn:ℕm:ℕh:n = mc:WickContraction n⊢ (↑((congr h) c)).card = (↑c).card
  subst hn:ℕc:WickContraction n⊢ (↑((congr ⋯) c)).card = (↑c).card
  simpAll goals completed! 🐙lemma congr_contractions {n m : ℕ} (h : n = m) (c : WickContraction n) :
    ((congr h) c).1 = Finset.map (Finset.mapEmbedding (finCongr h)).toEmbedding c.1 := byn:ℕm:ℕh:n = mc:WickContraction n⊢ ↑((congr h) c) = Finset.map (Finset.mapEmbedding (finCongr h).toEmbedding).toEmbedding ↑c
  subst hn:ℕc:WickContraction n⊢ ↑((congr ⋯) c) = Finset.map (Finset.mapEmbedding (finCongr ⋯).toEmbedding).toEmbedding ↑c
  ext an:ℕc:WickContraction na:Finset (Fin n)⊢ a ∈ ↑((congr ⋯) c) ↔ a ∈ Finset.map (Finset.mapEmbedding (finCongr ⋯).toEmbedding).toEmbedding ↑c
  simp only [congr_refl, Finset.mem_map, RelEmbedding.coe_toEmbedding, finCongr_refl,
    Equiv.refl_toEmbedding]n:ℕc:WickContraction na:Finset (Fin n)⊢ a ∈ ↑c ↔ ∃ a_1 ∈ ↑c, (Finset.mapEmbedding (Function.Embedding.refl (Fin n))) a_1 = a
  exact ⟨fun ha => ⟨a, ha, Finset.map_refl⟩,
    fun ⟨b, hb, hab⟩ => (Finset.map_refl.symm.trans hab) ▸ hb⟩All goals completed! 🐙@[simp]
lemma congr_trans {n m o : ℕ} (h1 : n = m) (h2 : m = o) :
    (congr h1).trans (congr h2) = congr (h1.trans h2) := byn:ℕm:ℕo:ℕh1:n = mh2:m = o⊢ (congr h1).trans (congr h2) = congr ⋯
  subst h1 h2n:ℕ⊢ (congr ⋯).trans (congr ⋯) = congr ⋯
  simp [congr]All goals completed! 🐙@[simp]
lemma congr_trans_apply {n m o : ℕ} (h1 : n = m) (h2 : m = o) (c : WickContraction n) :
    (congr h2) ((congr h1) c) = congr (h1.trans h2) c := byn:ℕm:ℕo:ℕh1:n = mh2:m = oc:WickContraction n⊢ (congr h2) ((congr h1) c) = (congr ⋯) c
  subst h1 h2n:ℕc:WickContraction n⊢ (congr ⋯) ((congr ⋯) c) = (congr ⋯) c
  simpAll goals completed! 🐙lemma mem_congr_iff {n m : ℕ} (h : n = m) {c : WickContraction n } {a : Finset (Fin m)} :
    a ∈ (congr h c).1 ↔ Finset.map (finCongr h.symm).toEmbedding a ∈ c.1 := byn:ℕm:ℕh:n = mc:WickContraction na:Finset (Fin m)⊢ a ∈ ↑((congr h) c) ↔ Finset.map (finCongr ⋯).toEmbedding a ∈ ↑c
  subst hn:ℕc:WickContraction na:Finset (Fin n)⊢ a ∈ ↑((congr ⋯) c) ↔ Finset.map (finCongr ⋯).toEmbedding a ∈ ↑c
  simpAll goals completed! 🐙

Given a contracted pair in c : WickContraction n the contracted pair in congr h c.

def congrLift {n m : ℕ} (h : n = m) {c : WickContraction n} (a : c.1) : (congr h c).1 :=
  ⟨a.1.map (finCongr h).toEmbedding, by𝓕:FieldSpecificationn✝:ℕc✝:WickContraction n✝n:ℕm:ℕh:n = mc:WickContraction na:↥↑c⊢ Finset.map (finCongr h).toEmbedding ↑a ∈ ↑((congr h) c) aesopAll goals completed! 🐙⟩

              @[simp]
lemma congrLift_rfl {n : ℕ} {c : WickContraction n} :
    c.congrLift rfl = id := byn:ℕc:WickContraction n⊢ congrLift ⋯ = id
  funext an:ℕc:WickContraction na:↥↑c⊢ congrLift ⋯ a = id a
  simp [congrLift]All goals completed! 🐙lemma congrLift_injective {n m : ℕ} {c : WickContraction n} (h : n = m) :
    Function.Injective (c.congrLift h) := byn:ℕm:ℕc:WickContraction nh:n = m⊢ Function.Injective (congrLift h)
  subst hn:ℕc:WickContraction n⊢ Function.Injective (congrLift ⋯)
  simpa using Function.injective_idAll goals completed! 🐙lemma congrLift_surjective {n m : ℕ} {c : WickContraction n} (h : n = m) :
    Function.Surjective (c.congrLift h) := byn:ℕm:ℕc:WickContraction nh:n = m⊢ Function.Surjective (congrLift h)
  subst hn:ℕc:WickContraction n⊢ Function.Surjective (congrLift ⋯)
  simp [Function.surjective_id]All goals completed! 🐙lemma congrLift_bijective {n m : ℕ} {c : WickContraction n} (h : n = m) :
    Function.Bijective (c.congrLift h) :=
  ⟨c.congrLift_injective h, c.congrLift_surjective h⟩

Given a contracted pair in c : WickContraction n the contracted pair in congr h c.

def congrLiftInv {n m : ℕ} (h : n = m) {c : WickContraction n} (a : (congr h c).1) : c.1 :=
  ⟨a.1.map (finCongr h.symm).toEmbedding, by𝓕:FieldSpecificationn✝:ℕc✝:WickContraction n✝n:ℕm:ℕh:n = mc:WickContraction na:↥↑((congr h) c)⊢ Finset.map (finCongr ⋯).toEmbedding ↑a ∈ ↑c aesopAll goals completed! 🐙⟩

lemma congrLiftInv_rfl {n : ℕ} {c : WickContraction n} :
    c.congrLiftInv rfl = id := byn:ℕc:WickContraction n⊢ congrLiftInv ⋯ = id
  funext an:ℕc:WickContraction na:↥↑((congr ⋯) c)⊢ congrLiftInv ⋯ a = id a
  simp [congrLiftInv]All goals completed! 🐙

lemma eq_filter_mem_self : c.1 = Finset.filter (fun x => x ∈ c.1) Finset.univ :=
  (Finset.filter_univ_mem c.1).symm

For a contraction c : WickContraction n and i : Fin n the j such that {i, j} is a contracted pair in c. If such an j does not exist, this returns none.

def getDual? (i : Fin n) : Option (Fin n) := Fin.find? (fun j => {i, j} ∈ c.1)

              lemma getDual?_congr {n m : ℕ} (h : n = m) (c : WickContraction n) (i : Fin m) :
    (congr h c).getDual? i = Option.map (finCongr h) (c.getDual? (finCongr h.symm i)) := byn:ℕm:ℕh:n = mc:WickContraction ni:Fin m⊢ ((congr h) c).getDual? i = Option.map (⇑(finCongr h)) (c.getDual? ((finCongr ⋯) i))
  subst hn:ℕc:WickContraction ni:Fin n⊢ ((congr ⋯) c).getDual? i = Option.map (⇑(finCongr ⋯)) (c.getDual? ((finCongr ⋯) i))
  simpAll goals completed! 🐙lemma getDual?_congr_get {n m : ℕ} (h : n = m) (c : WickContraction n) (i : Fin m)
    (hg : ((congr h c).getDual? i).isSome) :
    ((congr h c).getDual? i).get hg =
    (finCongr h ((c.getDual? (finCongr h.symm i)).get (by𝓕:FieldSpecificationn✝:ℕc✝:WickContraction n✝n:ℕm:ℕh:n = mc:WickContraction ni:Fin mhg:(((congr h) c).getDual? i).isSome = true⊢ (c.getDual? ((finCongr ⋯) i)).isSome = true simpa [getDual?_congr] using hgAll goals completed! 🐙))) := byn:ℕm:ℕh:n = mc:WickContraction ni:Fin mhg:(((congr h) c).getDual? i).isSome = true⊢ (((congr h) c).getDual? i).get hg = (finCongr h) ((c.getDual? ((finCongr ⋯) i)).get ⋯)
  simpa only [getDual?_congr] using Option.get_mapAll goals completed! 🐙

lemma getDual?_eq_some_iff_mem (i j : Fin n) :
    c.getDual? i = some j ↔ {i, j} ∈ c.1 := byn:ℕc:WickContraction ni:Fin nj:Fin n⊢ c.getDual? i = some j ↔ {i, j} ∈ ↑c
  rw [getDual?,n:ℕc:WickContraction ni:Fin nj:Fin n⊢ (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = some j ↔ {i, j} ∈ ↑cn:ℕc:WickContraction ni:Fin nj:Fin n⊢ (decide ({i, j} ∈ ↑c) = true ∧ ∀ j_1 < j, decide ({i, j_1} ∈ ↑c) = false) ↔ {i, j} ∈ ↑c Fin.find?_eq_some_iffn:ℕc:WickContraction ni:Fin nj:Fin n⊢ (decide ({i, j} ∈ ↑c) = true ∧ ∀ j_1 < j, decide ({i, j_1} ∈ ↑c) = false) ↔ {i, j} ∈ ↑cn:ℕc:WickContraction ni:Fin nj:Fin n⊢ (decide ({i, j} ∈ ↑c) = true ∧ ∀ j_1 < j, decide ({i, j_1} ∈ ↑c) = false) ↔ {i, j} ∈ ↑c]n:ℕc:WickContraction ni:Fin nj:Fin n⊢ (decide ({i, j} ∈ ↑c) = true ∧ ∀ j_1 < j, decide ({i, j_1} ∈ ↑c) = false) ↔ {i, j} ∈ ↑c
  refine ⟨fun h => byn:ℕc:WickContraction ni:Fin nj:Fin nh:decide ({i, j} ∈ ↑c) = true ∧ ∀ j_1 < j, decide ({i, j_1} ∈ ↑c) = false⊢ {i, j} ∈ ↑c simpa using h.1All goals completed! 🐙, fun h => ⟨byn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑c⊢ decide ({i, j} ∈ ↑c) = true simpa using hAll goals completed! 🐙, fun k hkj => ?_⟩⟩
  simp only [decide_eq_false_iff_not]n:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < j⊢ {i, k} ∉ ↑c
  intro hkn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑c⊢ False
  rcases c.2.2 _ h _ hk with heq | hdisjinln:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}⊢ Falseinrn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑chdisj:Disjoint {i, j} {i, k}⊢ False
  ·inln:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}⊢ False have hkm : k = i ∨ k = j := byn:ℕc:WickContraction ni:Fin nj:Fin n⊢ c.getDual? i = some j ↔ {i, j} ∈ ↑cinln:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}hkm:k = i ∨ k = j⊢ False simpa using (Finset.ext_iff.mp heq k).mpr (byn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}⊢ k ∈ {i, k}inln:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}hkm:k = i ∨ k = j⊢ False simpAll goals completed! 🐙inln:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}hkm:k = i ∨ k = j⊢ False)inln:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑cheq:{i, j} = {i, k}hkm:k = i ∨ k = j⊢ False
    rcases hkm with rfl | rflinl.inln:ℕc:WickContraction nj:Fin nk:Fin nhkj:k < jh:{k, j} ∈ ↑chk:{k, k} ∈ ↑cheq:{k, j} = {k, k}⊢ Falseinl.inrn:ℕc:WickContraction ni:Fin nk:Fin nhk:{i, k} ∈ ↑ch:{i, k} ∈ ↑chkj:k < kheq:{i, k} = {i, k}⊢ False
    ·inl.inln:ℕc:WickContraction nj:Fin nk:Fin nhkj:k < jh:{k, j} ∈ ↑chk:{k, k} ∈ ↑cheq:{k, j} = {k, k}⊢ False simpa using c.2.1 _ hkAll goals completed! 🐙
    ·inl.inrn:ℕc:WickContraction ni:Fin nk:Fin nhk:{i, k} ∈ ↑ch:{i, k} ∈ ↑chkj:k < kheq:{i, k} = {i, k}⊢ False omegaAll goals completed! 🐙
  ·inrn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑ck:Fin nhkj:k < jhk:{i, k} ∈ ↑chdisj:Disjoint {i, j} {i, k}⊢ False simpa using Finset.disjoint_left.mp hdisj (Finset.mem_insert_self i {j})All goals completed! 🐙

@[simp]
lemma getDual?_one_eq_none (c : WickContraction 1) (i : Fin 1) : c.getDual? i = none := byc:WickContraction 1i:Fin 1⊢ c.getDual? i = none
  by_contra hc:WickContraction 1i:Fin 1h:¬c.getDual? i = none⊢ False
  obtain ⟨a, ha⟩ := Option.ne_none_iff_exists'.mp hc:WickContraction 1i:Fin 1h:¬c.getDual? i = nonea:Fin 1ha:c.getDual? i = some a⊢ False
  rw [getDual?_eq_some_iff_memc:WickContraction 1i:Fin 1h:¬c.getDual? i = nonea:Fin 1ha:{i, a} ∈ ↑c⊢ Falsec:WickContraction 1i:Fin 1h:¬c.getDual? i = nonea:Fin 1ha:{i, a} ∈ ↑c⊢ False] at hac:WickContraction 1i:Fin 1h:¬c.getDual? i = nonea:Fin 1ha:{i, a} ∈ ↑c⊢ False
  simpa [show a = i byc:WickContraction 1i:Fin 1⊢ c.getDual? i = none omegaAll goals completed! 🐙] using c.2.1 _ ha

@[simp]
lemma getDual?_get_self_mem (i : Fin n) (h : (c.getDual? i).isSome) :
    {(c.getDual? i).get h, i} ∈ c.1 := byn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ {(c.getDual? i).get h, i} ∈ ↑c
  rw [@Finset.pair_comm,n:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ {i, (c.getDual? i).get h} ∈ ↑cAll goals completed! 🐙 ← getDual?_eq_some_iff_mem,n:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ c.getDual? i = some ((c.getDual? i).get h)All goals completed! 🐙 Option.some_getn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ c.getDual? i = c.getDual? iAll goals completed! 🐙]All goals completed! 🐙

@[simp]
lemma self_getDual?_get_mem (i : Fin n) (h : (c.getDual? i).isSome) :
    {i, (c.getDual? i).get h} ∈ c.1 := byn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ {i, (c.getDual? i).get h} ∈ ↑c
  rw [← getDual?_eq_some_iff_mem,n:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ c.getDual? i = some ((c.getDual? i).get h)All goals completed! 🐙 Option.some_getn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ c.getDual? i = c.getDual? iAll goals completed! 🐙]All goals completed! 🐙

lemma getDual?_eq_some_neq (i j : Fin n) (h : c.getDual? i = some j) :
    ¬ i = j := byn:ℕc:WickContraction ni:Fin nj:Fin nh:c.getDual? i = some j⊢ ¬i = j
  rw [getDual?_eq_some_iff_memn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑c⊢ ¬i = jn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑c⊢ ¬i = j] at hn:ℕc:WickContraction ni:Fin nj:Fin nh:{i, j} ∈ ↑c⊢ ¬i = j
  rintro rfln:ℕc:WickContraction ni:Fin nh:{i, i} ∈ ↑c⊢ False
  simpa using c.2.1 _ hAll goals completed! 🐙@[simp]
lemma self_ne_getDual?_get (i : Fin n) (h : (c.getDual? i).isSome) :
    ¬ i = (c.getDual? i).get h :=
  c.getDual?_eq_some_neq _ _ (Option.some_get h).symm@[simp]
lemma getDual?_get_self_neq (i : Fin n) (h : (c.getDual? i).isSome) :
    ¬ (c.getDual? i).get h = i :=
  Ne.symm (c.self_ne_getDual?_get i h)

lemma getDual?_isSome_iff (i : Fin n) : (c.getDual? i).isSome ↔ ∃ (a : c.1), i ∈ a.1 := byn:ℕc:WickContraction ni:Fin n⊢ (c.getDual? i).isSome = true ↔ ∃ a, i ∈ ↑a
  simp only [Option.isSome_iff_exists, getDual?_eq_some_iff_mem]n:ℕc:WickContraction ni:Fin n⊢ (∃ a, {i, a} ∈ ↑c) ↔ ∃ a, i ∈ ↑a
  refine ⟨fun ⟨j, hj⟩ => ⟨⟨_, hj⟩, Finset.mem_insert_self ..⟩, fun ⟨a, ha⟩ => ?_⟩n:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cha:i ∈ ↑a⊢ ∃ a, {i, a} ∈ ↑c
  obtain ⟨x, y, -, hxy⟩ := Finset.card_eq_two.mp (c.2.1 a a.2)n:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cha:i ∈ ↑ax:Fin ny:Fin nhxy:↑a = {x, y}⊢ ∃ a, {i, a} ∈ ↑c
  rw [hxyn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin ny:Fin nha:i ∈ {x, y}hxy:↑a = {x, y}⊢ ∃ a, {i, a} ∈ ↑cn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin ny:Fin nha:i ∈ {x, y}hxy:↑a = {x, y}⊢ ∃ a, {i, a} ∈ ↑c] at han:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin ny:Fin nha:i ∈ {x, y}hxy:↑a = {x, y}⊢ ∃ a, {i, a} ∈ ↑c
  simp only [Finset.mem_insert, Finset.mem_singleton] at han:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin ny:Fin nhxy:↑a = {x, y}ha:i = x ∨ i = y⊢ ∃ a, {i, a} ∈ ↑c
  rcases ha with rfl | rflinln:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cy:Fin nhxy:↑a = {i, y}⊢ ∃ a, {i, a} ∈ ↑cinrn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin nhxy:↑a = {x, i}⊢ ∃ a, {i, a} ∈ ↑c
  ·inln:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cy:Fin nhxy:↑a = {i, y}⊢ ∃ a, {i, a} ∈ ↑c exact ⟨y, hxy ▸ a.2⟩All goals completed! 🐙
  ·inrn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin nhxy:↑a = {x, i}⊢ ∃ a, {i, a} ∈ ↑c rw [Finset.pair_comminrn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin nhxy:↑a = {i, x}⊢ ∃ a, {i, a} ∈ ↑cinrn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin nhxy:↑a = {i, x}⊢ ∃ a, {i, a} ∈ ↑c] at hxyinrn:ℕc:WickContraction ni:Fin nx✝:∃ a, i ∈ ↑aa:↥↑cx:Fin nhxy:↑a = {i, x}⊢ ∃ a, {i, a} ∈ ↑c
    exact ⟨x, hxy ▸ a.2⟩All goals completed! 🐙lemma getDual?_isSome_of_mem (a : c.1) (i : a.1) : (c.getDual? i).isSome :=
  (c.getDual?_isSome_iff i).mpr ⟨a, i.2⟩@[simp]
lemma getDual?_getDual?_get_get (i : Fin n) (h : (c.getDual? i).isSome) :
    c.getDual? ((c.getDual? i).get h) = some i := byn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ c.getDual? ((c.getDual? i).get h) = some i
  simp [getDual?_eq_some_iff_mem]All goals completed! 🐙lemma getDual?_getDual?_get_isSome (i : Fin n) (h : (c.getDual? i).isSome) :
    (c.getDual? ((c.getDual? i).get h)).isSome := byn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ (c.getDual? ((c.getDual? i).get h)).isSome = true
  simpAll goals completed! 🐙lemma getDual?_getDual?_get_not_none (i : Fin n) (h : (c.getDual? i).isSome) :
    ¬ (c.getDual? ((c.getDual? i).get h)) = none := byn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ ¬c.getDual? ((c.getDual? i).get h) = none
  simpAll goals completed! 🐙

Extracting parts from a contraction.

The smallest of the two positions in a contracted pair given a Wick contraction.

def fstFieldOfContract (c : WickContraction n) (a : c.1) : Fin n :=
  (a.1.sort (· ≤ ·)).head (by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ ((↑a).sort fun x1 x2 => x1 ≤ x2) ≠ []
    have hx : (a.1.sort (fun x1 x2 => x1 ≤ x2)).length = a.1.card := Finset.length_sort ..𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑chx:((↑a).sort fun x1 x2 => x1 ≤ x2).length = (↑a).card⊢ ((↑a).sort fun x1 x2 => x1 ≤ x2) ≠ []
    by_contra hn𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑chx:((↑a).sort fun x1 x2 => x1 ≤ x2).length = (↑a).cardhn:((↑a).sort fun x1 x2 => x1 ≤ x2) = []⊢ False
    simp only [hn, List.length_nil, c.2.1 a.1 a.2, OfNat.zero_ne_ofNat] at hxAll goals completed! 🐙)

@[simp]
lemma fstFieldOfContract_congr {n m : ℕ} (h : n = m) (c : WickContraction n) (a : c.1) :
    (congr h c).fstFieldOfContract (c.congrLift h a) = (finCongr h) (c.fstFieldOfContract a) := byn:ℕm:ℕh:n = mc:WickContraction na:↥↑c⊢ ((congr h) c).fstFieldOfContract (congrLift h a) = (finCongr h) (c.fstFieldOfContract a)
  subst hn:ℕc:WickContraction na:↥↑c⊢ ((congr ⋯) c).fstFieldOfContract (congrLift ⋯ a) = (finCongr ⋯) (c.fstFieldOfContract a)
  simp [congr]All goals completed! 🐙

The largest of the two positions in a contracted pair given a Wick contraction.

def sndFieldOfContract (c : WickContraction n) (a : c.1) : Fin n :=
  (a.1.sort (· ≤ ·)).tail.head (by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ ((↑a).sort fun x1 x2 => x1 ≤ x2).tail ≠ []
    have hx : (a.1.sort (fun x1 x2 => x1 ≤ x2)).length = a.1.card := Finset.length_sort ..𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑chx:((↑a).sort fun x1 x2 => x1 ≤ x2).length = (↑a).card⊢ ((↑a).sort fun x1 x2 => x1 ≤ x2).tail ≠ []
    by_contra hn𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑chx:((↑a).sort fun x1 x2 => x1 ≤ x2).length = (↑a).cardhn:((↑a).sort fun x1 x2 => x1 ≤ x2).tail = []⊢ False
    have hn := congrArg List.length hn𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑chx:((↑a).sort fun x1 x2 => x1 ≤ x2).length = (↑a).cardhn✝:((↑a).sort fun x1 x2 => x1 ≤ x2).tail = []hn:((↑a).sort fun x1 x2 => x1 ≤ x2).tail.length = [].length⊢ False
    simp [c.2.1] at hnAll goals completed! 🐙)

              @[simp]
lemma sndFieldOfContract_congr {n m : ℕ} (h : n = m) (c : WickContraction n) (a : c.1) :
    (congr h c).sndFieldOfContract (c.congrLift h a) = (finCongr h) (c.sndFieldOfContract a) := byn:ℕm:ℕh:n = mc:WickContraction na:↥↑c⊢ ((congr h) c).sndFieldOfContract (congrLift h a) = (finCongr h) (c.sndFieldOfContract a)
  subst hn:ℕc:WickContraction na:↥↑c⊢ ((congr ⋯) c).sndFieldOfContract (congrLift ⋯ a) = (finCongr ⋯) (c.sndFieldOfContract a)
  simp [congr]All goals completed! 🐙

lemma finset_eq_fstFieldOfContract_sndFieldOfContract (c : WickContraction n) (a : c.1) :
    a.1 = {c.fstFieldOfContract a, c.sndFieldOfContract a} := byn:ℕc:WickContraction na:↥↑c⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
  suffices h : ∀ x y : Fin n, x < y → a.1 = {x, y} →
      a.1 = {c.fstFieldOfContract a, c.sndFieldOfContract a} byn:ℕc:WickContraction na:↥↑ch:∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
    obtain ⟨x, y, hxy, ha⟩ := Finset.card_eq_two.mp (c.2.1 a.1 a.2)n:ℕc:WickContraction na:↥↑ch:∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}x:Fin ny:Fin nhxy:x ≠ yha:↑a = {x, y}⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
    rcases lt_or_gt_of_ne hxy with h' | h'inln:ℕc:WickContraction na:↥↑ch:∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}x:Fin ny:Fin nhxy:x ≠ yha:↑a = {x, y}h':x < y⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}inrn:ℕc:WickContraction na:↥↑ch:∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}x:Fin ny:Fin nhxy:x ≠ yha:↑a = {x, y}h':y < x⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
    ·inln:ℕc:WickContraction na:↥↑ch:∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}x:Fin ny:Fin nhxy:x ≠ yha:↑a = {x, y}h':x < y⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a} exact h x y h' haAll goals completed! 🐙n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
    ·inrn:ℕc:WickContraction na:↥↑ch:∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}x:Fin ny:Fin nhxy:x ≠ yha:↑a = {x, y}h':y < x⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a} exact h y x h' (ha.trans (Finset.pair_comm x y))n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑c⊢ ∀ (x y : Fin n), x < y → ↑a = {x, y} → ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
  intro x y hxy han:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
  have h1 : ∀ b ∈ ({y} : Finset (Fin n)), x ≤ b := by simp [hxy.le]n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ b⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ b⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
  have hs : a.1.sort (· ≤ ·) = [x, y] := by
    rw [ha,n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ b⊢ ({x, y}.sort fun x1 x2 => x1 ≤ x2) = [x, y]n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a} Finset.sort_insert _ h1 (byn:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ b⊢ x ∉ {y}n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a} simp [hxy.ne]All goals completed! 🐙n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}), Finset.sort_singletonn:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ b⊢ [x, y] = [x, y]n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}]n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}
  rw [han:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ {x, y} = {c.fstFieldOfContract a, c.sndFieldOfContract a}n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ {x, y} = {c.fstFieldOfContract a, c.sndFieldOfContract a}]n:ℕc:WickContraction na:↥↑cx:Fin ny:Fin nhxy:x < yha:↑a = {x, y}h1:∀ b ∈ {y}, x ≤ bhs:((↑a).sort fun x1 x2 => x1 ≤ x2) = [x, y]⊢ {x, y} = {c.fstFieldOfContract a, c.sndFieldOfContract a}
  simp [fstFieldOfContract, sndFieldOfContract, hs]All goals completed! 🐙lemma fstFieldOfContract_ne_sndFieldOfContract (c : WickContraction n) (a : c.1) :
    c.fstFieldOfContract a ≠ c.sndFieldOfContract a := byn:ℕc:WickContraction na:↥↑c⊢ c.fstFieldOfContract a ≠ c.sndFieldOfContract a
  by_contra hnn:ℕc:WickContraction na:↥↑chn:c.fstFieldOfContract a = c.sndFieldOfContract a⊢ False
  simpa [c.finset_eq_fstFieldOfContract_sndFieldOfContract a, hn] using c.2.1 a.1 a.2All goals completed! 🐙lemma fstFieldOfContract_le_sndFieldOfContract (c : WickContraction n) (a : c.1) :
    c.fstFieldOfContract a ≤ c.sndFieldOfContract a :=
  (Finset.pairwise_sort ..).rel_head_tail (List.head_mem _)lemma fstFieldOfContract_lt_sndFieldOfContract (c : WickContraction n) (a : c.1) :
    c.fstFieldOfContract a < c.sndFieldOfContract a :=
  lt_of_le_of_ne (c.fstFieldOfContract_le_sndFieldOfContract a)
    (c.fstFieldOfContract_ne_sndFieldOfContract a)@[simp]
lemma fstFieldOfContract_mem (c : WickContraction n) (a : c.1) :
    c.fstFieldOfContract a ∈ a.1 := byn:ℕc:WickContraction na:↥↑c⊢ c.fstFieldOfContract a ∈ ↑a
  simp [finset_eq_fstFieldOfContract_sndFieldOfContract]All goals completed! 🐙lemma fstFieldOfContract_getDual?_isSome (c : WickContraction n) (a : c.1) :
    (c.getDual? (c.fstFieldOfContract a)).isSome :=
  (c.getDual?_isSome_iff _).mpr ⟨a, fstFieldOfContract_mem c a⟩@[simp]
lemma fstFieldOfContract_getDual? (c : WickContraction n) (a : c.1) :
    c.getDual? (c.fstFieldOfContract a) = some (c.sndFieldOfContract a) := byn:ℕc:WickContraction na:↥↑c⊢ c.getDual? (c.fstFieldOfContract a) = some (c.sndFieldOfContract a)
  simp [getDual?_eq_some_iff_mem, ← finset_eq_fstFieldOfContract_sndFieldOfContract]All goals completed! 🐙@[simp]
lemma sndFieldOfContract_mem (c : WickContraction n) (a : c.1) :
    c.sndFieldOfContract a ∈ a.1 := byn:ℕc:WickContraction na:↥↑c⊢ c.sndFieldOfContract a ∈ ↑a
  simp [finset_eq_fstFieldOfContract_sndFieldOfContract]All goals completed! 🐙lemma sndFieldOfContract_getDual?_isSome (c : WickContraction n) (a : c.1) :
    (c.getDual? (c.sndFieldOfContract a)).isSome :=
  (c.getDual?_isSome_iff _).mpr ⟨a, sndFieldOfContract_mem c a⟩

@[simp]
lemma sndFieldOfContract_getDual? (c : WickContraction n) (a : c.1) :
    c.getDual? (c.sndFieldOfContract a) = some (c.fstFieldOfContract a) := byn:ℕc:WickContraction na:↥↑c⊢ c.getDual? (c.sndFieldOfContract a) = some (c.fstFieldOfContract a)
  rw [getDual?_eq_some_iff_mem,n:ℕc:WickContraction na:↥↑c⊢ {c.sndFieldOfContract a, c.fstFieldOfContract a} ∈ ↑cn:ℕc:WickContraction na:↥↑c⊢ ↑a ∈ ↑c Finset.pair_comm,n:ℕc:WickContraction na:↥↑c⊢ {c.fstFieldOfContract a, c.sndFieldOfContract a} ∈ ↑cn:ℕc:WickContraction na:↥↑c⊢ ↑a ∈ ↑c ← finset_eq_fstFieldOfContract_sndFieldOfContractn:ℕc:WickContraction na:↥↑c⊢ ↑a ∈ ↑cn:ℕc:WickContraction na:↥↑c⊢ ↑a ∈ ↑c]n:ℕc:WickContraction na:↥↑c⊢ ↑a ∈ ↑c
  exact a.2All goals completed! 🐙

lemma eq_fstFieldOfContract_of_mem (c : WickContraction n) (a : c.1) (i j : Fin n)
    (hi : i ∈ a.1) (hj : j ∈ a.1) (hij : i < j) :
    c.fstFieldOfContract a = i := byn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ ↑ahj:j ∈ ↑ahij:i < j⊢ c.fstFieldOfContract a = i
  have hlt := fstFieldOfContract_lt_sndFieldOfContract c an:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ ↑ahj:j ∈ ↑ahij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = i
  rw [finset_eq_fstFieldOfContract_sndFieldOfContractn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hj:j ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = in:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hj:j ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = i] at hi hjn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hj:j ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = i
  simp only [Finset.mem_insert, Finset.mem_singleton] at hi hjn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahi:i = c.fstFieldOfContract a ∨ i = c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract a⊢ c.fstFieldOfContract a = i
  rcases hi with rfl | rflinln:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.fstFieldOfContract a < j⊢ c.fstFieldOfContract a = c.fstFieldOfContract ainrn:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.sndFieldOfContract a < j⊢ c.fstFieldOfContract a = c.sndFieldOfContract a <;>inln:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.fstFieldOfContract a < j⊢ c.fstFieldOfContract a = c.fstFieldOfContract ainrn:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.sndFieldOfContract a < j⊢ c.fstFieldOfContract a = c.sndFieldOfContract a rcases hj with rfl | rflinr.inln:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.fstFieldOfContract a⊢ c.fstFieldOfContract a = c.sndFieldOfContract ainr.inrn:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = c.sndFieldOfContract a <;>inl.inln:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.fstFieldOfContract a < c.fstFieldOfContract a⊢ c.fstFieldOfContract a = c.fstFieldOfContract ainl.inrn:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = c.fstFieldOfContract ainr.inln:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.fstFieldOfContract a⊢ c.fstFieldOfContract a = c.sndFieldOfContract ainr.inrn:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.sndFieldOfContract a⊢ c.fstFieldOfContract a = c.sndFieldOfContract a omegaAll goals completed! 🐙

lemma eq_sndFieldOfContract_of_mem (c : WickContraction n) (a : c.1) (i j : Fin n)
    (hi : i ∈ a.1) (hj : j ∈ a.1) (hij : i < j) :
    c.sndFieldOfContract a = j := byn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ ↑ahj:j ∈ ↑ahij:i < j⊢ c.sndFieldOfContract a = j
  have hlt := fstFieldOfContract_lt_sndFieldOfContract c an:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ ↑ahj:j ∈ ↑ahij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = j
  rw [finset_eq_fstFieldOfContract_sndFieldOfContractn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hj:j ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = jn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hj:j ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = j] at hi hjn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhi:i ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hj:j ∈ {c.fstFieldOfContract a, c.sndFieldOfContract a}hij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = j
  simp only [Finset.mem_insert, Finset.mem_singleton] at hi hjn:ℕc:WickContraction na:↥↑ci:Fin nj:Fin nhij:i < jhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahi:i = c.fstFieldOfContract a ∨ i = c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract a⊢ c.sndFieldOfContract a = j
  rcases hi with rfl | rflinln:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.fstFieldOfContract a < j⊢ c.sndFieldOfContract a = jinrn:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.sndFieldOfContract a < j⊢ c.sndFieldOfContract a = j <;>inln:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.fstFieldOfContract a < j⊢ c.sndFieldOfContract a = jinrn:ℕc:WickContraction na:↥↑cj:Fin nhlt:c.fstFieldOfContract a < c.sndFieldOfContract ahj:j = c.fstFieldOfContract a ∨ j = c.sndFieldOfContract ahij:c.sndFieldOfContract a < j⊢ c.sndFieldOfContract a = j rcases hj with rfl | rflinr.inln:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.fstFieldOfContract a⊢ c.sndFieldOfContract a = c.fstFieldOfContract ainr.inrn:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = c.sndFieldOfContract a <;>inl.inln:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.fstFieldOfContract a < c.fstFieldOfContract a⊢ c.sndFieldOfContract a = c.fstFieldOfContract ainl.inrn:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.fstFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = c.sndFieldOfContract ainr.inln:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.fstFieldOfContract a⊢ c.sndFieldOfContract a = c.fstFieldOfContract ainr.inrn:ℕc:WickContraction na:↥↑chlt:c.fstFieldOfContract a < c.sndFieldOfContract ahij:c.sndFieldOfContract a < c.sndFieldOfContract a⊢ c.sndFieldOfContract a = c.sndFieldOfContract a omegaAll goals completed! 🐙

As a type, any pair of contractions is equivalent to Fin 2 with 0 being associated with c.fstFieldOfContract a and 1 being associated with c.sndFieldOfContract.


def contractEquivFinTwo (c : WickContraction n) (a : c.1) :
    a ≃ Fin 2 where
  toFun i := if i = c.fstFieldOfContract a then 0 else 1
  invFun i :=
    match i with
    | 0 => ⟨c.fstFieldOfContract a, fstFieldOfContract_mem c a⟩
    | 1 => ⟨c.sndFieldOfContract a, sndFieldOfContract_mem c a⟩
  left_inv i := by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑a⊢ (fun i =>
      match i with
      | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
      | 1 => ⟨c.sndFieldOfContract a, ⋯⟩)
    ((fun i => if ↑i = c.fstFieldOfContract a then 0 else 1) i) =
  i
    simp only [Fin.isValue]𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i
    have hi := i.2𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑ahi:↑i ∈ ↑a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i
    have ha := c.finset_eq_fstFieldOfContract_sndFieldOfContract a𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑ahi:↑i ∈ ↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i
    simp only [ha, Finset.mem_insert, Finset.mem_singleton] at hi𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a ∨ ↑i = c.sndFieldOfContract a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i
    rcases hi with hi | hiinl𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i
    ·inl𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i rw [hiinl𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a⊢ (match if c.fstFieldOfContract a = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinl𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a⊢ (match if c.fstFieldOfContract a = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i]inl𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a⊢ (match if c.fstFieldOfContract a = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i
      simp only [↓reduceIte, Fin.isValue]inl𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.fstFieldOfContract a⊢ ⟨c.fstFieldOfContract a, ⋯⟩ = i
      exact Subtype.ext hi.symmAll goals completed! 🐙
    ·inr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match if ↑i = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i rw [hi,inr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match if c.sndFieldOfContract a = c.fstFieldOfContract a then 0 else 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinr.hnc𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ ¬c.sndFieldOfContract a = c.fstFieldOfContract a if_neginr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinr.hnc𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ ¬c.sndFieldOfContract a = c.fstFieldOfContract ainr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinr.hnc𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ ¬c.sndFieldOfContract a = c.fstFieldOfContract a]inr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  iinr.hnc𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ ¬c.sndFieldOfContract a = c.fstFieldOfContract a
      ·inr𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ (match 1 with
  | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
  | 1 => ⟨c.sndFieldOfContract a, ⋯⟩) =
  i exact Subtype.ext hi.symmAll goals completed! 🐙
      ·inr.hnc𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:↥↑aha:↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}hi:↑i = c.sndFieldOfContract a⊢ ¬c.sndFieldOfContract a = c.fstFieldOfContract a exact Ne.symm <| fstFieldOfContract_ne_sndFieldOfContract c aAll goals completed! 🐙
  right_inv i := by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑ci:Fin 2⊢ (fun i => if ↑i = c.fstFieldOfContract a then 0 else 1)
    ((fun i =>
        match i with
        | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
        | 1 => ⟨c.sndFieldOfContract a, ⋯⟩)
      i) =
  i
    fin_cases i«0»𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ (fun i => if ↑i = c.fstFieldOfContract a then 0 else 1)
    ((fun i =>
        match i with
        | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
        | 1 => ⟨c.sndFieldOfContract a, ⋯⟩)
      ((fun i => i) ⟨0, ⋯⟩)) =
  (fun i => i) ⟨0, ⋯⟩«1»𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ (fun i => if ↑i = c.fstFieldOfContract a then 0 else 1)
    ((fun i =>
        match i with
        | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
        | 1 => ⟨c.sndFieldOfContract a, ⋯⟩)
      ((fun i => i) ⟨1, ⋯⟩)) =
  (fun i => i) ⟨1, ⋯⟩
    ·«0»𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ (fun i => if ↑i = c.fstFieldOfContract a then 0 else 1)
    ((fun i =>
        match i with
        | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
        | 1 => ⟨c.sndFieldOfContract a, ⋯⟩)
      ((fun i => i) ⟨0, ⋯⟩)) =
  (fun i => i) ⟨0, ⋯⟩ simpAll goals completed! 🐙
    ·«1»𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ (fun i => if ↑i = c.fstFieldOfContract a then 0 else 1)
    ((fun i =>
        match i with
        | 0 => ⟨c.fstFieldOfContract a, ⋯⟩
        | 1 => ⟨c.sndFieldOfContract a, ⋯⟩)
      ((fun i => i) ⟨1, ⋯⟩)) =
  (fun i => i) ⟨1, ⋯⟩ simp only [Fin.isValue, Fin.mk_one, ite_eq_right_iff, zero_ne_one, imp_false]«1»𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction na:↥↑c⊢ ¬c.sndFieldOfContract a = c.fstFieldOfContract a
      exact Ne.symm <| fstFieldOfContract_ne_sndFieldOfContract c aAll goals completed! 🐙



lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1)
    (f : a.1 → M) [CommMonoid M] :
    ∏ (x : a), f x = f (⟨c.fstFieldOfContract a, fstFieldOfContract_mem c a⟩)
    * f (⟨c.sndFieldOfContract a, sndFieldOfContract_mem c a⟩) := byn:ℕM:Type u_1c:WickContraction na:↥↑cf:↥↑a → Minst✝:CommMonoid M⊢ ∏ x, f x = f ⟨c.fstFieldOfContract a, ⋯⟩ * f ⟨c.sndFieldOfContract a, ⋯⟩
  rw [← (c.contractEquivFinTwo a).symm.prod_compn:ℕM:Type u_1c:WickContraction na:↥↑cf:↥↑a → Minst✝:CommMonoid M⊢ ∏ i, f ((c.contractEquivFinTwo a).symm i) = f ⟨c.fstFieldOfContract a, ⋯⟩ * f ⟨c.sndFieldOfContract a, ⋯⟩n:ℕM:Type u_1c:WickContraction na:↥↑cf:↥↑a → Minst✝:CommMonoid M⊢ ∏ i, f ((c.contractEquivFinTwo a).symm i) = f ⟨c.fstFieldOfContract a, ⋯⟩ * f ⟨c.sndFieldOfContract a, ⋯⟩]n:ℕM:Type u_1c:WickContraction na:↥↑cf:↥↑a → Minst✝:CommMonoid M⊢ ∏ i, f ((c.contractEquivFinTwo a).symm i) = f ⟨c.fstFieldOfContract a, ⋯⟩ * f ⟨c.sndFieldOfContract a, ⋯⟩
  simp [contractEquivFinTwo]All goals completed! 🐙

For a field specification 𝓕, φs a list of 𝓕.FieldOp and a Wick contraction φsΛ of φs, the Wick contraction φsΛ is said to be GradingCompliant if for every pair in φsΛ the contracted fields are either both fermionic or both bosonic. In other words, in a GradingCompliant Wick contraction if no contracted pairs occur between fermionic and bosonic fields.

def GradingCompliant (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :=
  ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[(φsΛ.fstFieldOfContract a).1]) = (𝓕 |>ₛ φs[(φsΛ.sndFieldOfContract a).1])

lemma gradingCompliant_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs')
    (φsΛ : WickContraction φs.length) :
    GradingCompliant φs φsΛ ↔ GradingCompliant φs' (congr (by𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'φsΛ:WickContraction φs.length⊢ φs.length = φs'.length simp [h]All goals completed! 🐙) φsΛ) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'φsΛ:WickContraction φs.length⊢ GradingCompliant φs φsΛ ↔ GradingCompliant φs' ((congr ⋯) φsΛ)
  subst h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ GradingCompliant φs φsΛ ↔ GradingCompliant φs ((congr ⋯) φsΛ)
  rflAll goals completed! 🐙

An equivalence from the sigma type (a : c.1) × a to the subtype of Fin n consisting of those positions which are contracted.


def sigmaContractedEquiv : (a : c.1) × a ≃ {x : Fin n // (c.getDual? x).isSome} where
  toFun := fun x => ⟨x.2, getDual?_isSome_of_mem c x.fst x.snd⟩
  invFun := fun x => ⟨
    ⟨{x.1, (c.getDual? x.1).get x.2}, self_getDual?_get_mem c (↑x) x.prop⟩,
    ⟨x.1, by𝓕:FieldSpecificationn:ℕc:WickContraction nx:{ x // (c.getDual? x).isSome = true }⊢ ↑x ∈ ↑⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩ simpAll goals completed! 🐙⟩⟩
  left_inv x := by𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑a⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
    have hxa (x1 x2 : (a : c.1) × a) (h1 : x1.1 = x2.1)
      (h2 : x1.2.val = x2.2.val) : x1 = x2 := by
      cases x1mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ax2:(a : ↥↑c) × ↥↑afst✝:↥↑csnd✝:↥↑fst✝h1:⟨fst✝, snd✝⟩.fst = x2.fsth2:↑⟨fst✝, snd✝⟩.snd = ↑x2.snd⊢ ⟨fst✝, snd✝⟩ = x2𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      cases x2mk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑afst✝¹:↥↑csnd✝¹:↥↑fst✝fst✝:↥↑csnd✝:↥↑fst✝h1:⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fsth2:↑⟨fst✝¹, snd✝¹⟩.snd = ↑⟨fst✝, snd✝⟩.snd⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      simp_all only [Sigma.mk.inj_iff, true_and]mk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑afst✝¹:↥↑csnd✝¹:↥↑fst✝fst✝:↥↑csnd✝:↥↑fst✝h1:fst✝¹ = fst✝h2:↑snd✝¹ = ↑snd✝⊢ snd✝¹ ≍ snd✝𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      subst h1mk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑afst✝:↥↑csnd✝¹:↥↑fst✝snd✝:↥↑fst✝h2:↑snd✝¹ = ↑snd✝⊢ snd✝¹ ≍ snd✝𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      rename_i fst snd snd_1mk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑afst:↥↑csnd:↥↑fst✝snd_1:↥↑fst✝h2:↑snd✝¹ = ↑snd✝⊢ snd✝¹ ≍ snd✝𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      simp_all only [heq_eq_eq]mk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑afst:↥↑csnd:↥↑fst✝snd_1:↥↑fst✝h2:↑snd✝¹ = ↑snd✝⊢ snd = snd_1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      obtain ⟨val, property⟩ := fstmk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑aval:Finset (Fin n)property:val ∈ ↑csnd:↥↑⟨val, property⟩snd_1:↥↑⟨val, property⟩h2:↑snd = ↑snd_1⊢ snd = snd_1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      obtain ⟨val_2, property_2⟩ := sndmk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑aval:Finset (Fin n)property:val ∈ ↑csnd_1:↥↑⟨val, property⟩val_2:Fin nproperty_2:val_2 ∈ ↑⟨val, property⟩h2:↑⟨val_2, property_2⟩ = ↑snd_1⊢ ⟨val_2, property_2⟩ = snd_1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      subst h2mk.mk𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑aval:Finset (Fin n)property:val ∈ ↑csnd_1:↥↑⟨val, property⟩property_2:↑snd_1 ∈ ↑⟨val, property⟩⊢ ⟨↑snd_1, property_2⟩ = snd_1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
      simp_all only𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = x
    match x with
    | ⟨a, i⟩ =>𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑a⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩) = ⟨a, i⟩
    apply hxah1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑a⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fsth2𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑a⊢ ↑((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).snd = ↑⟨a, i⟩.snd
    ·h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑a⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst have hc := c.2.2 a.1 a.2 {i.1, (c.getDual? ↑i).get (getDual?_isSome_of_mem c a i)}
        (self_getDual?_get_mem c (↑i) (getDual?_isSome_of_mem c a i))h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst
      have hn : ¬ Disjoint a.1 {i.1, (c.getDual? ↑i).get (getDual?_isSome_of_mem c a i)} := by𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑a⊢ (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) x) = xh1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst
        rw [Finset.disjoint_iff_inter_eq_empty,𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ¬↑a ∩ {↑i, (c.getDual? ↑i).get ⋯} = ∅𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ¬∀ (x : Fin n), x ∉ ↑a ∩ {↑i, (c.getDual? ↑i).get ⋯}h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst @Finset.eq_empty_iff_forall_notMem𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ¬∀ (x : Fin n), x ∉ ↑a ∩ {↑i, (c.getDual? ↑i).get ⋯}𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ¬∀ (x : Fin n), x ∉ ↑a ∩ {↑i, (c.getDual? ↑i).get ⋯}h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst]𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ¬∀ (x : Fin n), x ∉ ↑a ∩ {↑i, (c.getDual? ↑i).get ⋯}h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst
        simp only [Finset.coe_mem, Finset.inter_insert_of_mem, Finset.mem_insert, Finset.mem_inter,
          Finset.mem_singleton, not_or, not_and, not_forall, Decidable.not_not]𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ∃ x, ¬x = ↑i → ∃ (_ : x ∈ ↑a), x = (c.getDual? ↑i).get ⋯h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst
        exact ⟨i, fun x ↦ (x rfl).elim⟩h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fsth1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯} ∨ Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}hn:¬Disjoint ↑a {↑i, (c.getDual? ↑i).get ⋯}⊢ ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).fst = ⟨a, i⟩.fst
      simp_all only [or_false, disjoint_self, Finset.bot_eq_empty, Finset.insert_ne_empty,
        not_false_eq_true]h1𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑ahc:↑a = {↑i, (c.getDual? ↑i).get ⋯}⊢ ⟨{↑i, (c.getDual? ↑i).get ⋯}, ⋯⟩ = a
      exact Subtype.ext (id (Eq.symm hc))All goals completed! 🐙
    ·h2𝓕:FieldSpecificationn:ℕc:WickContraction nx:(a : ↥↑c) × ↥↑ahxa:∀ (x1 x2 : (a : ↥↑c) × ↥↑a), x1.fst = x2.fst → ↑x1.snd = ↑x2.snd → x1 = x2a:↥↑ci:↥↑a⊢ ↑((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x => ⟨↑x.snd, ⋯⟩) ⟨a, i⟩)).snd = ↑⟨a, i⟩.snd simpAll goals completed! 🐙
  right_inv := by𝓕:FieldSpecificationn:ℕc:WickContraction n⊢ Function.RightInverse (fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) fun x => ⟨↑x.snd, ⋯⟩
    intro x𝓕:FieldSpecificationn:ℕc:WickContraction nx:{ x // (c.getDual? x).isSome = true }⊢ (fun x => ⟨↑x.snd, ⋯⟩) ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) x) = x
    cases xmk𝓕:FieldSpecificationn:ℕc:WickContraction nval✝:Fin nproperty✝:(c.getDual? val✝).isSome = true⊢ (fun x => ⟨↑x.snd, ⋯⟩) ((fun x => ⟨⟨{↑x, (c.getDual? ↑x).get ⋯}, ⋯⟩, ⟨↑x, ⋯⟩⟩) ⟨val✝, property✝⟩) = ⟨val✝, property✝⟩
    rflAll goals completed! 🐙