Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnSection

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.CrAnFieldOp
public import Physlib.Mathematics.List

Creation and annihilation sections

In the module Physlib.QFT.PerturbationTheory.FieldSpecification.Basic we defined states for a field specification, and in the module Physlib.QFT.PerturbationTheory.FieldStatistics.CrAnFieldOp we defined a refinement of states called CrAnFieldOp which distinguishes between the creation and annihilation components of states. There exists, in particular, a map from CrAnFieldOp to FieldOp called crAnFieldOpToFieldOp.

Given a list of FieldOp, φs, in this module we define a section of φs to be a list of CrAnFieldOp, ψs, such that under the map crAnFieldOpToFieldOp, ψs is mapped to φs. That is to say, the states underlying ψs are the states in φs. We denote these sections as CrAnSection φs.

Looking forward the main consequence of this definition is the lemma FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_sum.

In this module we define various properties of CrAnSection.

@[expose] public section

The sections in 𝓕.CrAnFieldOp over a list φs : List 𝓕.FieldOp. In terms of physics, given some fields φ₁...φₙ, the different ways one can associate each field as a creation or an annilation operator. E.g. the number of terms φ₁⁰φ₂¹...φₙ⁰ φ₁¹φ₂¹...φₙ⁰ etc. If some fields are exclusively creation or annihilation operators at this point (e.g. asymptotic states) this is accounted for.

def CrAnSection (φs : List 𝓕.FieldOp) : Type :=
  {ψs : List 𝓕.CrAnFieldOp // ψs.map 𝓕.crAnFieldOpToFieldOp = φs}

  -- Π i, 𝓕.fieldOpToCreateAnnihilateType (φs.get i)

namespace CrAnSection

@[simp]
lemma length_eq (ψs : CrAnSection φs) : ψs.1.length = φs.length := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (↑ψs).length = φs.length
  simpa using congrArg List.length ψs.2All goals completed! 🐙

The tail of a section for φs.


def tail : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) → CrAnSection φs.tail
  | [], ⟨[], h⟩ => ⟨[], h⟩
  | φ :: φs, ⟨[], h⟩ => False.elim (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOph:List.map 𝓕.crAnFieldOpToFieldOp [] = φ :: φs⊢ False simp at hAll goals completed! 🐙)
  | φ :: φs, ⟨ψ :: ψs, h⟩ => ⟨ψs, by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ψs = (φ :: φs).tail rw [List.map_cons,𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:𝓕.crAnFieldOpToFieldOp ψ :: List.map 𝓕.crAnFieldOpToFieldOp ψs = φ :: φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ψs = (φ :: φs).tail𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ψs = (φ :: φs).tail List.cons.injEq𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ψs = (φ :: φs).tail𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ψs = (φ :: φs).tail] at h𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ψs = (φ :: φs).tail; exact h.2All goals completed! 🐙⟩

              lemma head_state_eq {φ : 𝓕.FieldOp} : (ψs : CrAnSection (φ :: φs)) →
    (ψs.1.head (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection (φ :: φs)⊢ ↑ψs ≠ [] simp [← List.length_pos_iff_ne_nil]All goals completed! 🐙)).1 = φ
  | ⟨[], h⟩ => False.elim (by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOph:List.map 𝓕.crAnFieldOpToFieldOp [] = φ :: φs⊢ False simp at hAll goals completed! 🐙)
  | ⟨ψ :: ψs, h⟩ =>𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ ((↑⟨ψ :: ψs, h⟩).head ⋯).fst = φ by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ ((↑⟨ψ :: ψs, h⟩).head ⋯).fst = φ
    simp only [List.map_cons, List.cons.injEq] at h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φsh:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ ((↑⟨ψ :: ψs, h⟩).head ⋯).fst = φ
    exact h.1All goals completed! 🐙

lemma statistics_eq_state_statistics (ψs : CrAnSection φs) :
    (𝓕 |>ₛ ψs.1) = 𝓕 |>ₛ φs := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ ofList 𝓕.crAnStatistics ↑ψs = ofList 𝓕.fieldOpStatistic φs
  erw [FieldStatistic.ofList_eq_prod,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (List.map 𝓕.crAnStatistics ↑ψs).prod = ofList 𝓕.fieldOpStatistic φs FieldStatistic.ofList_eq_prod,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (List.map 𝓕.crAnStatistics ↑ψs).prod = (List.map 𝓕.fieldOpStatistic φs).prod crAnStatistics𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (List.map (𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp) ↑ψs).prod = (List.map 𝓕.fieldOpStatistic φs).prod]𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (List.map (𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp) ↑ψs).prod = (List.map 𝓕.fieldOpStatistic φs).prod
  rw [← List.map_comp_map,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ ((List.map 𝓕.fieldOpStatistic ∘ List.map 𝓕.crAnFieldOpToFieldOp) ↑ψs).prod = (List.map 𝓕.fieldOpStatistic φs).prodAll goals completed! 🐙 Function.comp_apply,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (List.map 𝓕.fieldOpStatistic (List.map 𝓕.crAnFieldOpToFieldOp ↑ψs)).prod = (List.map 𝓕.fieldOpStatistic φs).prodAll goals completed! 🐙 ψs.2𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (List.map 𝓕.fieldOpStatistic φs).prod = (List.map 𝓕.fieldOpStatistic φs).prodAll goals completed! 🐙]All goals completed! 🐙

lemma take_statistics_eq_take_state_statistics (ψs : CrAnSection φs) n :
    (𝓕 |>ₛ (ψs.1.take n)) = 𝓕 |>ₛ (φs.take n) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ ofList 𝓕.crAnStatistics (List.take n ↑ψs) = ofList 𝓕.fieldOpStatistic (List.take n φs)
  erw [FieldStatistic.ofList_eq_prod,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.map 𝓕.crAnStatistics (List.take n ↑ψs)).prod = ofList 𝓕.fieldOpStatistic (List.take n φs) FieldStatistic.ofList_eq_prod,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.map 𝓕.crAnStatistics (List.take n ↑ψs)).prod = (List.map 𝓕.fieldOpStatistic (List.take n φs)).prod crAnStatistics𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.map (𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp) (List.take n ↑ψs)).prod =
  (List.map 𝓕.fieldOpStatistic (List.take n φs)).prod]𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.map (𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp) (List.take n ↑ψs)).prod =
  (List.map 𝓕.fieldOpStatistic (List.take n φs)).prod
  simp only [List.map_take]𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.take n (List.map (𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp) ↑ψs)).prod =
  (List.take n (List.map 𝓕.fieldOpStatistic φs)).prod
  rw [← List.map_comp_map,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.take n ((List.map 𝓕.fieldOpStatistic ∘ List.map 𝓕.crAnFieldOpToFieldOp) ↑ψs)).prod =
  (List.take n (List.map 𝓕.fieldOpStatistic φs)).prodAll goals completed! 🐙 Function.comp_apply,𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.take n (List.map 𝓕.fieldOpStatistic (List.map 𝓕.crAnFieldOpToFieldOp ↑ψs))).prod =
  (List.take n (List.map 𝓕.fieldOpStatistic φs)).prodAll goals completed! 🐙 ψs.2𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φsn:ℕ⊢ (List.take n (List.map 𝓕.fieldOpStatistic φs)).prod = (List.take n (List.map 𝓕.fieldOpStatistic φs)).prodAll goals completed! 🐙]All goals completed! 🐙

