Physlib.QFT.PerturbationTheory.FieldStatistics.Basic

Imports

/-
Copyright (c) 2024 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.Mathematics.List.InsertIdx
public import Mathlib.Tactic.FinCases
public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
public import Mathlib.Data.Fintype.Card
public import Mathlib.Algebra.FreeMonoid.Basic
public import Mathlib.Data.List.Sort

Field statistics

Basic properties related to whether a field, or list of fields, is bosonic or fermionic.

@[expose] public section

The type FieldStatistic is the type containing two elements bosonic and fermionic. This type is used to specify if a field or operator obeys bosonic or fermionic statistics.

inductive FieldStatistic : Type where
  | bosonic : FieldStatistic
  | fermionic : FieldStatistic
deriving DecidableEq

The type FieldStatistic carries an instance of a commutative group in which

bosonic * bosonic = bosonic

bosonic * fermionic = fermionic

fermionic * bosonic = fermionic

fermionic * fermionic = bosonic

This group is isomorphic to ℤ₂.

@[simp]
instance : CommGroup FieldStatistic where
  one := bosonic
  mul a b :=
    match a, b with
    | bosonic, bosonic => bosonic
    | bosonic, fermionic => fermionic
    | fermionic, bosonic => fermionic
    | fermionic, fermionic => bosonic
  inv a := a
  mul_assoc a b c := by𝓕:Typea:FieldStatisticb:FieldStatisticc:FieldStatistic⊢ a * b * c = a * (b * c)
    cases abosonic𝓕:Typeb:FieldStatisticc:FieldStatistic⊢ bosonic * b * c = bosonic * (b * c)fermionic𝓕:Typeb:FieldStatisticc:FieldStatistic⊢ fermionic * b * c = fermionic * (b * c) <;>bosonic𝓕:Typeb:FieldStatisticc:FieldStatistic⊢ bosonic * b * c = bosonic * (b * c)fermionic𝓕:Typeb:FieldStatisticc:FieldStatistic⊢ fermionic * b * c = fermionic * (b * c) cases bfermionic.bosonic𝓕:Typec:FieldStatistic⊢ fermionic * bosonic * c = fermionic * (bosonic * c)fermionic.fermionic𝓕:Typec:FieldStatistic⊢ fermionic * fermionic * c = fermionic * (fermionic * c) <;>bosonic.bosonic𝓕:Typec:FieldStatistic⊢ bosonic * bosonic * c = bosonic * (bosonic * c)bosonic.fermionic𝓕:Typec:FieldStatistic⊢ bosonic * fermionic * c = bosonic * (fermionic * c)fermionic.bosonic𝓕:Typec:FieldStatistic⊢ fermionic * bosonic * c = fermionic * (bosonic * c)fermionic.fermionic𝓕:Typec:FieldStatistic⊢ fermionic * fermionic * c = fermionic * (fermionic * c) cases cfermionic.fermionic.bosonic𝓕:Type⊢ fermionic * fermionic * bosonic = fermionic * (fermionic * bosonic)fermionic.fermionic.fermionic𝓕:Type⊢ fermionic * fermionic * fermionic = fermionic * (fermionic * fermionic) <;>bosonic.bosonic.bosonic𝓕:Type⊢ bosonic * bosonic * bosonic = bosonic * (bosonic * bosonic)bosonic.bosonic.fermionic𝓕:Type⊢ bosonic * bosonic * fermionic = bosonic * (bosonic * fermionic)bosonic.fermionic.bosonic𝓕:Type⊢ bosonic * fermionic * bosonic = bosonic * (fermionic * bosonic)bosonic.fermionic.fermionic𝓕:Type⊢ bosonic * fermionic * fermionic = bosonic * (fermionic * fermionic)fermionic.bosonic.bosonic𝓕:Type⊢ fermionic * bosonic * bosonic = fermionic * (bosonic * bosonic)fermionic.bosonic.fermionic𝓕:Type⊢ fermionic * bosonic * fermionic = fermionic * (bosonic * fermionic)fermionic.fermionic.bosonic𝓕:Type⊢ fermionic * fermionic * bosonic = fermionic * (fermionic * bosonic)fermionic.fermionic.fermionic𝓕:Type⊢ fermionic * fermionic * fermionic = fermionic * (fermionic * fermionic)
    dsimp [HMul.hMul]All goals completed! 🐙
  one_mul a := by𝓕:Typea:FieldStatistic⊢ 1 * a = a
    cases abosonic𝓕:Type⊢ 1 * bosonic = bosonicfermionic𝓕:Type⊢ 1 * fermionic = fermionic <;>bosonic𝓕:Type⊢ 1 * bosonic = bosonicfermionic𝓕:Type⊢ 1 * fermionic = fermionic dsimp [HMul.hMul]All goals completed! 🐙
  mul_one a := by𝓕:Typea:FieldStatistic⊢ a * 1 = a
    cases abosonic𝓕:Type⊢ bosonic * 1 = bosonicfermionic𝓕:Type⊢ fermionic * 1 = fermionic <;>bosonic𝓕:Type⊢ bosonic * 1 = bosonicfermionic𝓕:Type⊢ fermionic * 1 = fermionic dsimp [HMul.hMul]All goals completed! 🐙
  inv_mul_cancel a := by𝓕:Typea:FieldStatistic⊢ a * a = 1
    cases abosonic𝓕:Type⊢ bosonic * bosonic = 1fermionic𝓕:Type⊢ fermionic * fermionic = 1 <;>bosonic𝓕:Type⊢ bosonic * bosonic = 1fermionic𝓕:Type⊢ fermionic * fermionic = 1 dsimp only [HMul.hMul, Nat.succ_eq_add_one]fermionic𝓕:Type⊢ bosonic = 1 <;>bosonic𝓕:Type⊢ bosonic = 1fermionic𝓕:Type⊢ bosonic = 1 rflAll goals completed! 🐙
  mul_comm a b := by𝓕:Typea:FieldStatisticb:FieldStatistic⊢ a * b = b * a
    cases abosonic𝓕:Typeb:FieldStatistic⊢ bosonic * b = b * bosonicfermionic𝓕:Typeb:FieldStatistic⊢ fermionic * b = b * fermionic <;>bosonic𝓕:Typeb:FieldStatistic⊢ bosonic * b = b * bosonicfermionic𝓕:Typeb:FieldStatistic⊢ fermionic * b = b * fermionic cases bfermionic.bosonic𝓕:Type⊢ fermionic * bosonic = bosonic * fermionicfermionic.fermionic𝓕:Type⊢ fermionic * fermionic = fermionic * fermionic <;>bosonic.bosonic𝓕:Type⊢ bosonic * bosonic = bosonic * bosonicbosonic.fermionic𝓕:Type⊢ bosonic * fermionic = fermionic * bosonicfermionic.bosonic𝓕:Type⊢ fermionic * bosonic = bosonic * fermionicfermionic.fermionic𝓕:Type⊢ fermionic * fermionic = fermionic * fermionic rflAll goals completed! 🐙

              @[simp]
