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

Join of contractions

@[expose] public section

Given a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, join φsΛ φsucΛ is defined as the Wick contraction of φs consisting of the contractions in φsΛ and those in φsucΛ.

As an example, for φs = [φ1, φ2, φ3, φ4], φsΛ = {{0, 1}} corresponding to the contraction of φ1 and φ2 in φs and φsucΛ = {{0, 1}} corresponding to the contraction of φ3 and φ4 in [φsΛ]ᵘᶜ = [φ3, φ4], then join φsΛ φsucΛ is the contraction {{0, 1}, {2, 3}} of φs.

𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a ∈ ↑φsucΛb:Finset (Fin [φsΛ]ᵘᶜ.length)hb:b ∈ ↑φsucΛ⊢ a = b ∨ Disjoint a b All goals completed! 🐙⟩
lemma join_congr {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} {φsΛ' : WickContraction φs.length} (h1 : φsΛ = φsΛ') : join φsΛ φsucΛ = join φsΛ' (congr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsΛ':WickContraction φs.lengthh1:φsΛ = φsΛ'⊢ [φsΛ]ᵘᶜ.length = [φsΛ']ᵘᶜ.length All goals completed! 🐙) φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsΛ':WickContraction φs.lengthh1:φsΛ = φsΛ'⊢ φsΛ.join φsucΛ = φsΛ'.join ((congr ⋯) φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ φsΛ.join φsucΛ = φsΛ.join ((congr ⋯) φsucΛ) All goals completed! 🐙

Given a contracting pair within φsΛ the corresponding contracting pair within (join φsΛ φsucΛ).