The head of a section for φ :: φs as an element in 𝓕.fieldOpToCreateAnnihilateType φ.

def head : {φ : 𝓕.FieldOp} → (ψs : CrAnSection (φ :: φs)) →
    𝓕.fieldOpToCrAnType φ
  | φ, ⟨[], h⟩ => False.elim (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOph:List.map 𝓕.crAnFieldOpToFieldOp [] = φ :: φs⊢ False simp at hAll goals completed! 🐙)
  | φ, ⟨ψ :: ψs, h⟩ => 𝓕.fieldOpToCreateAnnihilateTypeCongr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ ψ.fst = φ
    simpa using head_state_eq ⟨ψ :: ψs, h⟩All goals completed! 🐙) ψ.2

lemma eq_head_cons_tail {φ : 𝓕.FieldOp} {ψs : CrAnSection (φ :: φs)} :
    ψs.1 = ⟨φ, head ψs⟩ :: ψs.tail.1 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection (φ :: φs)⊢ ↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tail
  match ψs with
  | ⟨[], h⟩ =>𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection (φ :: φs)h:List.map 𝓕.crAnFieldOpToFieldOp [] = φ :: φs⊢ ↑⟨[], h⟩ = ⟨φ, head ⟨[], h⟩⟩ :: ↑(tail ⟨[], h⟩) exact False.elim (by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection (φ :: φs)h:List.map 𝓕.crAnFieldOpToFieldOp [] = φ :: φs⊢ False simp at hAll goals completed! 🐙)
  | ⟨ψ :: ψs, h⟩ =>𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs✝:CrAnSection (φ :: φs)ψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ ↑⟨ψ :: ψs, h⟩ = ⟨φ, head ⟨ψ :: ψs, h⟩⟩ :: ↑(tail ⟨ψ :: ψs, h⟩)
    have h2 := head_state_eq ⟨ψ :: ψs, h⟩𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs✝:CrAnSection (φ :: φs)ψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φsh2:((↑⟨ψ :: ψs, h⟩).head ⋯).fst = φ⊢ ↑⟨ψ :: ψs, h⟩ = ⟨φ, head ⟨ψ :: ψs, h⟩⟩ :: ↑(tail ⟨ψ :: ψs, h⟩)
    simp only [List.head_cons] at h2𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs✝:CrAnSection (φ :: φs)ψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φsh2:ψ.fst = φ⊢ ↑⟨ψ :: ψs, h⟩ = ⟨φ, head ⟨ψ :: ψs, h⟩⟩ :: ↑(tail ⟨ψ :: ψs, h⟩)
    subst h2𝓕:FieldSpecificationφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs✝:List 𝓕.CrAnFieldOpψs:CrAnSection (ψ.fst :: φs)h:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs✝) = ψ.fst :: φs⊢ ↑⟨ψ :: ψs✝, h⟩ = ⟨ψ.fst, head ⟨ψ :: ψs✝, h⟩⟩ :: ↑(tail ⟨ψ :: ψs✝, h⟩)
    rflAll goals completed! 🐙

The creation of a section from for φ : φs from a section for φs and a element of 𝓕.fieldOpToCreateAnnihilateType φ.

def cons {φ : 𝓕.FieldOp} (ψ : 𝓕.fieldOpToCrAnType φ) (ψs : CrAnSection φs) :
    CrAnSection (φ :: φs) := ⟨⟨φ, ψ⟩ :: ψs.1, by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.fieldOpToCrAnType φψs:CrAnSection φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (⟨φ, ψ⟩ :: ↑ψs) = φ :: φs
  simp [List.map_cons, ψs.2]All goals completed! 🐙⟩

For the empty list of states there is only one CrAnSection. Corresponding to the empty list of CrAnFieldOp.

def nilEquiv : CrAnSection (𝓕 := 𝓕) [] ≃ Unit where
  toFun _ := ()
  invFun _ := ⟨[], rfl⟩
  left_inv ψs := Subtype.ext <| by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection []⊢ ↑((fun x => ⟨[], ⋯⟩) ((fun x => ()) ψs)) = ↑ψs
    have h2 := ψs.2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection []h2:List.map 𝓕.crAnFieldOpToFieldOp ↑ψs = []⊢ ↑((fun x => ⟨[], ⋯⟩) ((fun x => ()) ψs)) = ↑ψs
    simp only [List.map_eq_nil_iff] at h2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection []h2:↑ψs = []⊢ ↑((fun x => ⟨[], ⋯⟩) ((fun x => ()) ψs)) = ↑ψs
    simp [h2]All goals completed! 🐙
  right_inv _ := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpx✝:Unit⊢ (fun x => ()) ((fun x => ⟨[], ⋯⟩) x✝) = x✝
    simpAll goals completed! 🐙

The creation and annihilation sections for a singleton list is given by a choice of 𝓕.fieldOpToCreateAnnihilateType φ. If φ is a asymptotic state there is no choice here, else there are two choices.


def singletonEquiv {φ : 𝓕.FieldOp} : CrAnSection [φ] ≃
    𝓕.fieldOpToCrAnType φ where
  toFun ψs := ψs.head
  invFun ψ := ⟨[⟨φ, ψ⟩], by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.fieldOpToCrAnType φ⊢ List.map 𝓕.crAnFieldOpToFieldOp [⟨φ, ψ⟩] = [φ] simpAll goals completed! 🐙⟩
  left_inv ψs := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]⊢ (fun ψ => ⟨[⟨φ, ψ⟩], ⋯⟩) ((fun ψs => ψs.head) ψs) = ψs
    apply Subtype.ext𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]⊢ ↑((fun ψ => ⟨[⟨φ, ψ⟩], ⋯⟩) ((fun ψs => ψs.head) ψs)) = ↑ψs
    simp only𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]⊢ [⟨φ, ψs.head⟩] = ↑ψs
    have h1 := eq_head_cons_tail (ψs := ψs)𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]h1:↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tail⊢ [⟨φ, ψs.head⟩] = ↑ψs
    rw [h1𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]h1:↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tail⊢ [⟨φ, ψs.head⟩] = ⟨φ, ψs.head⟩ :: ↑ψs.tail𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]h1:↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tail⊢ [⟨φ, ψs.head⟩] = ⟨φ, ψs.head⟩ :: ↑ψs.tail]𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]h1:↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tail⊢ [⟨φ, ψs.head⟩] = ⟨φ, ψs.head⟩ :: ↑ψs.tail
    have h2 := ψs.tail.2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]h1:↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tailh2:List.map 𝓕.crAnFieldOpToFieldOp ↑ψs.tail = [φ].tail⊢ [⟨φ, ψs.head⟩] = ⟨φ, ψs.head⟩ :: ↑ψs.tail
    simp only [List.tail_cons, List.map_eq_nil_iff] at h2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection [φ]h1:↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tailh2:↑ψs.tail = []⊢ [⟨φ, ψs.head⟩] = ⟨φ, ψs.head⟩ :: ↑ψs.tail
    simp [h2]All goals completed! 🐙
  right_inv ψ := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.fieldOpToCrAnType φ⊢ (fun ψs => ψs.head) ((fun ψ => ⟨[⟨φ, ψ⟩], ⋯⟩) ψ) = ψ
    simp only [head]𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψ:𝓕.fieldOpToCrAnType φ⊢ (𝓕.fieldOpToCreateAnnihilateTypeCongr ⋯) ψ = ψ
    rflAll goals completed! 🐙