lemma bosonic_mul_bosonic : bosonic * bosonic = bosonic := rfl@[simp]
lemma bosonic_mul_fermionic : bosonic * fermionic = fermionic := rfl@[simp]
lemma fermionic_mul_bosonic : fermionic * bosonic = fermionic := rfl@[simp]
lemma fermionic_mul_fermionic : fermionic * fermionic = bosonic := rfl@[simp]
lemma mul_bosonic (a : FieldStatistic) : a * bosonic = a := bya:FieldStatistic⊢ a * bosonic = a
  cases abosonic⊢ bosonic * bosonic = bosonicfermionic⊢ fermionic * bosonic = fermionic <;>bosonic⊢ bosonic * bosonic = bosonicfermionic⊢ fermionic * bosonic = fermionic rflAll goals completed! 🐙@[simp]
lemma mul_self (a : FieldStatistic) : a * a = 1 := bya:FieldStatistic⊢ a * a = 1
  cases abosonic⊢ bosonic * bosonic = 1fermionic⊢ fermionic * fermionic = 1 <;>bosonic⊢ bosonic * bosonic = 1fermionic⊢ fermionic * fermionic = 1 rflAll goals completed! 🐙

Field statics form a finite type.

instance : Fintype FieldStatistic where
  elems := {bosonic, fermionic}
  complete := by𝓕:Type⊢ ∀ (x : FieldStatistic), x ∈ {bosonic, fermionic}
    intro c𝓕:Typec:FieldStatistic⊢ c ∈ {bosonic, fermionic}
    cases cbosonic𝓕:Type⊢ bosonic ∈ {bosonic, fermionic}fermionic𝓕:Type⊢ fermionic ∈ {bosonic, fermionic}
    ·bosonic𝓕:Type⊢ bosonic ∈ {bosonic, fermionic} exact Finset.mem_insert_self bosonic {fermionic}All goals completed! 🐙
    ·fermionic𝓕:Type⊢ fermionic ∈ {bosonic, fermionic} refine Finset.insert_eq_self.mp ?_fermionic𝓕:Type⊢ {fermionic, bosonic, fermionic} = {bosonic, fermionic}
      exact rflAll goals completed! 🐙

              @[simp]
lemma fermionic_not_eq_bonsic : ¬ fermionic = bosonic := by⊢ ¬fermionic = bosonic
  intro hh:fermionic = bosonic⊢ False
  exact FieldStatistic.noConfusion hAll goals completed! 🐙lemma bonsic_eq_fermionic_false : bosonic = fermionic ↔ false := by⊢ bosonic = fermionic ↔ false = true
  simp only [reduceCtorEq, Bool.false_eq_true]All goals completed! 🐙@[simp]
lemma neq_fermionic_iff_eq_bosonic (a : FieldStatistic) : ¬ a = fermionic ↔ a = bosonic := bya:FieldStatistic⊢ ¬a = fermionic ↔ a = bosonic
  fin_cases a«0»⊢ ¬bosonic = fermionic ↔ bosonic = bosonic«1»⊢ ¬fermionic = fermionic ↔ fermionic = bosonic
  ·«0»⊢ ¬bosonic = fermionic ↔ bosonic = bosonic simpAll goals completed! 🐙
  ·«1»⊢ ¬fermionic = fermionic ↔ fermionic = bosonic simpAll goals completed! 🐙@[simp]
lemma neq_bosonic_iff_eq_fermionic (a : FieldStatistic) : ¬ a = bosonic ↔ a = fermionic := bya:FieldStatistic⊢ ¬a = bosonic ↔ a = fermionic
  fin_cases a«0»⊢ ¬bosonic = bosonic ↔ bosonic = fermionic«1»⊢ ¬fermionic = bosonic ↔ fermionic = fermionic
  ·«0»⊢ ¬bosonic = bosonic ↔ bosonic = fermionic simpAll goals completed! 🐙
  ·«1»⊢ ¬fermionic = bosonic ↔ fermionic = fermionic simpAll goals completed! 🐙@[simp]
lemma bosonic_ne_iff_fermionic_eq (a : FieldStatistic) : ¬ bosonic = a ↔ fermionic = a := bya:FieldStatistic⊢ ¬bosonic = a ↔ fermionic = a
  fin_cases a«0»⊢ ¬bosonic = bosonic ↔ fermionic = bosonic«1»⊢ ¬bosonic = fermionic ↔ fermionic = fermionic
  ·«0»⊢ ¬bosonic = bosonic ↔ fermionic = bosonic simpAll goals completed! 🐙
  ·«1»⊢ ¬bosonic = fermionic ↔ fermionic = fermionic simpAll goals completed! 🐙@[simp]