def joinLiftLeft {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsΛ.1 → (join φsΛ φsucΛ).1 := fun a => ⟨a, 𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ ↑a ∈ ↑(φsΛ.join φsucΛ) All goals completed! 🐙⟩
lemma jointLiftLeft_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLiftLeft _ _ φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ Function.Injective joinLiftLeft 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛb:↥↑φsΛh:joinLiftLeft a = joinLiftLeft b⊢ a = b 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛb:↥↑φsΛh:↑a = ↑b⊢ a = b All goals completed! 🐙

Given a contracting pair within φsucΛ the corresponding contracting pair within (join φsΛ φsucΛ).

def joinLiftRight {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsucΛ.1 → (join φsΛ φsucΛ).1 := fun a => ⟨a.1.map uncontractedListEmd, 𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ Finset.map uncontractedListEmd ↑a ∈ ↑(φsΛ.join φsucΛ) 𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ Finset.map uncontractedListEmd ↑a ∈ ↑φsΛ ∨ ∃ a_1 ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a_1 = Finset.map uncontractedListEmd ↑a 𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ ∃ a_1 ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a_1 = Finset.map uncontractedListEmd ↑a 𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ ↑a ∈ ↑φsucΛ ∧ (Finset.mapEmbedding uncontractedListEmd) ↑a = Finset.map uncontractedListEmd ↑a 𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ (Finset.mapEmbedding uncontractedListEmd) ↑a = Finset.map uncontractedListEmd ↑a All goals completed! 🐙⟩
lemma joinLiftRight_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLiftRight _ _ φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ Function.Injective joinLiftRight 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛb:↥↑φsucΛh:joinLiftRight a = joinLiftRight b⊢ a = b 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛb:↥↑φsucΛh:↑a = ↑b⊢ a = b All goals completed! 🐙lemma jointLiftLeft_disjoint_joinLiftRight {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} (a : φsΛ.1) (b : φsucΛ.1) : Disjoint (@joinLiftLeft _ _ _ φsucΛ a).1 (joinLiftRight b).1 := (uncontractedListEmd_finset_disjoint_left b.1 a.1 a.2).symm𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛb:↥↑φsucΛhn:joinLiftLeft a = joinLiftRight bh1:↑(joinLiftRight b) = ∅⊢ False 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛb:↥↑φsucΛhn:joinLiftLeft a = joinLiftRight bh1:↑(joinLiftRight b) = ∅hj:(↑(joinLiftRight b)).card = 2⊢ False All goals completed! 🐙

The map from contracted pairs of φsΛ and φsucΛ to contracted pairs in (join φsΛ φsucΛ).

def joinLift {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsΛ.1 ⊕ φsucΛ.1 → (join φsΛ φsucΛ).1 := fun a => match a with | Sum.inl a => joinLiftLeft a | Sum.inr a => joinLiftRight a
lemma joinLift_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLift _ _ φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ Function.Injective joinLift 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ ⊕ ↥↑φsucΛb:↥↑φsΛ ⊕ ↥↑φsucΛh:joinLift a = joinLift b⊢ a = b match a, b with 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:↥↑φsΛ ⊕ ↥↑φsucΛb✝:↥↑φsΛ ⊕ ↥↑φsucΛa:↥↑φsΛb:↥↑φsΛh:joinLift (Sum.inl a) = joinLift (Sum.inl b)⊢ Sum.inl a = Sum.inl b All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:↥↑φsΛ ⊕ ↥↑φsucΛb✝:↥↑φsΛ ⊕ ↥↑φsucΛa:↥↑φsucΛb:↥↑φsucΛh:joinLift (Sum.inr a) = joinLift (Sum.inr b)⊢ Sum.inr a = Sum.inr b All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:↥↑φsΛ ⊕ ↥↑φsucΛb✝:↥↑φsΛ ⊕ ↥↑φsucΛa:↥↑φsΛb:↥↑φsucΛh:joinLift (Sum.inl a) = joinLift (Sum.inr b)⊢ Sum.inl a = Sum.inr b All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:↥↑φsΛ ⊕ ↥↑φsucΛb✝:↥↑φsΛ ⊕ ↥↑φsucΛa:↥↑φsucΛb:↥↑φsΛh:joinLift (Sum.inr a) = joinLift (Sum.inl b)⊢ Sum.inr a = Sum.inl b All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 ∈ ↑φsucΛ ∧ Finset.map uncontractedListEmd a2 = ↑a⊢ ∃ a_1, joinLift a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 ∈ ↑φsucΛ ∧ Finset.map uncontractedListEmd a2 = ↑a⊢ joinLift (Sum.inr ⟨a2, ⋯⟩) = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 ∈ ↑φsucΛ ∧ Finset.map uncontractedListEmd a2 = ↑a⊢ ⟨Finset.map uncontractedListEmd a2, ⋯⟩ = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 ∈ ↑φsucΛ ∧ Finset.map uncontractedListEmd a2 = ↑a⊢ ↑⟨Finset.map uncontractedListEmd a2, ⋯⟩ = ↑a All goals completed! 🐙lemma joinLift_bijective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Bijective (@joinLift _ _ φsΛ φsucΛ) := ⟨joinLift_injective, joinLift_surjective⟩𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthf:↥↑(φsΛ.join φsucΛ) → Minst✝:CommMonoid M⊢ ∏ i, f ((Equiv.ofBijective joinLift ⋯) i) = (∏ a, f (joinLiftLeft a)) * ∏ a, f (joinLiftRight a) 𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthf:↥↑(φsΛ.join φsucΛ) → Minst✝:CommMonoid M⊢ (∏ a₁ ∈ (↑φsΛ).attach, f ((Equiv.ofBijective joinLift ⋯) (Sum.inl a₁))) * ∏ a₂ ∈ (↑φsucΛ).attach, f ((Equiv.ofBijective joinLift ⋯) (Sum.inr a₂)) = (∏ a ∈ (↑φsΛ).attach, f (joinLiftLeft a)) * ∏ a ∈ (↑φsucΛ).attach, f (joinLiftRight a) All goals completed! 🐙lemma joinLiftLeft_or_joinLiftRight_of_mem_join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) {a : Finset (Fin φs.length)} (ha : a ∈ (join φsΛ φsucΛ).1) : (∃ b, a = (joinLiftLeft (φsucΛ := φsucΛ) b).1) ∨ (∃ b, a = (joinLiftRight (φsucΛ := φsucΛ) b).1) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑(φsΛ.join φsucΛ)⊢ (∃ b, a = ↑(joinLiftLeft b)) ∨ ∃ b, a = ↑(joinLiftRight b) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛ ∨ ∃ a_1 ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a_1 = a⊢ (∃ b, a = ↑(joinLiftLeft b)) ∨ ∃ b, a = ↑(joinLiftRight b) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛ⊢ (∃ b, a = ↑(joinLiftLeft b)) ∨ ∃ b, a = ↑(joinLiftRight b)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a ∈ ↑φsucΛ⊢ (∃ b, (Finset.mapEmbedding uncontractedListEmd) a = ↑(joinLiftLeft b)) ∨ ∃ b, (Finset.mapEmbedding uncontractedListEmd) a = ↑(joinLiftRight b) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛ⊢ (∃ b, a = ↑(joinLiftLeft b)) ∨ ∃ b, a = ↑(joinLiftRight b) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a ∈ ↑φsucΛ⊢ (∃ b, (Finset.mapEmbedding uncontractedListEmd) a = ↑(joinLiftLeft b)) ∨ ∃ b, (Finset.mapEmbedding uncontractedListEmd) a = ↑(joinLiftRight b) All goals completed! 🐙@[simp] lemma join_fstFieldOfContract_joinLiftRight {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsucΛ.1) : (join φsΛ φsucΛ).fstFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.fstFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ (φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.fstFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) ∈ ↑(joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∈ ↑(joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) ∈ ↑(joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∈ ↑(joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ φsucΛ.fstFieldOfContract a < φsucΛ.sndFieldOfContract a All goals completed! 🐙@[simp] lemma join_sndFieldOfContract_joinLiftRight {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsucΛ.1) : (join φsΛ φsucΛ).sndFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.sndFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ (φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) ∈ ↑(joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∈ ↑(joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) ∈ ↑(joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∈ ↑(joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛ⊢ φsucΛ.fstFieldOfContract a < φsucΛ.sndFieldOfContract a All goals completed! 🐙@[simp] lemma join_fstFieldOfContract_joinLiftLeft {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsΛ.1) : (join φsΛ φsucΛ).fstFieldOfContract (joinLiftLeft a) = (φsΛ.fstFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ (φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a) = φsΛ.fstFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a ∈ ↑(joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.sndFieldOfContract a ∈ ↑(joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a ∈ ↑(joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.sndFieldOfContract a ∈ ↑(joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a All goals completed! 🐙@[simp] lemma join_sndFieldOfContract_joinLift {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsΛ.1) : (join φsΛ φsucΛ).sndFieldOfContract (joinLiftLeft a) = (φsΛ.sndFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ (φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a) = φsΛ.sndFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a ∈ ↑(joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.sndFieldOfContract a ∈ ↑(joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a ∈ ↑(joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.sndFieldOfContract a ∈ ↑(joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsΛ⊢ φsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:Finset (Fin [φsΛ]ᵘᶜ.length)h1':Finset.map uncontractedListEmd a ∉ ↑φsΛa:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a ∈ ↑φsucΛh2:a = a✝⊢ a ∈ ↑φsucΛ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛx:Finset (Fin [φsΛ]ᵘᶜ.length)hx:x ∈ ↑φsucΛhn:Finset.map uncontractedListEmd x = ahdis:Disjoint a a⊢ False 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛx:Finset (Fin [φsΛ]ᵘᶜ.length)hx:x ∈ ↑φsucΛhn:Finset.map uncontractedListEmd x = ahdis:Disjoint a ahcard:a.card = 2⊢ False All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction [empty]ᵘᶜ.lengtha:Finset (Fin φs.length)h:Finset.map (finCongr ⋯).toEmbedding a ∈ ↑φsΛ⊢ Finset.map ((finCongr ⋯).toEmbedding.trans (finCongr ⋯).toEmbedding) a = a All goals completed! 🐙@[simp] lemma join_empty {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : join φsΛ empty = φsΛ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ φsΛ.join empty = φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ ↑(φsΛ.join empty) = ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)⊢ a ∈ ↑(φsΛ.join empty) ↔ a ∈ ↑φsΛ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ (∏ a, ⟨WickAlgebra.timeContract φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a))] φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a))], ⋯⟩) * ∏ a, ⟨WickAlgebra.timeContract φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))] φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))], ⋯⟩ = (∏ x, ⟨WickAlgebra.timeContract φs[↑(φsΛ.fstFieldOfContract x)] φs[↑(φsΛ.sndFieldOfContract x)], ⋯⟩) * ∏ x, ⟨WickAlgebra.timeContract [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract x)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract x)], ⋯⟩ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ ∏ a, ⟨WickAlgebra.timeContract φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))] φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))], ⋯⟩ = ∏ x, ⟨WickAlgebra.timeContract [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract x)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract x)], ⋯⟩ exact Finset.prod_congr rfl fun a _ => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛx✝:a ∈ Finset.univ⊢ ⟨WickAlgebra.timeContract φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))] φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))], ⋯⟩ = ⟨WickAlgebra.timeContract [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract a)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)], ⋯⟩ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ (∏ a, ⟨(superCommute (anPart φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a))])) (ofFieldOp φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a))]), ⋯⟩) * ∏ a, ⟨(superCommute (anPart φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))])) (ofFieldOp φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))]), ⋯⟩ = (∏ x, ⟨(superCommute (anPart φs[↑(φsΛ.fstFieldOfContract x)])) (ofFieldOp φs[↑(φsΛ.sndFieldOfContract x)]), ⋯⟩) * ∏ x, ⟨(superCommute (anPart [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract x)])) (ofFieldOp [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract x)]), ⋯⟩ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ ∏ a, ⟨(superCommute (anPart φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))])) (ofFieldOp φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))]), ⋯⟩ = ∏ x, ⟨(superCommute (anPart [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract x)])) (ofFieldOp [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract x)]), ⋯⟩ exact Finset.prod_congr rfl fun a _ => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:↥↑φsucΛx✝:a ∈ Finset.univ⊢ ⟨(superCommute (anPart φs[↑((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))])) (ofFieldOp φs[↑((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))]), ⋯⟩ = ⟨(superCommute (anPart [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract a)])) (ofFieldOp [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)]), ⋯⟩ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthha:∀ p ∈ ↑φsucΛ, i ∉ pp:Finset (Fin [φsΛ]ᵘᶜ.length)hp:p ∈ ↑φsucΛ⊢ i ∉ p All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthha:∀ p ∈ ↑(φsΛ.join φsucΛ), i ∉ p⊢ ∀ p ∈ ↑φsΛ, i ∉ p 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthha:∀ (p : Finset (Fin φs.length)), (p ∈ ↑φsΛ ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = p) → i ∉ p⊢ ∀ p ∈ ↑φsΛ, i ∉ p 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthha:∀ (p : Finset (Fin φs.length)), (p ∈ ↑φsΛ ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = p) → i ∉ pp:Finset (Fin φs.length)hp:p ∈ ↑φsΛ⊢ i ∉ p All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengthhi:∀ p ∈ ↑(φsΛ.join φsucΛ), uncontractedListEmd j ∉ phi':uncontractedListEmd j ∈ φsΛ.uncontractedp:Finset (Fin [φsΛ]ᵘᶜ.length)hp:p ∈ ↑φsucΛhip:uncontractedListEmd j ∉ Finset.map uncontractedListEmd p⊢ j ∉ p All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ ((φsΛ.join φsucΛ).uncontracted.sort fun x1 x2 => x1 ≤ x2) = (Finset.map uncontractedListEmd φsucΛ.uncontracted).sort fun x1 x2 => x1 ≤ x2𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ (φsΛ.join φsucΛ).uncontracted = Finset.map uncontractedListEmd φsucΛ.uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length⊢ a ∈ (φsΛ.join φsucΛ).uncontracted ↔ a ∈ Finset.map uncontractedListEmd φsucΛ.uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length⊢ a ∈ (φsΛ.join φsucΛ).uncontracted ↔ ∃ a_1 ∈ φsucΛ.uncontracted, uncontractedListEmd a_1 = a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length⊢ a ∈ (φsΛ.join φsucΛ).uncontracted → ∃ a_2 ∈ φsucΛ.uncontracted, uncontractedListEmd a_2 = a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length⊢ (∃ a_1 ∈ φsucΛ.uncontracted, uncontractedListEmd a_1 = a) → a ∈ (φsΛ.join φsucΛ).uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length⊢ a ∈ (φsΛ.join φsucΛ).uncontracted → ∃ a_2 ∈ φsucΛ.uncontracted, uncontractedListEmd a_2 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengthh:a ∈ (φsΛ.join φsucΛ).uncontracted⊢ ∃ a_1 ∈ φsucΛ.uncontracted, uncontractedListEmd a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthha:a ∈ φsucΛ.uncontractedh:uncontractedListEmd a ∈ (φsΛ.join φsucΛ).uncontracted⊢ ∃ a_1 ∈ φsucΛ.uncontracted, uncontractedListEmd a_1 = uncontractedListEmd a All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length⊢ (∃ a_1 ∈ φsucΛ.uncontracted, uncontractedListEmd a_1 = a) → a ∈ (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengthh:∃ a_1 ∈ φsucΛ.uncontracted, uncontractedListEmd a_1 = a⊢ a ∈ (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthha:a ∈ φsucΛ.uncontracted⊢ uncontractedListEmd a ∈ (φsΛ.join φsucΛ).uncontracted All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthb:Fin [φsΛ]ᵘᶜ.lengthh:a < b⊢ uncontractedListEmd a < uncontractedListEmd b All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh1:∀ {n : ℕ} (l1 l2 : List (Fin n)) (h : l1 = l2), l1.get = l2.get ∘ Fin.cast ⋯⊢ (φsΛ.join φsucΛ).uncontractedList.get = ⇑uncontractedListEmd ∘ φsucΛ.uncontractedList.get ∘ Fin.cast ⋯ conv_lhs => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh1:∀ {n : ℕ} (l1 l2 : List (Fin n)) (h : l1 = l2), l1.get = l2.get ∘ Fin.cast ⋯| (List.map (⇑uncontractedListEmd) φsucΛ.uncontractedList).get ∘ Fin.cast ⋯ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh1:∀ {n : ℕ} (l1 l2 : List (Fin n)) (h : l1 = l2), l1.get = l2.get ∘ Fin.cast ⋯i:Fin (φsΛ.join φsucΛ).uncontractedList.length⊢ ↑(((List.map (⇑uncontractedListEmd) φsucΛ.uncontractedList).get ∘ Fin.cast ⋯) i) = ↑((⇑uncontractedListEmd ∘ φsucΛ.uncontractedList.get ∘ Fin.cast ⋯) i) All goals completed! 🐙lemma join_uncontractedListGet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : (join φsΛ φsucΛ).uncontractedListGet = φsucΛ.uncontractedListGet := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ [φsΛ.join φsucΛ]ᵘᶜ = [φsucΛ]ᵘᶜ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ ∀ a ∈ φsucΛ.uncontractedList, φs[↑(uncontractedListEmd a)] = φs[↑φsΛ.uncontractedList[↑a]] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin (List.map φs.get φsΛ.uncontractedList).lengthha:a ∈ φsucΛ.uncontractedList⊢ φs[↑(uncontractedListEmd a)] = φs[↑φsΛ.uncontractedList[↑a]] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin (List.map φs.get φsΛ.uncontractedList).lengthha:a ∈ φsucΛ.uncontractedList⊢ φs[↑((((finCongr ⋯).toEmbedding.trans { toFun := fun i => ⟨φsΛ.uncontractedList[↑i], ⋯⟩, invFun := fun i => ⟨List.idxOf (↑i) φsΛ.uncontractedList, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toEmbedding).trans (Function.Embedding.subtype fun x => x ∈ φsΛ.uncontracted)) a)] = φs[↑φsΛ.uncontractedList[↑a]] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ (⇑uncontractedListEmd ∘ φsucΛ.uncontractedList.get ∘ Fin.cast ⋯) ∘ ⇑(finCongr ⋯) = ⇑(((finCongr ⋯).toEmbedding.trans uncontractedListEmd).trans uncontractedListEmd) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsucΛ':WickContraction [φsΛ.join φsucΛ]ᵘᶜ.lengtha:Finset (Fin [φsucΛ]ᵘᶜ.length)ha':a ∈ ↑((congr ⋯) φsucΛ')ha:(Finset.mapEmbedding uncontractedListEmd) ((Finset.mapEmbedding uncontractedListEmd) a) ∉ ↑φsΛa':↥↑φsucΛ' := congrLiftInv ⋯ ⟨a, ha'⟩⊢ Finset.map ((finCongr ⋯).toEmbedding.trans (finCongr ⋯).toEmbedding) a = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsucΛ':WickContraction [φsΛ.join φsucΛ]ᵘᶜ.lengtha:Finset (Fin [φsucΛ]ᵘᶜ.length)ha':a ∈ ↑((congr ⋯) φsucΛ')ha:(Finset.mapEmbedding uncontractedListEmd) ((Finset.mapEmbedding uncontractedListEmd) a) ∉ ↑φsΛa':↥↑φsucΛ' := congrLiftInv ⋯ ⟨a, ha'⟩⊢ Finset.map (Equiv.refl (Fin [φsucΛ]ᵘᶜ.length)).toEmbedding a = a All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted ↔ i ∈ φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted → i ∈ φsucΛ.uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ i ∈ φsucΛ.uncontracted → uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted → i ∈ φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted⊢ i ∈ φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracteda:Fin [φsΛ]ᵘᶜ.lengthha':uncontractedListEmd a = uncontractedListEmd iha:a ∈ φsucΛ.uncontracted⊢ i ∈ φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracteda:Fin [φsΛ]ᵘᶜ.lengthha:a ∈ φsucΛ.uncontractedha':a = i⊢ i ∈ φsucΛ.uncontracted All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ i ∈ φsucΛ.uncontracted → uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:i ∈ φsucΛ.uncontracted⊢ uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ ¬((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true ↔ ¬(φsucΛ.getDual? i).isSome = true All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthhi:((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true⊢ Finset.map uncontractedListEmd {i, (φsucΛ.getDual? i).get ⋯} = {uncontractedListEmd i, uncontractedListEmd ((φsucΛ.getDual? i).get ⋯)} All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true⊢ some (uncontractedListEmd ((φsucΛ.getDual? i).get ⋯)) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true⊢ ((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true conv_rhs => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true| Option.map (⇑uncontractedListEmd) (some ((φsucΛ.getDual? i).get h)) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true⊢ ((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:¬(φsucΛ.getDual? i).isSome = true⊢ (φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:φsucΛ.getDual? i = none⊢ (φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i) All goals completed! 🐙

Subcontractions and quotient contractions

lemma join_sub_quot (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) : join (subContraction S ha) (quotContraction S ha) = φsΛ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ (subContraction S ha).join (quotContraction S ha) = φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ ↑((subContraction S ha).join (quotContraction S ha)) = ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)⊢ a ∈ ↑((subContraction S ha).join (quotContraction S ha)) ↔ a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)⊢ (a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a) ↔ a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)⊢ (a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a) → a ∈ ↑φsΛ𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)⊢ a ∈ ↑φsΛ → a ∈ ↑(subContraction S ha) ∨ ∃ a_2 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_2 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)⊢ (a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a) → a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a⊢ a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑(subContraction S ha)⊢ a ∈ ↑φsΛ𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a⊢ a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑(subContraction S ha)⊢ a ∈ ↑φsΛ All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a⊢ a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha✝]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S ha✝)⊢ (Finset.mapEmbedding uncontractedListEmd) a ∈ ↑φsΛ All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)⊢ a ∈ ↑φsΛ → a ∈ ↑(subContraction S ha) ∨ ∃ a_2 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_2 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛ⊢ a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛh1:a ∈ ↑(subContraction S ha) ∨ ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S ha)⊢ a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛh1:a ∈ ↑(subContraction S ha)⊢ a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛh1:∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S ha)⊢ a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛh1:a ∈ ↑(subContraction S ha)⊢ a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛh1:∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S ha)⊢ a ∈ ↑(subContraction S ha) ∨ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:Finset (Fin φs.length)h:a ∈ ↑φsΛh1:∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ ↑(quotContraction S ha)⊢ ∃ a_1 ∈ ↑(quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S ⊆ ↑φsΛa:Finset (Fin [subContraction S ha✝]ᵘᶜ.length)ha:a ∈ ↑(quotContraction S ha✝)h:Finset.map uncontractedListEmd a ∈ ↑φsΛ⊢ ∃ a_1 ∈ ↑(quotContraction S ha✝), (Finset.mapEmbedding uncontractedListEmd) a_1 = Finset.map uncontractedListEmd a All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛ⊢ (↑((subContraction S ha).join (quotContraction S ha))).card = (↑φsΛ).card All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ {i, j} ∈ ↑((singleton h).join φsucΛ) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ {j, i} ∈ ↑((singleton h).join φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ {j, i} = {i, j} ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = {j, i} 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ {j, i} = {i, j} All goals completed! 🐙lemma exists_contraction_pair_of_card_ge_zero {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h : 0 < φsΛ.1.card) : ∃ a, a ∈ φsΛ.1 := Finset.card_pos.mp h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:0 < (↑φsΛ).cardhc:GradingCompliant φs φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛφsucΛ:WickContraction [singleton ⋯]ᵘᶜ.length := (congr ⋯) (quotContraction {a} ⋯)h1:(↑(subContraction {a} ⋯)).card + (↑(quotContraction {a} ⋯)).card = (↑φsΛ).card⊢ (↑(quotContraction {a} ⋯)).card + 1 = (↑φsΛ).card 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:0 < (↑φsΛ).cardhc:GradingCompliant φs φsΛa:Finset (Fin φs.length)ha:a ∈ ↑φsΛφsucΛ:WickContraction [singleton ⋯]ᵘᶜ.length := (congr ⋯) (quotContraction {a} ⋯)h1:1 + (↑(quotContraction {a} ⋯)).card = (↑φsΛ).card⊢ (↑(quotContraction {a} ⋯)).card + 1 = (↑φsΛ).card All goals completed! 🐙lemma join_not_gradingCompliant_of_left_not_gradingCompliant {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : ¬ φsΛ.GradingCompliant) : ¬ (join φsΛ φsucΛ).GradingCompliant := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthhc:¬GradingCompliant φs φsΛ⊢ ¬GradingCompliant φs (φsΛ.join φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthhc:∃ x, ∃ (x_1 : x ∈ ↑φsΛ), ¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨x, x_1⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨x, x_1⟩)]⊢ ∃ x, ∃ (x_1 : x ∈ ↑(φsΛ.join φsucΛ)), ¬(𝓕|>ₛφs[↑((φsΛ.join φsucΛ).fstFieldOfContract ⟨x, x_1⟩)]) = 𝓕|>ₛφs[↑((φsΛ.join φsucΛ).sndFieldOfContract ⟨x, x_1⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ ∃ x, ∃ (x_1 : x ∈ ↑(φsΛ.join φsucΛ)), ¬(𝓕|>ₛφs[↑((φsΛ.join φsucΛ).fstFieldOfContract ⟨x, x_1⟩)]) = 𝓕|>ₛφs[↑((φsΛ.join φsucΛ).sndFieldOfContract ⟨x, x_1⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ ∃ (x : ↑(joinLiftLeft ⟨a, ha⟩) ∈ ↑(φsΛ.join φsucΛ)), ¬(𝓕|>ₛφs[↑((φsΛ.join φsucΛ).fstFieldOfContract ⟨↑(joinLiftLeft ⟨a, ha⟩), x⟩)]) = 𝓕|>ₛφs[↑((φsΛ.join φsucΛ).sndFieldOfContract ⟨↑(joinLiftLeft ⟨a, ha⟩), x⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ ¬(𝓕|>ₛφs[↑((φsΛ.join φsucΛ).fstFieldOfContract ⟨↑(joinLiftLeft ⟨a, ha⟩), ⋯⟩)]) = 𝓕|>ₛφs[↑((φsΛ.join φsucΛ).sndFieldOfContract ⟨↑(joinLiftLeft ⟨a, ha⟩), ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ ¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)] All goals completed! 🐙