An equivalence separating the head of a creation and annihilation section from the tail.

def consEquiv {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} : CrAnSection (φ :: φs) ≃
    𝓕.fieldOpToCrAnType φ × CrAnSection φs where
  toFun ψs := ⟨ψs.head, ψs.tail⟩
  invFun ψψs :=
    match ψψs with
    | (ψ, ψs) => cons ψ ψs
  left_inv ψs := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψs:CrAnSection (φ :: φs)⊢ (fun ψψs =>
      match ψψs with
      | (ψ, ψs) => cons ψ ψs)
    ((fun ψs => (ψs.head, ψs.tail)) ψs) =
  ψs
    apply Subtype.ext𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψs:CrAnSection (φ :: φs)⊢ ↑((fun ψψs =>
        match ψψs with
        | (ψ, ψs) => cons ψ ψs)
      ((fun ψs => (ψs.head, ψs.tail)) ψs)) =
  ↑ψs
    exact Eq.symm eq_head_cons_tailAll goals completed! 🐙
  right_inv ψψs := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψψs:𝓕.fieldOpToCrAnType φ × CrAnSection φs⊢ (fun ψs => (ψs.head, ψs.tail))
    ((fun ψψs =>
        match ψψs with
        | (ψ, ψs) => cons ψ ψs)
      ψψs) =
  ψψs
    match ψψs with
    | (ψ, ψs) =>𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψψs:𝓕.fieldOpToCrAnType φ × CrAnSection φsψ:𝓕.fieldOpToCrAnType φψs:CrAnSection φs⊢ (fun ψs => (ψs.head, ψs.tail))
    ((fun ψψs =>
        match ψψs with
        | (ψ, ψs) => cons ψ ψs)
      (ψ, ψs)) =
  (ψ, ψs) rflAll goals completed! 🐙

The instance of a finite type on CrAnSections defined recursively through consEquiv.

instance fintype : (φs : List 𝓕.FieldOp) → Fintype (CrAnSection φs)
  | [] => Fintype.ofEquiv _ nilEquiv.symm
  | _ :: φs =>
    haveI : Fintype (CrAnSection φs) := fintype φs
    Fintype.ofEquiv _ consEquiv.symm

              

@[simp]
lemma card_nil_eq : Fintype.card (CrAnSection (𝓕 := 𝓕) []) = 1 := by𝓕:FieldSpecification⊢ Fintype.card (CrAnSection []) = 1
  rw [Fintype.ofEquiv_card nilEquiv.symm𝓕:FieldSpecification⊢ Fintype.card Unit = 1𝓕:FieldSpecification⊢ Fintype.card Unit = 1]𝓕:FieldSpecification⊢ Fintype.card Unit = 1
  simpAll goals completed! 🐙

lemma card_cons_eq {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} :
    Fintype.card (CrAnSection (φ :: φs)) = Fintype.card (𝓕.fieldOpToCrAnType φ) *
    Fintype.card (CrAnSection φs) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (φ :: φs)) = Fintype.card (𝓕.fieldOpToCrAnType φ) * Fintype.card (CrAnSection φs)
  rw [Fintype.ofEquiv_card consEquiv.symm𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType φ × CrAnSection φs) =
  Fintype.card (𝓕.fieldOpToCrAnType φ) * Fintype.card (CrAnSection φs)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType φ × CrAnSection φs) =
  Fintype.card (𝓕.fieldOpToCrAnType φ) * Fintype.card (CrAnSection φs)]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType φ × CrAnSection φs) =
  Fintype.card (𝓕.fieldOpToCrAnType φ) * Fintype.card (CrAnSection φs)
  simpAll goals completed! 🐙

lemma card_eq_mul : {φs : List 𝓕.FieldOp} → Fintype.card (CrAnSection φs) =
    2 ^ (List.countP 𝓕.statesIsPosition φs)
  | [] =>𝓕:FieldSpecification⊢ Fintype.card (CrAnSection []) = 2 ^ List.countP 𝓕.statesIsPosition [] by𝓕:FieldSpecification⊢ Fintype.card (CrAnSection []) = 2 ^ List.countP 𝓕.statesIsPosition []
    simpAll goals completed! 🐙
  | FieldOp.position _ :: φs =>𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.position a✝ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition (FieldOp.position a✝ :: φs) by𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.position a✝ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition (FieldOp.position a✝ :: φs)
      simp only [statesIsPosition, List.countP_cons_of_pos]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.position a✝ :: φs)) = 2 ^ (List.countP 𝓕.statesIsPosition φs + 1)
      rw [card_cons_eq𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.position a✝)) * Fintype.card (CrAnSection φs) =
  2 ^ (List.countP 𝓕.statesIsPosition φs + 1)𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.position a✝)) * Fintype.card (CrAnSection φs) =
  2 ^ (List.countP 𝓕.statesIsPosition φs + 1)]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.position a✝)) * Fintype.card (CrAnSection φs) =
  2 ^ (List.countP 𝓕.statesIsPosition φs + 1)
      rw [card_eq_mul𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.position a✝)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ (List.countP 𝓕.statesIsPosition φs + 1)𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.position a✝)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ (List.countP 𝓕.statesIsPosition φs + 1)]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.position a✝)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ (List.countP 𝓕.statesIsPosition φs + 1)
      simp only [fieldOpToCrAnType]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ Fintype.card CreateAnnihilate * 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ (List.countP 𝓕.statesIsPosition φs + 1)
      erw [CreateAnnihilate.CreateAnnihilate_card_eq_two𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ 2 * 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ (List.countP 𝓕.statesIsPosition φs + 1)]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφs:List 𝓕.FieldOp⊢ 2 * 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ (List.countP 𝓕.statesIsPosition φs + 1)
      ringAll goals completed! 🐙
  | FieldOp.inAsymp x_ :: φs =>𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.inAsymp x_ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition (FieldOp.inAsymp x_ :: φs) by𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.inAsymp x_ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition (FieldOp.inAsymp x_ :: φs)
      simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg]𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.inAsymp x_ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition φs
      rw [card_cons_eq𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.inAsymp x_)) * Fintype.card (CrAnSection φs) =
  2 ^ List.countP 𝓕.statesIsPosition φs𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.inAsymp x_)) * Fintype.card (CrAnSection φs) =
  2 ^ List.countP 𝓕.statesIsPosition φs]𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.inAsymp x_)) * Fintype.card (CrAnSection φs) =
  2 ^ List.countP 𝓕.statesIsPosition φs
      rw [card_eq_mul𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.inAsymp x_)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ List.countP 𝓕.statesIsPosition φs𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.inAsymp x_)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ List.countP 𝓕.statesIsPosition φs]𝓕:FieldSpecificationx_:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.inAsymp x_)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ List.countP 𝓕.statesIsPosition φs
      simp [fieldOpToCrAnType]All goals completed! 🐙
  | FieldOp.outAsymp _ :: φs =>𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.outAsymp a✝ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition (FieldOp.outAsymp a✝ :: φs) by𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.outAsymp a✝ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition (FieldOp.outAsymp a✝ :: φs)
      simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (CrAnSection (FieldOp.outAsymp a✝ :: φs)) = 2 ^ List.countP 𝓕.statesIsPosition φs
      rw [card_cons_eq𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.outAsymp a✝)) * Fintype.card (CrAnSection φs) =
  2 ^ List.countP 𝓕.statesIsPosition φs𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.outAsymp a✝)) * Fintype.card (CrAnSection φs) =
  2 ^ List.countP 𝓕.statesIsPosition φs]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.outAsymp a✝)) * Fintype.card (CrAnSection φs) =
  2 ^ List.countP 𝓕.statesIsPosition φs
      rw [card_eq_mul𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.outAsymp a✝)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ List.countP 𝓕.statesIsPosition φs𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.outAsymp a✝)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ List.countP 𝓕.statesIsPosition φs]𝓕:FieldSpecificationa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφs:List 𝓕.FieldOp⊢ Fintype.card (𝓕.fieldOpToCrAnType (FieldOp.outAsymp a✝)) * 2 ^ List.countP 𝓕.statesIsPosition φs =
  2 ^ List.countP 𝓕.statesIsPosition φs
      simp [fieldOpToCrAnType]All goals completed! 🐙