lemma fermionic_ne_iff_bosonic_eq (a : FieldStatistic) : ¬ fermionic = a ↔ bosonic = a := bya:FieldStatistic⊢ ¬fermionic = a ↔ bosonic = a
  fin_cases a«0»⊢ ¬fermionic = bosonic ↔ bosonic = bosonic«1»⊢ ¬fermionic = fermionic ↔ bosonic = fermionic
  ·«0»⊢ ¬fermionic = bosonic ↔ bosonic = bosonic simpAll goals completed! 🐙
  ·«1»⊢ ¬fermionic = fermionic ↔ bosonic = fermionic simpAll goals completed! 🐙lemma eq_self_if_eq_bosonic {a : FieldStatistic} :
    (if a = bosonic then bosonic else fermionic) = a := bya:FieldStatistic⊢ (if a = bosonic then bosonic else fermionic) = a
  fin_cases a«0»⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic«1»⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic <;>«0»⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic«1»⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic rflAll goals completed! 🐙lemma eq_self_if_bosonic_eq {a : FieldStatistic} :
    (if bosonic = a then bosonic else fermionic) = a := bya:FieldStatistic⊢ (if bosonic = a then bosonic else fermionic) = a
  fin_cases a«0»⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic«1»⊢ (if bosonic = fermionic then bosonic else fermionic) = fermionic <;>«0»⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic«1»⊢ (if bosonic = fermionic then bosonic else fermionic) = fermionic rflAll goals completed! 🐙lemma mul_eq_one_iff (a b : FieldStatistic) : a * b = 1 ↔ a = b := bya:FieldStatisticb:FieldStatistic⊢ a * b = 1 ↔ a = b
  fin_cases a«0»b:FieldStatistic⊢ bosonic * b = 1 ↔ bosonic = b«1»b:FieldStatistic⊢ fermionic * b = 1 ↔ fermionic = b <;>«0»b:FieldStatistic⊢ bosonic * b = 1 ↔ bosonic = b«1»b:FieldStatistic⊢ fermionic * b = 1 ↔ fermionic = b fin_cases b«1».«0»⊢ fermionic * bosonic = 1 ↔ fermionic = bosonic«1».«1»⊢ fermionic * fermionic = 1 ↔ fermionic = fermionic <;>«0».«0»⊢ bosonic * bosonic = 1 ↔ bosonic = bosonic«0».«1»⊢ bosonic * fermionic = 1 ↔ bosonic = fermionic«1».«0»⊢ fermionic * bosonic = 1 ↔ fermionic = bosonic«1».«1»⊢ fermionic * fermionic = 1 ↔ fermionic = fermionic simpAll goals completed! 🐙lemma one_eq_mul_iff (a b : FieldStatistic) : 1 = a * b ↔ a = b := bya:FieldStatisticb:FieldStatistic⊢ 1 = a * b ↔ a = b
  fin_cases a«0»b:FieldStatistic⊢ 1 = bosonic * b ↔ bosonic = b«1»b:FieldStatistic⊢ 1 = fermionic * b ↔ fermionic = b <;>«0»b:FieldStatistic⊢ 1 = bosonic * b ↔ bosonic = b«1»b:FieldStatistic⊢ 1 = fermionic * b ↔ fermionic = b fin_cases b«1».«0»⊢ 1 = fermionic * bosonic ↔ fermionic = bosonic«1».«1»⊢ 1 = fermionic * fermionic ↔ fermionic = fermionic <;>«0».«0»⊢ 1 = bosonic * bosonic ↔ bosonic = bosonic«0».«1»⊢ 1 = bosonic * fermionic ↔ bosonic = fermionic«1».«0»⊢ 1 = fermionic * bosonic ↔ fermionic = bosonic«1».«1»⊢ 1 = fermionic * fermionic ↔ fermionic = fermionic simpAll goals completed! 🐙lemma mul_eq_iff_eq_mul (a b c : FieldStatistic) : a * b = c ↔ a = b * c := bya:FieldStatisticb:FieldStatisticc:FieldStatistic⊢ a * b = c ↔ a = b * c
  fin_cases a«0»b:FieldStatisticc:FieldStatistic⊢ bosonic * b = c ↔ bosonic = b * c«1»b:FieldStatisticc:FieldStatistic⊢ fermionic * b = c ↔ fermionic = b * c <;>«0»b:FieldStatisticc:FieldStatistic⊢ bosonic * b = c ↔ bosonic = b * c«1»b:FieldStatisticc:FieldStatistic⊢ fermionic * b = c ↔ fermionic = b * c fin_cases b«1».«0»c:FieldStatistic⊢ fermionic * bosonic = c ↔ fermionic = bosonic * c«1».«1»c:FieldStatistic⊢ fermionic * fermionic = c ↔ fermionic = fermionic * c <;>«0».«0»c:FieldStatistic⊢ bosonic * bosonic = c ↔ bosonic = bosonic * c«0».«1»c:FieldStatistic⊢ bosonic * fermionic = c ↔ bosonic = fermionic * c«1».«0»c:FieldStatistic⊢ fermionic * bosonic = c ↔ fermionic = bosonic * c«1».«1»c:FieldStatistic⊢ fermionic * fermionic = c ↔ fermionic = fermionic * c fin_cases c«1».«1».«0»⊢ fermionic * fermionic = bosonic ↔ fermionic = fermionic * bosonic«1».«1».«1»⊢ fermionic * fermionic = fermionic ↔ fermionic = fermionic * fermionic <;>«0».«0».«0»⊢ bosonic * bosonic = bosonic ↔ bosonic = bosonic * bosonic«0».«0».«1»⊢ bosonic * bosonic = fermionic ↔ bosonic = bosonic * fermionic«0».«1».«0»⊢ bosonic * fermionic = bosonic ↔ bosonic = fermionic * bosonic«0».«1».«1»⊢ bosonic * fermionic = fermionic ↔ bosonic = fermionic * fermionic«1».«0».«0»⊢ fermionic * bosonic = bosonic ↔ fermionic = bosonic * bosonic«1».«0».«1»⊢ fermionic * bosonic = fermionic ↔ fermionic = bosonic * fermionic«1».«1».«0»⊢ fermionic * fermionic = bosonic ↔ fermionic = fermionic * bosonic«1».«1».«1»⊢ fermionic * fermionic = fermionic ↔ fermionic = fermionic * fermionic
    simp only [bosonic_mul_fermionic, fermionic_not_eq_bonsic, mul_self,
      reduceCtorEq, fermionic_mul_bosonic, true_iff, iff_true]All goals completed! 🐙
  all_goals rflAll goals completed! 🐙lemma mul_eq_iff_eq_mul' (a b c : FieldStatistic) : a * b = c ↔ b = a * c := bya:FieldStatisticb:FieldStatisticc:FieldStatistic⊢ a * b = c ↔ b = a * c
  fin_cases a«0»b:FieldStatisticc:FieldStatistic⊢ bosonic * b = c ↔ b = bosonic * c«1»b:FieldStatisticc:FieldStatistic⊢ fermionic * b = c ↔ b = fermionic * c <;>«0»b:FieldStatisticc:FieldStatistic⊢ bosonic * b = c ↔ b = bosonic * c«1»b:FieldStatisticc:FieldStatistic⊢ fermionic * b = c ↔ b = fermionic * c fin_cases b«1».«0»c:FieldStatistic⊢ fermionic * bosonic = c ↔ bosonic = fermionic * c«1».«1»c:FieldStatistic⊢ fermionic * fermionic = c ↔ fermionic = fermionic * c <;>«0».«0»c:FieldStatistic⊢ bosonic * bosonic = c ↔ bosonic = bosonic * c«0».«1»c:FieldStatistic⊢ bosonic * fermionic = c ↔ fermionic = bosonic * c«1».«0»c:FieldStatistic⊢ fermionic * bosonic = c ↔ bosonic = fermionic * c«1».«1»c:FieldStatistic⊢ fermionic * fermionic = c ↔ fermionic = fermionic * c fin_cases c«1».«1».«0»⊢ fermionic * fermionic = bosonic ↔ fermionic = fermionic * bosonic«1».«1».«1»⊢ fermionic * fermionic = fermionic ↔ fermionic = fermionic * fermionic <;>«0».«0».«0»⊢ bosonic * bosonic = bosonic ↔ bosonic = bosonic * bosonic«0».«0».«1»⊢ bosonic * bosonic = fermionic ↔ bosonic = bosonic * fermionic«0».«1».«0»⊢ bosonic * fermionic = bosonic ↔ fermionic = bosonic * bosonic«0».«1».«1»⊢ bosonic * fermionic = fermionic ↔ fermionic = bosonic * fermionic«1».«0».«0»⊢ fermionic * bosonic = bosonic ↔ bosonic = fermionic * bosonic«1».«0».«1»⊢ fermionic * bosonic = fermionic ↔ bosonic = fermionic * fermionic«1».«1».«0»⊢ fermionic * fermionic = bosonic ↔ fermionic = fermionic * bosonic«1».«1».«1»⊢ fermionic * fermionic = fermionic ↔ fermionic = fermionic * fermionic
    simp only [bosonic_mul_fermionic, fermionic_not_eq_bonsic, mul_self,
      reduceCtorEq, fermionic_mul_bosonic, true_iff, iff_true]All goals completed! 🐙
  all_goals rflAll goals completed! 🐙

The field statistics of a list of fields is fermionic if there is an odd number of fermions, otherwise it is bosonic.

def ofList (s : 𝓕 → FieldStatistic) : (φs : List 𝓕) → FieldStatistic
  | [] => bosonic
  | φ :: φs => if s φ = ofList s φs then bosonic else fermionic

              

lemma ofList_cons_eq_mul (s : 𝓕 → FieldStatistic) (φ : 𝓕) (φs : List 𝓕) :
    ofList s (φ :: φs) = s φ * ofList s φs := by𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ ofList s (φ :: φs) = s φ * ofList s φs
  have ha (a b : FieldStatistic) : (if a = b then bosonic else fermionic) = a * b := by
    fin_cases a«0»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕b:FieldStatistic⊢ (if bosonic = b then bosonic else fermionic) = bosonic * b«1»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕b:FieldStatistic⊢ (if fermionic = b then bosonic else fermionic) = fermionic * b𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ ofList s (φ :: φs) = s φ * ofList s φs <;>«0»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕b:FieldStatistic⊢ (if bosonic = b then bosonic else fermionic) = bosonic * b«1»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕b:FieldStatistic⊢ (if fermionic = b then bosonic else fermionic) = fermionic * b𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ ofList s (φ :: φs) = s φ * ofList s φs fin_cases b«1».«0»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic * bosonic«1».«1»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (if fermionic = fermionic then bosonic else fermionic) = fermionic * fermionic𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ ofList s (φ :: φs) = s φ * ofList s φs <;>«0».«0»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic * bosonic«0».«1»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (if bosonic = fermionic then bosonic else fermionic) = bosonic * fermionic«1».«0»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic * bosonic«1».«1»𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (if fermionic = fermionic then bosonic else fermionic) = fermionic * fermionic𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ ofList s (φ :: φs) = s φ * ofList s φs rfl𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ ofList s (φ :: φs) = s φ * ofList s φs𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ ofList s (φ :: φs) = s φ * ofList s φs
  exact ha (s φ) (ofList s φs)All goals completed! 🐙

lemma ofList_eq_prod (s : 𝓕 → FieldStatistic) : (φs : List 𝓕) →
    ofList s φs = (List.map s φs).prod
  | [] => rfl
  | φ :: φs =>𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ ofList s (φ :: φs) = (List.map s (φ :: φs)).prod by𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ ofList s (φ :: φs) = (List.map s (φ :: φs)).prod
    rw [ofList_cons_eq_mul,𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ s φ * ofList s φs = (List.map s (φ :: φs)).prodAll goals completed! 🐙 List.map_cons,𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ s φ * ofList s φs = (s φ :: List.map s φs).prodAll goals completed! 🐙 List.prod_cons,𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ s φ * ofList s φs = s φ * (List.map s φs).prodAll goals completed! 🐙 ofList_eq_prod𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ s φ * (List.map s φs).prod = s φ * (List.map s φs).prodAll goals completed! 🐙]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
@[simp]
lemma ofList_singleton (s : 𝓕 → FieldStatistic) (φ : 𝓕) : ofList s [φ] = s φ := by𝓕:Types:𝓕 → FieldStatisticφ:𝓕⊢ ofList s [φ] = s φ
  simp only [ofList]𝓕:Types:𝓕 → FieldStatisticφ:𝓕⊢ (if s φ = bosonic then bosonic else fermionic) = s φ
  rw [eq_self_if_eq_bosonic𝓕:Types:𝓕 → FieldStatisticφ:𝓕⊢ s φ = s φAll goals completed! 🐙]All goals completed! 🐙@[simp]
lemma ofList_freeMonoid (s : 𝓕 → FieldStatistic) (φ : 𝓕) : ofList s (FreeMonoid.of φ) = s φ :=
  ofList_singleton s φ@[simp]
lemma ofList_empty (s : 𝓕 → FieldStatistic) : ofList s [] = bosonic := rfl