lemma card_perm_eq {φs φs' : List 𝓕.FieldOp} (h : φs.Perm φs') :
    Fintype.card (CrAnSection φs) = Fintype.card (CrAnSection φs') := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ Fintype.card (CrAnSection φs) = Fintype.card (CrAnSection φs')
  rw [card_eq_mul,𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ 2 ^ List.countP 𝓕.statesIsPosition φs = Fintype.card (CrAnSection φs')𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ List.countP 𝓕.statesIsPosition φs' card_eq_mul𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ List.countP 𝓕.statesIsPosition φs'𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ List.countP 𝓕.statesIsPosition φs']𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ 2 ^ List.countP 𝓕.statesIsPosition φs = 2 ^ List.countP 𝓕.statesIsPosition φs'
  congr 1e_a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs.Perm φs'⊢ List.countP 𝓕.statesIsPosition φs = List.countP 𝓕.statesIsPosition φs'
  exact List.Perm.countP_congr h fun x => congrFun rflAll goals completed! 🐙

@[simp]
lemma sum_nil (f : CrAnSection (𝓕 := 𝓕) [] → M) [AddCommMonoid M] :
    ∑ (s : CrAnSection []), f s = f ⟨[], rfl⟩ := by𝓕:FieldSpecificationM:Type u_1f:CrAnSection [] → Minst✝:AddCommMonoid M⊢ ∑ s, f s = f ⟨[], ⋯⟩
  rw [← nilEquiv.symm.sum_comp𝓕:FieldSpecificationM:Type u_1f:CrAnSection [] → Minst✝:AddCommMonoid M⊢ ∑ i, f (nilEquiv.symm i) = f ⟨[], ⋯⟩𝓕:FieldSpecificationM:Type u_1f:CrAnSection [] → Minst✝:AddCommMonoid M⊢ ∑ i, f (nilEquiv.symm i) = f ⟨[], ⋯⟩]𝓕:FieldSpecificationM:Type u_1f:CrAnSection [] → Minst✝:AddCommMonoid M⊢ ∑ i, f (nilEquiv.symm i) = f ⟨[], ⋯⟩
  simp only [Finset.univ_unique, PUnit.default_eq_unit, Finset.sum_singleton]𝓕:FieldSpecificationM:Type u_1f:CrAnSection [] → Minst✝:AddCommMonoid M⊢ f (nilEquiv.symm PUnit.unit) = f ⟨[], ⋯⟩
  rflAll goals completed! 🐙

lemma sum_cons (f : CrAnSection (φ :: φs) → M) [AddCommMonoid M] :
    ∑ (s : CrAnSection (φ :: φs)), f s = ∑ (a : 𝓕.fieldOpToCrAnType φ),
    ∑ (s : CrAnSection φs), f (cons a s) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpM:Type u_1f:CrAnSection (φ :: φs) → Minst✝:AddCommMonoid M⊢ ∑ s, f s = ∑ a, ∑ s, f (cons a s)
  rw [← consEquiv.symm.sum_comp,𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpM:Type u_1f:CrAnSection (φ :: φs) → Minst✝:AddCommMonoid M⊢ ∑ i, f (consEquiv.symm i) = ∑ a, ∑ s, f (cons a s)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpM:Type u_1f:CrAnSection (φ :: φs) → Minst✝:AddCommMonoid M⊢ ∑ x, ∑ y, f (consEquiv.symm (x, y)) = ∑ a, ∑ s, f (cons a s) Fintype.sum_prod_type𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpM:Type u_1f:CrAnSection (φ :: φs) → Minst✝:AddCommMonoid M⊢ ∑ x, ∑ y, f (consEquiv.symm (x, y)) = ∑ a, ∑ s, f (cons a s)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpM:Type u_1f:CrAnSection (φ :: φs) → Minst✝:AddCommMonoid M⊢ ∑ x, ∑ y, f (consEquiv.symm (x, y)) = ∑ a, ∑ s, f (cons a s)]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpM:Type u_1f:CrAnSection (φ :: φs) → Minst✝:AddCommMonoid M⊢ ∑ x, ∑ y, f (consEquiv.symm (x, y)) = ∑ a, ∑ s, f (cons a s)
  rflAll goals completed! 🐙

lemma sum_over_length {s : CrAnSection φs} (f : Fin s.1.length → M)
    [AddCommMonoid M] : ∑ (n : Fin s.1.length), f n =
    ∑ (n : Fin φs.length), f (Fin.cast (length_eq s).symm n) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpM:Type u_1s:CrAnSection φsf:Fin (↑s).length → Minst✝:AddCommMonoid M⊢ ∑ n, f n = ∑ n, f (Fin.cast ⋯ n)
  rw [← (finCongr (length_eq s)).sum_comp𝓕:FieldSpecificationφs:List 𝓕.FieldOpM:Type u_1s:CrAnSection φsf:Fin (↑s).length → Minst✝:AddCommMonoid M⊢ ∑ n, f n = ∑ i, f (Fin.cast ⋯ ((finCongr ⋯) i))𝓕:FieldSpecificationφs:List 𝓕.FieldOpM:Type u_1s:CrAnSection φsf:Fin (↑s).length → Minst✝:AddCommMonoid M⊢ ∑ n, f n = ∑ i, f (Fin.cast ⋯ ((finCongr ⋯) i))]𝓕:FieldSpecificationφs:List 𝓕.FieldOpM:Type u_1s:CrAnSection φsf:Fin (↑s).length → Minst✝:AddCommMonoid M⊢ ∑ n, f n = ∑ i, f (Fin.cast ⋯ ((finCongr ⋯) i))
  rflAll goals completed! 🐙

The equivalence between CrAnSection φs and CrAnSection φs' induced by an equality φs = φs'.

def congr : {φs φs' : List 𝓕.FieldOp} → (h : φs = φs') →
    CrAnSection φs ≃ CrAnSection φs'
  | _, _, rfl => Equiv.refl _

              @[simp]
lemma congr_fst {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (ψs : CrAnSection φs) :
    (congr h ψs).1 = ψs.1 := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'ψs:CrAnSection φs⊢ ↑((congr h) ψs) = ↑ψs
  cases hrefl𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ ↑((congr ⋯) ψs) = ↑ψs
  rflAll goals completed! 🐙@[simp]
lemma congr_symm {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
    (congr h).symm = congr h.symm := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'⊢ (congr h).symm = congr ⋯
  cases hrefl𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ (congr ⋯).symm = congr ⋯
  rflAll goals completed! 🐙

@[simp]
lemma congr_trans_apply {φs φs' φs'' : List 𝓕.FieldOp} (h1 : φs = φs') (h2 : φs' = φs'')
    (ψs : CrAnSection φs) :
    (congr h2 (congr h1 ψs)) = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOph1:φs = φs'h2:φs' = φs''ψs:CrAnSection φs⊢ φs = φs'' rw [h1,𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOph1:φs = φs'h2:φs' = φs''ψs:CrAnSection φs⊢ φs' = φs''All goals completed! 🐙 h2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOph1:φs = φs'h2:φs' = φs''ψs:CrAnSection φs⊢ φs'' = φs''All goals completed! 🐙]All goals completed! 🐙) ψs := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOph1:φs = φs'h2:φs' = φs''ψs:CrAnSection φs⊢ (congr h2) ((congr h1) ψs) = (congr ⋯) ψs
  subst h1 h2𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:CrAnSection φs⊢ (congr ⋯) ((congr ⋯) ψs) = (congr ⋯) ψs
  rflAll goals completed! 🐙

Returns the first n elements of a section and its underlying list.

def take (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.take n) :=
  ⟨ψs.1.take n, by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.take n ↑ψs) = List.take n φs simp [ψs.2]All goals completed! 🐙⟩



@[simp]
lemma take_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (n : ℕ)
    (ψs : CrAnSection φs) :
    (take n (congr h ψs)) = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'n:ℕψs:CrAnSection φs⊢ List.take n φs = List.take n φs' rw [h𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'n:ℕψs:CrAnSection φs⊢ List.take n φs' = List.take n φs'All goals completed! 🐙]All goals completed! 🐙) (take n ψs) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'n:ℕψs:CrAnSection φs⊢ take n ((congr h) ψs) = (congr ⋯) (take n ψs)
  subst h𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ take n ((congr ⋯) ψs) = (congr ⋯) (take n ψs)
  rflAll goals completed! 🐙

Removes the first n elements of a section and its underlying list.

def drop (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.drop n) :=
  ⟨ψs.1.drop n, by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.drop n ↑ψs) = List.drop n φs simp [ψs.2]All goals completed! 🐙⟩



@[simp]
lemma drop_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (n : ℕ)
    (ψs : CrAnSection φs) :
    (drop n (congr h ψs)) = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'n:ℕψs:CrAnSection φs⊢ List.drop n φs = List.drop n φs' rw [h𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'n:ℕψs:CrAnSection φs⊢ List.drop n φs' = List.drop n φs'All goals completed! 🐙]All goals completed! 🐙) (drop n ψs) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'n:ℕψs:CrAnSection φs⊢ drop n ((congr h) ψs) = (congr ⋯) (drop n ψs)
  subst h𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ drop n ((congr ⋯) ψs) = (congr ⋯) (drop n ψs)
  rflAll goals completed! 🐙

Appends two sections and their underlying lists.

def append {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
    (ψs' : CrAnSection φs') : CrAnSection (φs ++ φs') :=
  ⟨ψs.1 ++ ψs'.1, by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ List.map 𝓕.crAnFieldOpToFieldOp (↑ψs ++ ↑ψs') = φs ++ φs' simp [ψs.2, ψs'.2]All goals completed! 🐙⟩

              lemma append_assoc {φs φs' φs'' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
    (ψs' : CrAnSection φs') (ψs'' : CrAnSection φs'') :
    append ψs (append ψs' ψs'') = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'ψs'':CrAnSection φs''⊢ φs ++ φs' ++ φs'' = φs ++ (φs' ++ φs'') simpAll goals completed! 🐙) (append (append ψs ψs') ψs'') := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'ψs'':CrAnSection φs''⊢ ψs.append (ψs'.append ψs'') = (congr ⋯) ((ψs.append ψs').append ψs'')
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'ψs'':CrAnSection φs''⊢ ↑(ψs.append (ψs'.append ψs'')) = ↑((congr ⋯) ((ψs.append ψs').append ψs''))
  simp [append]All goals completed! 🐙lemma append_assoc' {φs φs' φs'' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
    (ψs' : CrAnSection φs') (ψs'' : CrAnSection φs'') :
    (append (append ψs ψs') ψs'') = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'ψs'':CrAnSection φs''⊢ φs ++ (φs' ++ φs'') = φs ++ φs' ++ φs'' simpAll goals completed! 🐙) (append ψs (append ψs' ψs'')) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'ψs'':CrAnSection φs''⊢ (ψs.append ψs').append ψs'' = (congr ⋯) (ψs.append (ψs'.append ψs''))
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpφs'':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'ψs'':CrAnSection φs''⊢ ↑((ψs.append ψs').append ψs'') = ↑((congr ⋯) (ψs.append (ψs'.append ψs'')))
  simp [append]All goals completed! 🐙lemma singletonEquiv_append_eq_cons {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp}
    (ψs : CrAnSection φs) (ψ : 𝓕.fieldOpToCrAnType φ) :
    append (singletonEquiv.symm ψ) ψs = cons ψ ψs := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection φsψ:𝓕.fieldOpToCrAnType φ⊢ (singletonEquiv.symm ψ).append ψs = cons ψ ψs
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpψs:CrAnSection φsψ:𝓕.fieldOpToCrAnType φ⊢ ↑((singletonEquiv.symm ψ).append ψs) = ↑(cons ψ ψs)
  simp [append, cons, singletonEquiv]All goals completed! 🐙@[simp]
lemma take_append_drop {n : ℕ} (ψs : CrAnSection φs) :
    append (take n ψs) (drop n ψs) = congr (List.take_append_drop n φs).symm ψs := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ (take n ψs).append (drop n ψs) = (congr ⋯) ψs
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ ↑((take n ψs).append (drop n ψs)) = ↑((congr ⋯) ψs)
  simp [take, drop, append]All goals completed! 🐙

lemma congr_append {φs1 φs1' φs2 φs2' : List 𝓕.FieldOp} (h1 : φs1 = φs1') (h2 : φs2 = φs2')
    (ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) :
    (append (congr h1 ψs1) (congr h2 ψs2)) = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph1:φs1 = φs1'h2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1 ++ φs2 = φs1' ++ φs2' rw [h1,𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph1:φs1 = φs1'h2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1' ++ φs2 = φs1' ++ φs2'All goals completed! 🐙 h2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph1:φs1 = φs1'h2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1' ++ φs2' = φs1' ++ φs2'All goals completed! 🐙]All goals completed! 🐙) (append ψs1 ψs2) := by𝓕:FieldSpecificationφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph1:φs1 = φs1'h2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ ((congr h1) ψs1).append ((congr h2) ψs2) = (congr ⋯) (ψs1.append ψs2)
  subst h1 h2𝓕:FieldSpecificationφs1:List 𝓕.FieldOpφs2:List 𝓕.FieldOpψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ ((congr ⋯) ψs1).append ((congr ⋯) ψs2) = (congr ⋯) (ψs1.append ψs2)
  rflAll goals completed! 🐙

@[simp]
lemma congr_fst_append {φs1 φs1' φs2 : List 𝓕.FieldOp} (h1 : φs1 = φs1')
    (ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) :
    (append (congr h1 ψs1) (ψs2)) = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOph1:φs1 = φs1'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1 ++ φs2 = φs1' ++ φs2 rw [h1𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOph1:φs1 = φs1'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1' ++ φs2 = φs1' ++ φs2All goals completed! 🐙]All goals completed! 🐙) (append ψs1 ψs2) := by𝓕:FieldSpecificationφs1:List 𝓕.FieldOpφs1':List 𝓕.FieldOpφs2:List 𝓕.FieldOph1:φs1 = φs1'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ ((congr h1) ψs1).append ψs2 = (congr ⋯) (ψs1.append ψs2)
  subst h1𝓕:FieldSpecificationφs1:List 𝓕.FieldOpφs2:List 𝓕.FieldOpψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ ((congr ⋯) ψs1).append ψs2 = (congr ⋯) (ψs1.append ψs2)
  rflAll goals completed! 🐙

@[simp]
lemma congr_snd_append {φs1 φs2 φs2' : List 𝓕.FieldOp} (h2 : φs2 = φs2')
    (ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) :
    (append ψs1 (congr h2 ψs2)) = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1 ++ φs2 = φs1 ++ φs2' rw [h2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs1:List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ φs1 ++ φs2' = φs1 ++ φs2'All goals completed! 🐙]All goals completed! 🐙) (append ψs1 ψs2) := by𝓕:FieldSpecificationφs1:List 𝓕.FieldOpφs2:List 𝓕.FieldOpφs2':List 𝓕.FieldOph2:φs2 = φs2'ψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ ψs1.append ((congr h2) ψs2) = (congr ⋯) (ψs1.append ψs2)
  subst h2𝓕:FieldSpecificationφs1:List 𝓕.FieldOpφs2:List 𝓕.FieldOpψs1:CrAnSection φs1ψs2:CrAnSection φs2⊢ ψs1.append ((congr ⋯) ψs2) = (congr ⋯) (ψs1.append ψs2)
  rflAll goals completed! 🐙@[simp]
lemma take_left {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
    (ψs' : CrAnSection φs') :
    take φs.length (ψs.append ψs') = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ φs = List.take φs.length (φs ++ φs') simpAll goals completed! 🐙) ψs := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ take φs.length (ψs.append ψs') = (congr ⋯) ψs
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ ↑(take φs.length (ψs.append ψs')) = ↑((congr ⋯) ψs)
  simp [take, append]All goals completed! 🐙@[simp]
lemma drop_left {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs)
    (ψs' : CrAnSection φs') :
    drop φs.length (ψs.append ψs') = congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ φs' = List.drop φs.length (φs ++ φs') simpAll goals completed! 🐙) ψs' := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ drop φs.length (ψs.append ψs') = (congr ⋯) ψs'
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection φsψs':CrAnSection φs'⊢ ↑(drop φs.length (ψs.append ψs')) = ↑((congr ⋯) ψs')
  simp [drop, append]All goals completed! 🐙

The equivalence between CrAnSection (φs ++ φs') and CrAnSection φs × CrAnSection φs formed by append, take and drop and their interrelationship.

def appendEquiv {φs φs' : List 𝓕.FieldOp} : CrAnSection (φs ++ φs') ≃
    CrAnSection φs × CrAnSection φs' where
  toFun ψs := (congr (List.take_left (l₁ := φs) (l₂ := φs')) (take φs.length ψs),
    congr (List.drop_left (l₁ := φs) (l₂ := φs')) (drop φs.length ψs))
  invFun ψsψs' := append ψsψs'.1 ψsψs'.2
  left_inv ψs := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection (φs ++ φs')⊢ (fun ψsψs' => ψsψs'.1.append ψsψs'.2) ((fun ψs => ((congr ⋯) (take φs.length ψs), (congr ⋯) (drop φs.length ψs))) ψs) =
  ψs
    apply Subtype.ext𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψs:CrAnSection (φs ++ φs')⊢ ↑((fun ψsψs' => ψsψs'.1.append ψsψs'.2)
      ((fun ψs => ((congr ⋯) (take φs.length ψs), (congr ⋯) (drop φs.length ψs))) ψs)) =
  ↑ψs
    simpAll goals completed! 🐙
  right_inv ψsψs' := by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'⊢ (fun ψs => ((congr ⋯) (take φs.length ψs), (congr ⋯) (drop φs.length ψs)))
    ((fun ψsψs' => ψsψs'.1.append ψsψs'.2) ψsψs') =
  ψsψs'
    match ψsψs' with
    | (ψs, ψs') =>𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'ψs:CrAnSection φsψs':CrAnSection φs'⊢ (fun ψs => ((congr ⋯) (take φs.length ψs), (congr ⋯) (drop φs.length ψs)))
    ((fun ψsψs' => ψsψs'.1.append ψsψs'.2) (ψs, ψs')) =
  (ψs, ψs')
    simp only [take_left, drop_left, Prod.mk.injEq]𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'ψs:CrAnSection φsψs':CrAnSection φs'⊢ (congr ⋯) ((congr ⋯) ψs) = ψs ∧ (congr ⋯) ((congr ⋯) ψs') = ψs'
    refine And.intro (Subtype.ext ?_) (Subtype.ext ?_)refine_1𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'ψs:CrAnSection φsψs':CrAnSection φs'⊢ ↑((congr ⋯) ((congr ⋯) ψs)) = ↑ψsrefine_2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'ψs:CrAnSection φsψs':CrAnSection φs'⊢ ↑((congr ⋯) ((congr ⋯) ψs')) = ↑ψs' <;>refine_1𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'ψs:CrAnSection φsψs':CrAnSection φs'⊢ ↑((congr ⋯) ((congr ⋯) ψs)) = ↑ψsrefine_2𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpψsψs':CrAnSection φs × CrAnSection φs'ψs:CrAnSection φsψs':CrAnSection φs'⊢ ↑((congr ⋯) ((congr ⋯) ψs')) = ↑ψs' simpAll goals completed! 🐙

@[simp]
lemma _root_.List.map_eraseIdx {α β : Type} (f : α → β) : (l : List α) → (n : ℕ) →
    List.map f (l.eraseIdx n) = (List.map f l).eraseIdx n
  | [], _ => rfl
  | a :: l, 0 => rfl
  | a :: l, n+1 =>α:Typeβ:Typef:α → βa:αl:List αn:ℕ⊢ List.map f ((a :: l).eraseIdx (n + 1)) = (List.map f (a :: l)).eraseIdx (n + 1) byα:Typeβ:Typef:α → βa:αl:List αn:ℕ⊢ List.map f ((a :: l).eraseIdx (n + 1)) = (List.map f (a :: l)).eraseIdx (n + 1)
    simp only [List.eraseIdx, List.map_cons, List.cons.injEq, true_and]α:Typeβ:Typef:α → βa:αl:List αn:ℕ⊢ List.map f (l.eraseIdx n) = (List.map f l).eraseIdx n
    exact List.map_eraseIdx f l nAll goals completed! 🐙

Erasing an element from a section and it's underlying list.

def eraseIdx (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.eraseIdx n) :=
  ⟨ψs.1.eraseIdx n, by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φs⊢ List.map 𝓕.crAnFieldOpToFieldOp ((↑ψs).eraseIdx n) = φs.eraseIdx n simp [ψs.2]All goals completed! 🐙⟩

The equivalence formed by extracting an element from a section.

def eraseIdxEquiv (n : ℕ) (φs : List 𝓕.FieldOp) (hn : n < φs.length) :
    CrAnSection φs ≃ 𝓕.fieldOpToCrAnType φs[n] ×
    CrAnSection (φs.eraseIdx n) :=
  (congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.length⊢ φs = List.take n φs ++ [φs[n]] ++ List.drop (n + 1) φs simp only [List.take_concat_get', List.take_append_drop]All goals completed! 🐙)).trans <|
  appendEquiv.trans <|
  (Equiv.prodCongr (appendEquiv.trans (Equiv.prodComm _ _)) (Equiv.refl _)).trans <|
  (Equiv.prodAssoc _ _ _).trans <|
  Equiv.prodCongr singletonEquiv <|
  appendEquiv.symm.trans <|
  congr (List.eraseIdx_eq_take_drop_succ φs n).symm

              

@[simp]
lemma eraseIdxEquiv_apply_snd {n : ℕ} (ψs : CrAnSection φs) (hn : n < φs.length) :
    (eraseIdxEquiv n φs hn ψs).snd = eraseIdx n ψs := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ ((eraseIdxEquiv n φs hn) ψs).2 = eraseIdx n ψs
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ ↑((eraseIdxEquiv n φs hn) ψs).2 = ↑(eraseIdx n ψs)
  simp only [eraseIdxEquiv, appendEquiv, take, List.take_concat_get', List.length_take, drop,
    append, Equiv.trans_apply, Equiv.coe_fn_mk, congr_fst, Equiv.prodCongr_apply, Equiv.coe_trans,
    Equiv.coe_prodComm, Equiv.coe_refl, Prod.map_apply, Function.comp_apply, Prod.swap_prod_mk,
    id_eq, Equiv.prodAssoc_apply, Equiv.coe_fn_symm_mk, eraseIdx]𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take (min n φs.length) (List.take (min (n + 1) φs.length) ↑ψs) ++ List.drop (min (n + 1) φs.length) ↑ψs =
  (↑ψs).eraseIdx n
  rw [Nat.min_eq_left (Nat.le_of_succ_le hn),𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take n (List.take (min (n + 1) φs.length) ↑ψs) ++ List.drop (min (n + 1) φs.length) ↑ψs = (↑ψs).eraseIdx n𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take (min n n.succ) ↑ψs ++ List.drop n.succ ↑ψs = (↑ψs).eraseIdx n Nat.min_eq_left hn,𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take n (List.take n.succ ↑ψs) ++ List.drop n.succ ↑ψs = (↑ψs).eraseIdx n𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take (min n n.succ) ↑ψs ++ List.drop n.succ ↑ψs = (↑ψs).eraseIdx n List.take_take𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take (min n n.succ) ↑ψs ++ List.drop n.succ ↑ψs = (↑ψs).eraseIdx n𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take (min n n.succ) ↑ψs ++ List.drop n.succ ↑ψs = (↑ψs).eraseIdx n]𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take (min n n.succ) ↑ψs ++ List.drop n.succ ↑ψs = (↑ψs).eraseIdx n
  simp only [Nat.succ_eq_add_one, le_add_iff_nonneg_right, zero_le, inf_of_le_left]𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕψs:CrAnSection φshn:n < φs.length⊢ List.take n ↑ψs ++ List.drop (n + 1) ↑ψs = (↑ψs).eraseIdx n
  exact Eq.symm (List.eraseIdx_eq_take_drop_succ ψs.1 n)All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma eraseIdxEquiv_symm_eq_take_cons_drop {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length)
    (a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
    (eraseIdxEquiv n φs hn).symm ⟨a, s⟩ =
    congr (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ List.take n (φs.eraseIdx n) ++ φs[n] :: List.drop n (φs.eraseIdx n) = φs
    rw [Physlib.List.take_eraseIdx_same,𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ List.take n φs ++ φs[n] :: List.drop n (φs.eraseIdx n) = φs𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ List.take n φs ++ List.drop n φs = φs Physlib.List.drop_eraseIdx_succ𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ List.take n φs ++ List.drop n φs = φs𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ List.take n φs ++ List.drop n φs = φs]𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ List.take n φs ++ List.drop n φs = φs
    conv_rhs => rw [← List.take_append_drop n φs]𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)| List.take n φs ++ List.drop n φs) (append (take n s) (cons a (drop n s))) := by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (eraseIdxEquiv n φs hn).symm (a, s) = (congr ⋯) ((take n s).append (cons a (drop n s)))
  simp only [eraseIdxEquiv, appendEquiv, Equiv.symm_trans_apply, congr_symm, Equiv.prodCongr_symm,
    Equiv.refl_symm, Equiv.prodCongr_apply, Prod.map_apply, Equiv.symm_symm, Equiv.coe_fn_mk,
    take_congr, congr_trans_apply, drop_congr, Equiv.prodAssoc_symm_apply, Equiv.coe_refl,
    Equiv.prodComm_symm, Equiv.prodComm_apply, Prod.swap_prod_mk, Equiv.coe_fn_symm_mk,
    congr_fst_append, id_eq, congr_snd_append]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯) (((take (List.take n φs).length s).append (singletonEquiv.symm a)).append (drop (List.take n φs).length s)) =
  (congr ⋯) ((take n s).append (cons a (drop n s)))
  rw [append_assoc',𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯)
    ((congr ⋯)
      ((take (List.take n φs).length s).append ((singletonEquiv.symm a).append (drop (List.take n φs).length s)))) =
  (congr ⋯) ((take n s).append (cons a (drop n s)))𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯) ((congr ⋯) ((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s)))) =
  (congr ⋯) ((take n s).append (cons a (drop n s))) singletonEquiv_append_eq_cons𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯) ((congr ⋯) ((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s)))) =
  (congr ⋯) ((take n s).append (cons a (drop n s)))𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯) ((congr ⋯) ((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s)))) =
  (congr ⋯) ((take n s).append (cons a (drop n s)))]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯) ((congr ⋯) ((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s)))) =
  (congr ⋯) ((take n s).append (cons a (drop n s)))
  simp only [List.singleton_append, congr_trans_apply]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (congr ⋯) ((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  (congr ⋯) ((take n s).append (cons a (drop n s)))
  apply Subtype.ext𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ ↑((congr ⋯) ((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s)))) =
  ↑((congr ⋯) ((take n s).append (cons a (drop n s))))
  simp only [congr_fst]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))
  have hn : (List.take n φs).length = n := by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (eraseIdxEquiv n φs hn).symm (a, s) = (congr ⋯) ((take n s).append (cons a (drop n s)))𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))
    rw [@List.length_take𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ min n φs.length = n𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ min n φs.length = n𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ min n φs.length = n𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))
    simp only [inf_eq_left]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n ≤ φs.length𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))
    exact Nat.le_of_succ_le hn𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take (List.take n φs).length s).append (cons a (drop (List.take n φs).length s))) =
  ↑((take n s).append (cons a (drop n s)))
  rw [hn𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)hn:(List.take n φs).length = n⊢ ↑((take n s).append (cons a (drop n s))) = ↑((take n s).append (cons a (drop n s)))All goals completed! 🐙]All goals completed! 🐙

@[simp]
lemma eraseIdxEquiv_symm_getElem {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length)
    (a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
    getElem ((eraseIdxEquiv n φs hn).symm ⟨a,s⟩).1 n
    (by𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n < (↑((eraseIdxEquiv n φs hn).symm (a, s))).length rw [length_eq𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n < φs.length𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n < φs.length]𝓕✝:FieldSpecification𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n < φs.length; exact hnAll goals completed! 🐙) = ⟨φs[n], a⟩ := by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (↑((eraseIdxEquiv n φs hn).symm (a, s)))[n] = ⟨φs[n], a⟩
  simp only [eraseIdxEquiv_symm_eq_take_cons_drop, append, take, cons, drop, congr_fst,
    List.length_take, length_eq, inf_le_left, List.getElem_append_right]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩
  have h0 : n ⊓ (φs.eraseIdx n).length = n := by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (↑((eraseIdxEquiv n φs hn).symm (a, s)))[n] = ⟨φs[n], a⟩𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)h0:min n (φs.eraseIdx n).length = n⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩
    simp only [inf_eq_left]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n ≤ (φs.eraseIdx n).length𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)h0:min n (φs.eraseIdx n).length = n⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩
    rw [← Physlib.List.eraseIdx_length _ ⟨n, hn⟩𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengthhn:n < (φs.eraseIdx ↑⟨n, hn✝⟩).length + 1a:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n ≤ (φs.eraseIdx n).length𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengthhn:n < (φs.eraseIdx ↑⟨n, hn✝⟩).length + 1a:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n ≤ (φs.eraseIdx n).length𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)h0:min n (φs.eraseIdx n).length = n⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩] at hn𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn✝:n < φs.lengthhn:n < (φs.eraseIdx ↑⟨n, hn✝⟩).length + 1a:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ n ≤ (φs.eraseIdx n).length𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)h0:min n (φs.eraseIdx n).length = n⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩
    exact Nat.le_of_lt_succ hn𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)h0:min n (φs.eraseIdx n).length = n⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)h0:min n (φs.eraseIdx n).length = n⊢ (⟨φs[n], a⟩ :: List.drop n ↑s)[n - min n (φs.eraseIdx n).length] = ⟨φs[n], a⟩
  simp [h0]All goals completed! 🐙

@[simp]
lemma eraseIdxEquiv_symm_eraseIdx {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length)
    (a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) :
    ((eraseIdxEquiv n φs hn).symm ⟨a, s⟩).1.eraseIdx n = s.1 := by𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ (↑((eraseIdxEquiv n φs hn).symm (a, s))).eraseIdx n = ↑s
  change (((eraseIdxEquiv n φs hn).symm ⟨a, s⟩).eraseIdx n).1 = _𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ ↑(eraseIdx n ((eraseIdxEquiv n φs hn).symm (a, s))) = ↑s
  rw [← eraseIdxEquiv_apply_snd _ hn𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ ↑((eraseIdxEquiv n φs hn) ((eraseIdxEquiv n φs hn).symm (a, s))).2 = ↑s𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ ↑((eraseIdxEquiv n φs hn) ((eraseIdxEquiv n φs hn).symm (a, s))).2 = ↑s]𝓕:FieldSpecificationn:ℕφs:List 𝓕.FieldOphn:n < φs.lengtha:𝓕.fieldOpToCrAnType φs[n]s:CrAnSection (φs.eraseIdx n)⊢ ↑((eraseIdxEquiv n φs hn) ((eraseIdxEquiv n φs hn).symm (a, s))).2 = ↑s
  simpAll goals completed! 🐙

lemma sum_eraseIdxEquiv (n : ℕ) (φs : List 𝓕.FieldOp) (hn : n < φs.length)
    (f : CrAnSection φs → M) [AddCommMonoid M] : ∑ (s : CrAnSection φs), f s =
    ∑ (a : 𝓕.fieldOpToCrAnType φs[n]), ∑ (s : CrAnSection (φs.eraseIdx n)),
    f ((eraseIdxEquiv n φs hn).symm ⟨a, s⟩) := by𝓕:FieldSpecificationM:Type u_1n:ℕφs:List 𝓕.FieldOphn:n < φs.lengthf:CrAnSection φs → Minst✝:AddCommMonoid M⊢ ∑ s, f s = ∑ a, ∑ s, f ((eraseIdxEquiv n φs hn).symm (a, s))
  rw [← (eraseIdxEquiv n φs hn).symm.sum_comp𝓕:FieldSpecificationM:Type u_1n:ℕφs:List 𝓕.FieldOphn:n < φs.lengthf:CrAnSection φs → Minst✝:AddCommMonoid M⊢ ∑ i, f ((eraseIdxEquiv n φs hn).symm i) = ∑ a, ∑ s, f ((eraseIdxEquiv n φs hn).symm (a, s))𝓕:FieldSpecificationM:Type u_1n:ℕφs:List 𝓕.FieldOphn:n < φs.lengthf:CrAnSection φs → Minst✝:AddCommMonoid M⊢ ∑ i, f ((eraseIdxEquiv n φs hn).symm i) = ∑ a, ∑ s, f ((eraseIdxEquiv n φs hn).symm (a, s))]𝓕:FieldSpecificationM:Type u_1n:ℕφs:List 𝓕.FieldOphn:n < φs.lengthf:CrAnSection φs → Minst✝:AddCommMonoid M⊢ ∑ i, f ((eraseIdxEquiv n φs hn).symm i) = ∑ a, ∑ s, f ((eraseIdxEquiv n φs hn).symm (a, s))
  rw [Fintype.sum_prod_type𝓕:FieldSpecificationM:Type u_1n:ℕφs:List 𝓕.FieldOphn:n < φs.lengthf:CrAnSection φs → Minst✝:AddCommMonoid M⊢ ∑ x, ∑ y, f ((eraseIdxEquiv n φs hn).symm (x, y)) = ∑ a, ∑ s, f ((eraseIdxEquiv n φs hn).symm (a, s))All goals completed! 🐙]All goals completed! 🐙