set_option backward.isDefEq.respectTransparency false in
@[simp]
lemma ofList_append (s : 𝓕 → FieldStatistic) (φs φs' : List 𝓕) :
    ofList s (φs ++ φs') = if ofList s φs = ofList s φs' then bosonic else fermionic := by𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ ofList s (φs ++ φs') = if ofList s φs = ofList s φs' then bosonic else fermionic
  induction φs with
  | nil =>nil𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕⊢ ofList s ([] ++ φs') = if ofList s [] = ofList s φs' then bosonic else fermionic
    simp only [List.nil_append, ofList_empty, eq_self_if_bosonic_eq]All goals completed! 🐙
  | cons a l ih =>cons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic
    have hab (a b c : FieldStatistic) :
        (if a = (if b = c then bosonic else fermionic) then bosonic else fermionic) =
        if (if a = b then bosonic else fermionic) = c then bosonic else fermionic := by𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ ofList s (φs ++ φs') = if ofList s φs = ofList s φs' then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic
      fin_cases a«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicb:FieldStatisticc:FieldStatistic⊢ (if bosonic = if b = c then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = b then bosonic else fermionic) = c then bosonic else fermionic«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicb:FieldStatisticc:FieldStatistic⊢ (if fermionic = if b = c then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = b then bosonic else fermionic) = c then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic <;>«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicb:FieldStatisticc:FieldStatistic⊢ (if bosonic = if b = c then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = b then bosonic else fermionic) = c then bosonic else fermionic«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicb:FieldStatisticc:FieldStatistic⊢ (if fermionic = if b = c then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = b then bosonic else fermionic) = c then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic fin_cases b«1».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicc:FieldStatistic⊢ (if fermionic = if bosonic = c then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = bosonic then bosonic else fermionic) = c then bosonic else fermionic«1».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicc:FieldStatistic⊢ (if fermionic = if fermionic = c then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = fermionic then bosonic else fermionic) = c then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic <;>«0».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicc:FieldStatistic⊢ (if bosonic = if bosonic = c then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = bosonic then bosonic else fermionic) = c then bosonic else fermionic«0».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicc:FieldStatistic⊢ (if bosonic = if fermionic = c then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = fermionic then bosonic else fermionic) = c then bosonic else fermionic«1».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicc:FieldStatistic⊢ (if fermionic = if bosonic = c then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = bosonic then bosonic else fermionic) = c then bosonic else fermionic«1».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionicc:FieldStatistic⊢ (if fermionic = if fermionic = c then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = fermionic then bosonic else fermionic) = c then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic fin_cases c«1».«1».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if fermionic = if fermionic = bosonic then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = fermionic then bosonic else fermionic) = bosonic then bosonic else fermionic«1».«1».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if fermionic = if fermionic = fermionic then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = fermionic then bosonic else fermionic) = fermionic then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic <;>«0».«0».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if bosonic = if bosonic = bosonic then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = bosonic then bosonic else fermionic) = bosonic then bosonic else fermionic«0».«0».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if bosonic = if bosonic = fermionic then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = bosonic then bosonic else fermionic) = fermionic then bosonic else fermionic«0».«1».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if bosonic = if fermionic = bosonic then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = fermionic then bosonic else fermionic) = bosonic then bosonic else fermionic«0».«1».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if bosonic = if fermionic = fermionic then bosonic else fermionic then bosonic else fermionic) =
  if (if bosonic = fermionic then bosonic else fermionic) = fermionic then bosonic else fermionic«1».«0».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if fermionic = if bosonic = bosonic then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = bosonic then bosonic else fermionic) = bosonic then bosonic else fermionic«1».«0».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if fermionic = if bosonic = fermionic then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = bosonic then bosonic else fermionic) = fermionic then bosonic else fermionic«1».«1».«0»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if fermionic = if fermionic = bosonic then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = fermionic then bosonic else fermionic) = bosonic then bosonic else fermionic«1».«1».«1»𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionic⊢ (if fermionic = if fermionic = fermionic then bosonic else fermionic then bosonic else fermionic) =
  if (if fermionic = fermionic then bosonic else fermionic) = fermionic then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic rflcons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermioniccons𝓕:Types:𝓕 → FieldStatisticφs':List 𝓕a:𝓕l:List 𝓕ih:ofList s (l ++ φs') = if ofList s l = ofList s φs' then bosonic else fermionichab:∀ (a b c : FieldStatistic),
  (if a = if b = c then bosonic else fermionic then bosonic else fermionic) =
    if (if a = b then bosonic else fermionic) = c then bosonic else fermionic⊢ ofList s (a :: l ++ φs') = if ofList s (a :: l) = ofList s φs' then bosonic else fermionic
    simp only [List.cons_append, ofList, ih, hab]All goals completed! 🐙

lemma ofList_append_eq_mul (s : 𝓕 → FieldStatistic) (φs φs' : List 𝓕) :
    ofList s (φs ++ φs') = ofList s φs * ofList s φs' := by𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ ofList s (φs ++ φs') = ofList s φs * ofList s φs'
  rw [ofList_append𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs'𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs']𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs'
  have ha (a b : FieldStatistic) : (if a = b then bosonic else fermionic) = a * b := by𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ ofList s (φs ++ φs') = ofList s φs * ofList s φs'𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs'
    fin_cases a«0»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕b:FieldStatistic⊢ (if bosonic = b then bosonic else fermionic) = bosonic * b«1»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕b:FieldStatistic⊢ (if fermionic = b then bosonic else fermionic) = fermionic * b𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs' <;>«0»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕b:FieldStatistic⊢ (if bosonic = b then bosonic else fermionic) = bosonic * b«1»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕b:FieldStatistic⊢ (if fermionic = b then bosonic else fermionic) = fermionic * b𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs' fin_cases b«1».«0»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic * bosonic«1».«1»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if fermionic = fermionic then bosonic else fermionic) = fermionic * fermionic𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs' <;>«0».«0»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic * bosonic«0».«1»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if bosonic = fermionic then bosonic else fermionic) = bosonic * fermionic«1».«0»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic * bosonic«1».«1»𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕⊢ (if fermionic = fermionic then bosonic else fermionic) = fermionic * fermionic𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs' rfl𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs'𝓕:Types:𝓕 → FieldStatisticφs:List 𝓕φs':List 𝓕ha:∀ (a b : FieldStatistic), (if a = b then bosonic else fermionic) = a * b⊢ (if ofList s φs = ofList s φs' then bosonic else fermionic) = ofList s φs * ofList s φs'
  exact ha _ _All goals completed! 🐙

lemma ofList_perm (s : 𝓕 → FieldStatistic) {l l' : List 𝓕} (h : l.Perm l') :
    ofList s l = ofList s l' := by𝓕:Types:𝓕 → FieldStatisticl:List 𝓕l':List 𝓕h:l.Perm l'⊢ ofList s l = ofList s l'
  rw [ofList_eq_prod,𝓕:Types:𝓕 → FieldStatisticl:List 𝓕l':List 𝓕h:l.Perm l'⊢ (List.map s l).prod = ofList s l'𝓕:Types:𝓕 → FieldStatisticl:List 𝓕l':List 𝓕h:l.Perm l'⊢ (List.map s l).prod = (List.map s l').prod ofList_eq_prod𝓕:Types:𝓕 → FieldStatisticl:List 𝓕l':List 𝓕h:l.Perm l'⊢ (List.map s l).prod = (List.map s l').prod𝓕:Types:𝓕 → FieldStatisticl:List 𝓕l':List 𝓕h:l.Perm l'⊢ (List.map s l).prod = (List.map s l').prod]𝓕:Types:𝓕 → FieldStatisticl:List 𝓕l':List 𝓕h:l.Perm l'⊢ (List.map s l).prod = (List.map s l').prod
  exact List.Perm.prod_eq (List.Perm.map s h)All goals completed! 🐙lemma ofList_orderedInsert (s : 𝓕 → FieldStatistic) (le1 : 𝓕 → 𝓕 → Prop) [DecidableRel le1]
    (φs : List 𝓕) (φ : 𝓕) : ofList s (List.orderedInsert le1 φ φs) = ofList s (φ :: φs) :=
  ofList_perm s (List.perm_orderedInsert le1 φ φs)@[simp]
lemma ofList_insertionSort (s : 𝓕 → FieldStatistic) (le1 : 𝓕 → 𝓕 → Prop) [DecidableRel le1]
    (φs : List 𝓕) : ofList s (List.insertionSort le1 φs) = ofList s φs :=
  ofList_perm s (List.perm_insertionSort le1 φs)

lemma ofList_map_eq_finset_prod (s : 𝓕 → FieldStatistic) :
    (φs : List 𝓕) → (l : List (Fin φs.length)) → (hl : l.Nodup) →
    ofList s (l.map φs.get) = ∏ (i : Fin φs.length), if i ∈ l then s φs[i] else 1
  | [], [], _ => rfl
  | [], i :: l, hl => Fin.elim0 i
  | φ :: φs, [], hl =>𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕hl:[].Nodup⊢ ofList s (List.map (φ :: φs).get []) = ∏ i, if i ∈ [] then s (φ :: φs)[i] else 1 by𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕hl:[].Nodup⊢ ofList s (List.map (φ :: φs).get []) = ∏ i, if i ∈ [] then s (φ :: φs)[i] else 1
    simp only [List.length_cons, List.map_nil, ofList_empty, List.not_mem_nil, ↓reduceIte,
      Finset.prod_const_one]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕hl:[].Nodup⊢ bosonic = 1
    rflAll goals completed! 🐙
  | φ :: φs, i :: l, hl =>𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ ofList s (List.map (φ :: φs).get (i :: l)) = ∏ i_1, if i_1 ∈ i :: l then s (φ :: φs)[i_1] else 1 by𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ ofList s (List.map (φ :: φs).get (i :: l)) = ∏ i_1, if i_1 ∈ i :: l then s (φ :: φs)[i_1] else 1
    simp only [List.length_cons, List.map_cons, List.get_eq_getElem, List.mem_cons, Fin.getElem_fin]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ ofList s ((φ :: φs)[↑i] :: List.map (φ :: φs).get l) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1
    rw [ofList_cons_eq_mul𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ s (φ :: φs)[↑i] * ofList s (List.map (φ :: φs).get l) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ s (φ :: φs)[↑i] * ofList s (List.map (φ :: φs).get l) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ s (φ :: φs)[↑i] * ofList s (List.map (φ :: φs).get l) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1
    rw [ofList_map_eq_finset_prod s (φ :: φs) l𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    have h1 : s (φ :: φs)[↑i] = ∏ (j : Fin (φ :: φs).length),
      if j = i then s (φ :: φs)[↑i] else 1 := by𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ ofList s (List.map (φ :: φs).get (i :: l)) = ∏ i_1, if i_1 ∈ i :: l then s (φ :: φs)[i_1] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
      rw [Fintype.prod_ite_eq'𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ s (φ :: φs)[i] = s (φ :: φs)[i]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (s (φ :: φs)[↑i] * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) = ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    erw [h1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ ((∏ j, if j = i then s (φ :: φs)[i] else 1) * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) =
  ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ ((∏ j, if j = i then s (φ :: φs)[i] else 1) * ∏ i, if i ∈ l then s (φ :: φs)[i] else 1) =
  ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    rw [← Finset.prod_mul_distrib𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (∏ x, (if x = i then s (φ :: φs)[i] else 1) * if x ∈ l then s (φ :: φs)[x] else 1) =
  ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (∏ x, (if x = i then s (φ :: φs)[i] else 1) * if x ∈ l then s (φ :: φs)[x] else 1) =
  ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup]𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (∏ x, (if x = i then s (φ :: φs)[i] else 1) * if x ∈ l then s (φ :: φs)[x] else 1) =
  ∏ x, if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    congre_f𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1⊢ (fun x => (if x = i then s (φ :: φs)[i] else 1) * if x ∈ l then s (φ :: φs)[x] else 1) = fun x =>
  if x = i ∨ x ∈ l then s (φ :: φs)[↑x] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    funext ae_f𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).length⊢ ((if a = i then s (φ :: φs)[i] else 1) * if a ∈ l then s (φ :: φs)[a] else 1) =
  if a = i ∨ a ∈ l then s (φ :: φs)[↑a] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    simp only [List.length_cons, mul_ite, ite_mul, one_mul, mul_one]e_f𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).length⊢ (if a ∈ l then if a = i then s (φ :: φs)[i] * s (φ :: φs)[a] else s (φ :: φs)[a]
  else if a = i then s (φ :: φs)[i] else 1) =
  if a = i ∨ a ∈ l then s (φ :: φs)[↑a] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    by_cases ha : a = ipos𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ (if a ∈ l then if a = i then s (φ :: φs)[i] * s (φ :: φs)[a] else s (φ :: φs)[a]
  else if a = i then s (φ :: φs)[i] else 1) =
  if a = i ∨ a ∈ l then s (φ :: φs)[↑a] else 1neg𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:¬a = i⊢ (if a ∈ l then if a = i then s (φ :: φs)[i] * s (φ :: φs)[a] else s (φ :: φs)[a]
  else if a = i then s (φ :: φs)[i] else 1) =
  if a = i ∨ a ∈ l then s (φ :: φs)[↑a] else 1𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Nodup⊢ l.Nodup
    ·pos𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ (if a ∈ l then if a = i then s (φ :: φs)[i] * s (φ :: φs)[a] else s (φ :: φs)[a]
  else if a = i then s (φ :: φs)[i] else 1) =
  if a = i ∨ a ∈ l then s (φ :: φs)[↑a] else 1 simp only [ha, ↓reduceIte, mul_self, true_or]pos𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ (if i ∈ l then 1 else s (φ :: φs)[i]) = s (φ :: φs)[↑i]
      rw [if_negpos𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ s (φ :: φs)[i] = s (φ :: φs)[↑i]pos.hnc𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ i ∉ lpos𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ s (φ :: φs)[i] = s (φ :: φs)[↑i]pos.hnc𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ i ∉ l]pos𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ s (φ :: φs)[i] = s (φ :: φs)[↑i]pos.hnc𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ i ∉ l
      rflpos.hnc𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = i⊢ i ∉ l
      simp only [List.length_cons, List.nodup_cons] at hlpos.hnc𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)h1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:a = ihl:i ∉ l ∧ l.Nodup⊢ i ∉ l
      exact hl.1All goals completed! 🐙
    ·neg𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:¬a = i⊢ (if a ∈ l then if a = i then s (φ :: φs)[i] * s (φ :: φs)[a] else s (φ :: φs)[a]
  else if a = i then s (φ :: φs)[i] else 1) =
  if a = i ∨ a ∈ l then s (φ :: φs)[↑a] else 1 simp only [ha, ↓reduceIte, false_or]neg𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:(i :: l).Noduph1:s (φ :: φs)[i] = ∏ j, if j = i then s (φ :: φs)[i] else 1a:Fin (φ :: φs).lengthha:¬a = i⊢ (if a ∈ l then s (φ :: φs)[a] else 1) = if a ∈ l then s (φ :: φs)[↑a] else 1
      rflAll goals completed! 🐙
    simp only [List.length_cons, List.nodup_cons] at hl𝓕:Types:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕i:Fin (φ :: φs).lengthl:List (Fin (φ :: φs).length)hl:i ∉ l ∧ l.Nodup⊢ l.Nodup
    exact hl.2All goals completed! 🐙

lemma ofList_pair (s : 𝓕 → FieldStatistic) (φ1 φ2 : 𝓕) :
    ofList s [φ1, φ2] = s φ1 * s φ2 := by𝓕:Types:𝓕 → FieldStatisticφ1:𝓕φ2:𝓕⊢ ofList s [φ1, φ2] = s φ1 * s φ2
  rw [ofList_cons_eq_mul,𝓕:Types:𝓕 → FieldStatisticφ1:𝓕φ2:𝓕⊢ s φ1 * ofList s [φ2] = s φ1 * s φ2All goals completed! 🐙 ofList_singleton𝓕:Types:𝓕 → FieldStatisticφ1:𝓕φ2:𝓕⊢ s φ1 * s φ2 = s φ1 * s φ2All goals completed! 🐙]All goals completed! 🐙

ofList and take

              
lemma ofList_take_insert (n : ℕ) (φ : 𝓕) (φs : List 𝓕) :
    ofList q (List.take n φs) = ofList q (List.take n (List.insertIdx φs n φ)) := by𝓕:Typeq:𝓕 → FieldStatisticn:ℕφ:𝓕φs:List 𝓕⊢ ofList q (List.take n φs) = ofList q (List.take n (φs.insertIdx n φ))
  congr 1e_φs𝓕:Typeq:𝓕 → FieldStatisticn:ℕφ:𝓕φs:List 𝓕⊢ List.take n φs = List.take n (φs.insertIdx n φ)
  rw [take_insert_samee_φs𝓕:Typeq:𝓕 → FieldStatisticn:ℕφ:𝓕φs:List 𝓕⊢ List.take n φs = List.take n φsAll goals completed! 🐙]All goals completed! 🐙

lemma ofList_take_eraseIdx (n : ℕ) (φs : List 𝓕) :
    ofList q (List.take n (φs.eraseIdx n)) = ofList q (List.take n φs) := by𝓕:Typeq:𝓕 → FieldStatisticn:ℕφs:List 𝓕⊢ ofList q (List.take n (φs.eraseIdx n)) = ofList q (List.take n φs)
  congr 1e_φs𝓕:Typeq:𝓕 → FieldStatisticn:ℕφs:List 𝓕⊢ List.take n (φs.eraseIdx n) = List.take n φs
  rw [take_eraseIdx_samee_φs𝓕:Typeq:𝓕 → FieldStatisticn:ℕφs:List 𝓕⊢ List.take n φs = List.take n φsAll goals completed! 🐙]All goals completed! 🐙lemma ofList_take_zero (φs : List 𝓕) :
    ofList q (List.take 0 φs) = 1 := by𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕⊢ ofList q (List.take 0 φs) = 1
  simp only [List.take_zero, ofList_empty]𝓕:Typeq:𝓕 → FieldStatisticφs:List 𝓕⊢ bosonic = 1
  rflAll goals completed! 🐙

lemma ofList_take_succ_cons (n : ℕ) (φ1 : 𝓕) (φs : List 𝓕) :
    ofList q ((φ1 :: φs).take (n + 1)) = q φ1 * ofList q (φs.take n) := by𝓕:Typeq:𝓕 → FieldStatisticn:ℕφ1:𝓕φs:List 𝓕⊢ ofList q (List.take (n + 1) (φ1 :: φs)) = q φ1 * ofList q (List.take n φs)
  simp only [List.take_succ_cons]𝓕:Typeq:𝓕 → FieldStatisticn:ℕφ1:𝓕φs:List 𝓕⊢ ofList q (φ1 :: List.take n φs) = q φ1 * ofList q (List.take n φs)
  rw [ofList_cons_eq_mul𝓕:Typeq:𝓕 → FieldStatisticn:ℕφ1:𝓕φs:List 𝓕⊢ q φ1 * ofList q (List.take n φs) = q φ1 * ofList q (List.take n φs)All goals completed! 🐙]All goals completed! 🐙

lemma ofList_take_insertIdx_gt (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn : n < m) :
    ofList q ((List.insertIdx φs m φ1).take n) = ofList q (φs.take n) := by𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:n < m⊢ ofList q (List.take n (φs.insertIdx m φ1)) = ofList q (List.take n φs)
  rw [take_insert_gt φ1 n m hn φs𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:n < m⊢ ofList q (List.take n φs) = ofList q (List.take n φs)All goals completed! 🐙]All goals completed! 🐙lemma ofList_insert_lt_eq (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn : m ≤ n)
    (hm : m ≤ φs.length) :
    ofList q ((List.insertIdx φs m φ1).take (n + 1)) =
    ofList q ((φ1 :: φs).take (n + 1)) := by𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ ofList q (List.take (n + 1) (φs.insertIdx m φ1)) = ofList q (List.take (n + 1) (φ1 :: φs))
  apply ofList_perm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ (List.take (n + 1) (φs.insertIdx m φ1)).Perm (List.take (n + 1) (φ1 :: φs))
  simp only [List.take_succ_cons]𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ (List.take (n + 1) (φs.insertIdx m φ1)).Perm (φ1 :: List.take n φs)
  refine take_insert_let φ1 n m hn φs hmAll goals completed! 🐙

lemma ofList_take_insertIdx_le (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn : m ≤ n) (hm : m ≤ φs.length) :
    ofList q ((List.insertIdx φs m φ1).take (n + 1)) = q φ1 * ofList q (φs.take n) := by𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ ofList q (List.take (n + 1) (φs.insertIdx m φ1)) = q φ1 * ofList q (List.take n φs)
  rw [ofList_insert_lt_eq,𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ ofList q (List.take (n + 1) (φ1 :: φs)) = q φ1 * ofList q (List.take n φs)hn𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ nhm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ φs.lengthhn𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ nhm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ φs.length ofList_take_succ_cons𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ q φ1 * ofList q (List.take n φs) = q φ1 * ofList q (List.take n φs)hn𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ nhm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ φs.lengthhn𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ nhm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ φs.length]hn𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ nhm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ φs.length
  ·hn𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ n exact hnAll goals completed! 🐙
  ·hm𝓕:Typeq:𝓕 → FieldStatisticn:ℕm:ℕφ1:𝓕φs:List 𝓕hn:m ≤ nhm:m ≤ φs.length⊢ m ≤ φs.length exact hmAll goals completed! 🐙

The instance of an additive monoid on FieldStatistic.


instance : AddMonoid FieldStatistic where
  zero := bosonic
  add a b := a * b
  nsmul n a := ∏ (i : Fin n), a
  zero_add a := by𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ 0 + a = a
    cases abosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ 0 + bosonic = bosonicfermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ 0 + fermionic = fermionic <;>bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ 0 + bosonic = bosonicfermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ 0 + fermionic = fermionic rflAll goals completed! 🐙
  add_zero a := by𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ a + 0 = a
    cases abosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ bosonic + 0 = bosonicfermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + 0 = fermionic <;>bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ bosonic + 0 = bosonicfermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + 0 = fermionic rflAll goals completed! 🐙
  add_assoc a b c := by𝓕:Typeq:𝓕 → FieldStatistica:FieldStatisticb:FieldStatisticc:FieldStatistic⊢ a + b + c = a + (b + c)
    cases abosonic𝓕:Typeq:𝓕 → FieldStatisticb:FieldStatisticc:FieldStatistic⊢ bosonic + b + c = bosonic + (b + c)fermionic𝓕:Typeq:𝓕 → FieldStatisticb:FieldStatisticc:FieldStatistic⊢ fermionic + b + c = fermionic + (b + c) <;>bosonic𝓕:Typeq:𝓕 → FieldStatisticb:FieldStatisticc:FieldStatistic⊢ bosonic + b + c = bosonic + (b + c)fermionic𝓕:Typeq:𝓕 → FieldStatisticb:FieldStatisticc:FieldStatistic⊢ fermionic + b + c = fermionic + (b + c) cases bfermionic.bosonic𝓕:Typeq:𝓕 → FieldStatisticc:FieldStatistic⊢ fermionic + bosonic + c = fermionic + (bosonic + c)fermionic.fermionic𝓕:Typeq:𝓕 → FieldStatisticc:FieldStatistic⊢ fermionic + fermionic + c = fermionic + (fermionic + c) <;>bosonic.bosonic𝓕:Typeq:𝓕 → FieldStatisticc:FieldStatistic⊢ bosonic + bosonic + c = bosonic + (bosonic + c)bosonic.fermionic𝓕:Typeq:𝓕 → FieldStatisticc:FieldStatistic⊢ bosonic + fermionic + c = bosonic + (fermionic + c)fermionic.bosonic𝓕:Typeq:𝓕 → FieldStatisticc:FieldStatistic⊢ fermionic + bosonic + c = fermionic + (bosonic + c)fermionic.fermionic𝓕:Typeq:𝓕 → FieldStatisticc:FieldStatistic⊢ fermionic + fermionic + c = fermionic + (fermionic + c) cases cfermionic.fermionic.bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + fermionic + bosonic = fermionic + (fermionic + bosonic)fermionic.fermionic.fermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + fermionic + fermionic = fermionic + (fermionic + fermionic) <;>bosonic.bosonic.bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ bosonic + bosonic + bosonic = bosonic + (bosonic + bosonic)bosonic.bosonic.fermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ bosonic + bosonic + fermionic = bosonic + (bosonic + fermionic)bosonic.fermionic.bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ bosonic + fermionic + bosonic = bosonic + (fermionic + bosonic)bosonic.fermionic.fermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ bosonic + fermionic + fermionic = bosonic + (fermionic + fermionic)fermionic.bosonic.bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + bosonic + bosonic = fermionic + (bosonic + bosonic)fermionic.bosonic.fermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + bosonic + fermionic = fermionic + (bosonic + fermionic)fermionic.fermionic.bosonic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + fermionic + bosonic = fermionic + (fermionic + bosonic)fermionic.fermionic.fermionic𝓕:Typeq:𝓕 → FieldStatistic⊢ fermionic + fermionic + fermionic = fermionic + (fermionic + fermionic) rflAll goals completed! 🐙
  nsmul_zero a := by𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ 0 • a = 0
    show (∏ _i : Fin 0, a) = (1 : FieldStatistic)𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ ∏ _i, a = 1
    rw [Finset.prod_const,𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ a ^ Finset.univ.card = 1All goals completed! 🐙 Finset.card_univ,𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ a ^ Fintype.card (Fin 0) = 1All goals completed! 🐙 Fintype.card_fin,𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ a ^ 0 = 1All goals completed! 🐙 pow_zero𝓕:Typeq:𝓕 → FieldStatistica:FieldStatistic⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙
  nsmul_succ a n := by𝓕:Typeq:𝓕 → FieldStatistica:ℕn:FieldStatistic⊢ (a + 1) • n = a • n + n
    show (∏ _i : Fin (a + 1), n) = (∏ _i : Fin a, n) * n𝓕:Typeq:𝓕 → FieldStatistica:ℕn:FieldStatistic⊢ ∏ _i, n = (∏ _i, n) * n
    simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin, pow_succ]All goals completed! 🐙

@[simp]
lemma add_eq_mul (a b : FieldStatistic) : a + b = a * b := rfl