Physlib.QFT.PerturbationTheory.WickAlgebra.Grading

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.WickAlgebra.Basic

Grading on the field operation algebra

@[expose] public section

The submodule of 𝓕.WickAlgebra spanned by lists of field statistic f.

def statSubmodule (f : FieldStatistic) : Submodule ℂ 𝓕.WickAlgebra :=
  Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ (𝓕 |>ₛ φs) = f}

              lemma ofCrAnList_mem_statSubmodule_of_eq (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic)
    (h : (𝓕 |>ₛ φs) = f) : ofCrAnList φs ∈ statSubmodule f :=
  Submodule.mem_span.mpr fun _ a => a ⟨φs, ⟨rfl, h⟩⟩lemma ofCrAnList_mem_statSubmodule (φs : List 𝓕.CrAnFieldOp) :
    ofCrAnList φs ∈ statSubmodule (𝓕 |>ₛ φs) :=
  Submodule.mem_span.mpr fun _ a => a ⟨φs, ⟨rfl, rfl⟩⟩lemma mem_bosonic_of_mem_free_bosonic (a : 𝓕.FieldOpFreeAlgebra)
    (h : a ∈ statisticSubmodule bosonic) : ι a ∈ statSubmodule .bosonic := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonic⊢ ι a ∈ statSubmodule bosonic
  let p (a : 𝓕.FieldOpFreeAlgebra) (hx : a ∈ statisticSubmodule bosonic) : Prop :=
    ι a ∈ statSubmodule .bosonic𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ι a ∈ statSubmodule bosonic
  change p a h𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ p a h
  apply Submodule.span_inductionmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}), p x ⋯zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ p 0 ⋯add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}),
  p x hx → p y hy → p (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}),
  p x hx → p (a • x) ⋯
  ·mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}), p x ⋯ intro x hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicx:𝓕.FieldOpFreeAlgebrahx:x ∈ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}⊢ p x ⋯
    simp only [Set.mem_setOf_eq] at hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicx:𝓕.FieldOpFreeAlgebrahx:∃ φs, x = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic⊢ p x ⋯
    obtain ⟨φs, rfl, h⟩ := hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicφs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ p (ofCrAnListF φs) ⋯
    simp [p]mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicφs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ι (ofCrAnListF φs) ∈ statSubmodule bosonic
    apply ofCrAnList_mem_statSubmodule_of_eqmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicφs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ofList 𝓕.crAnStatistics φs = bosonic
    exact hAll goals completed! 🐙
  ·zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ p 0 ⋯ simp only [map_zero, p]zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ 0 ∈ statSubmodule bosonic
    exact Submodule.zero_mem (statSubmodule bosonic)All goals completed! 🐙
  ·add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}),
  p x hx → p y hy → p (x + y) ⋯ intro x y hx hy hpx hpyadd𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hpx:p x hxhpy:p y hy⊢ p (x + y) ⋯
    simp_all only [p, map_add]add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonicx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hpx:ι x ∈ statSubmodule bosonichpy:ι y ∈ statSubmodule bosonic⊢ ι x + ι y ∈ statSubmodule bosonic
    exact Submodule.add_mem _ hpx hpyAll goals completed! 🐙
  ·smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonic⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}),
  p x hx → p (a • x) ⋯ intro a x hx hysmul𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonica:ℂx:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hy:p x hx⊢ p (a • x) ⋯
    simp_all only [p, map_smul]smul𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule bosonic → Prop := fun a hx => ι a ∈ statSubmodule bosonica:ℂx:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hy:ι x ∈ statSubmodule bosonic⊢ a • ι x ∈ statSubmodule bosonic
    exact Submodule.smul_mem _ _ hyAll goals completed! 🐙lemma mem_fermionic_of_mem_free_fermionic (a : 𝓕.FieldOpFreeAlgebra)
    (h : a ∈ statisticSubmodule fermionic) : ι a ∈ statSubmodule .fermionic := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionic⊢ ι a ∈ statSubmodule fermionic
  let p (a : 𝓕.FieldOpFreeAlgebra) (hx : a ∈ statisticSubmodule fermionic) : Prop :=
    ι a ∈ statSubmodule .fermionic𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ι a ∈ statSubmodule fermionic
  change p a h𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ p a h
  apply Submodule.span_inductionmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}), p x ⋯zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ p 0 ⋯add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p y hy → p (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p (a • x) ⋯
  ·mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}), p x ⋯ intro x hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicx:𝓕.FieldOpFreeAlgebrahx:x ∈ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}⊢ p x ⋯
    simp only [Set.mem_setOf_eq] at hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicx:𝓕.FieldOpFreeAlgebrahx:∃ φs, x = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic⊢ p x ⋯
    obtain ⟨φs, rfl, h⟩ := hxmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicφs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ p (ofCrAnListF φs) ⋯
    simp [p]mem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicφs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ι (ofCrAnListF φs) ∈ statSubmodule fermionic
    apply ofCrAnList_mem_statSubmodule_of_eqmem𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicφs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ofList 𝓕.crAnStatistics φs = fermionic
    exact hAll goals completed! 🐙
  ·zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ p 0 ⋯ simp only [map_zero, p]zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ 0 ∈ statSubmodule fermionic
    exact Submodule.zero_mem (statSubmodule fermionic)All goals completed! 🐙
  ·add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p y hy → p (x + y) ⋯ intro x y hx hy hpx hpyadd𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hpx:p x hxhpy:p y hy⊢ p (x + y) ⋯
    simp_all only [p, map_add]add𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionicx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hpx:ι x ∈ statSubmodule fermionichpy:ι y ∈ statSubmodule fermionic⊢ ι x + ι y ∈ statSubmodule fermionic
    exact Submodule.add_mem _ hpx hpyAll goals completed! 🐙
  ·smul𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionic⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p (a • x) ⋯ intro a x hx hysmul𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionica:ℂx:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hy:p x hx⊢ p (a • x) ⋯
    simp_all only [p, map_smul]smul𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) → a ∈ statisticSubmodule fermionic → Prop := fun a hx => ι a ∈ statSubmodule fermionica:ℂx:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnListF φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hy:ι x ∈ statSubmodule fermionic⊢ a • ι x ∈ statSubmodule fermionic
    exact Submodule.smul_mem _ _ hyAll goals completed! 🐙lemma mem_statSubmodule_of_mem_statisticSubmodule (f : FieldStatistic) (a : 𝓕.FieldOpFreeAlgebra)
    (h : a ∈ statisticSubmodule f) : ι a ∈ statSubmodule f := by𝓕:FieldSpecificationf:FieldStatistica:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule f⊢ ι a ∈ statSubmodule f
  fin_cases f«0»𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonic⊢ ι a ∈ statSubmodule bosonic«1»𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionic⊢ ι a ∈ statSubmodule fermionic
  ·«0»𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonic⊢ ι a ∈ statSubmodule bosonic exact mem_bosonic_of_mem_free_bosonic a hAll goals completed! 🐙
  ·«1»𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionic⊢ ι a ∈ statSubmodule fermionic exact mem_fermionic_of_mem_free_fermionic a hAll goals completed! 🐙

The projection of statisticSubmodule (𝓕 := 𝓕) f defined in the free algebra to statSubmodule (𝓕 := 𝓕) f.

def ιStateSubmodule (f : FieldStatistic) :
    statisticSubmodule (𝓕 := 𝓕) f →ₗ[ℂ] statSubmodule (𝓕 := 𝓕) f where
  toFun a := ⟨a.1, mem_statSubmodule_of_mem_statisticSubmodule f a.1 a.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Defining bosonicProj

The projection of 𝓕.FieldOpFreeAlgebra to statSubmodule (𝓕 := 𝓕) bosonic.

def bosonicProjFree : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] statSubmodule (𝓕 := 𝓕) bosonic :=
  ιStateSubmodule .bosonic ∘ₗ bosonicProjF

              lemma bosonicProjFree_eq_ι_bosonicProjF (a : 𝓕.FieldOpFreeAlgebra) :
    (bosonicProjFree a).1 = ι (bosonicProjF a) := rfl

lemma bosonicProjFree_zero_of_ι_zero (a : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) :
    bosonicProjFree a = 0 := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι a = 0⊢ bosonicProjFree a = 0
  rw [ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ bosonicProjFree a = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ bosonicProjFree a = 0] at h𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ bosonicProjFree a = 0
  apply Subtype.ext𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ↑(bosonicProjFree a) = ↑0
  rw [bosonicProjFree_eq_ι_bosonicProjF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ι ↑(bosonicProjF a) = ↑0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ι ↑(bosonicProjF a) = ↑0]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ι ↑(bosonicProjF a) = ↑0
  exact h.1All goals completed! 🐙

lemma bosonicProjFree_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
    bosonicProjFree a = bosonicProjFree b := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:a ≈ b⊢ bosonicProjFree a = bosonicProjFree b
  rw [equiv_iff_sub_mem_ideal,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:a - b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ bosonicProjFree a = bosonicProjFree b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ bosonicProjFree a = bosonicProjFree b ← ι_eq_zero_iff_mem_ideal𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ bosonicProjFree a = bosonicProjFree b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ bosonicProjFree a = bosonicProjFree b] at h𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ bosonicProjFree a = bosonicProjFree b
  rw [LinearMap.sub_mem_ker_iff.mp𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ bosonicProjFree ?m.35 = bosonicProjFree b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ a - ?m.35 ∈ bosonicProjFree.ker𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ 𝓕.FieldOpFreeAlgebra𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ a - b ∈ bosonicProjFree.ker]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ a - b ∈ bosonicProjFree.ker
  simp only [LinearMap.mem_ker]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ bosonicProjFree (a - b) = 0
  exact bosonicProjFree_zero_of_ι_zero (a - b) hAll goals completed! 🐙

The projection of 𝓕.WickAlgebra to statSubmodule (𝓕 := 𝓕) bosonic.


def bosonicProj : 𝓕.WickAlgebra →ₗ[ℂ] statSubmodule (𝓕 := 𝓕) bosonic where
  toFun := Quotient.lift bosonicProjFree bosonicProjFree_eq_of_equiv
  map_add' x y := by𝓕:FieldSpecificationx:𝓕.WickAlgebray:𝓕.WickAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ (x + y) = Quotient.lift ⇑bosonicProjFree ⋯ x + Quotient.lift ⇑bosonicProjFree ⋯ y
    obtain ⟨x, hx⟩ := ι_surjective x𝓕:FieldSpecificationx✝:𝓕.WickAlgebray:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebrahx:ι x = x✝⊢ Quotient.lift ⇑bosonicProjFree ⋯ (x + y) = Quotient.lift ⇑bosonicProjFree ⋯ x + Quotient.lift ⇑bosonicProjFree ⋯ y
    obtain ⟨y, hy⟩ := ι_surjective y𝓕:FieldSpecificationx✝:𝓕.WickAlgebray✝:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebrahx:ι x = x✝y:𝓕.FieldOpFreeAlgebrahy:ι y = y✝⊢ Quotient.lift ⇑bosonicProjFree ⋯ (x + y) = Quotient.lift ⇑bosonicProjFree ⋯ x + Quotient.lift ⇑bosonicProjFree ⋯ y
    subst hx hy𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ (ι x + ι y) =
  Quotient.lift ⇑bosonicProjFree ⋯ (ι x) + Quotient.lift ⇑bosonicProjFree ⋯ (ι y)
    rw [← map_add,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ (ι (x + y)) =
  Quotient.lift ⇑bosonicProjFree ⋯ (ι x) + Quotient.lift ⇑bosonicProjFree ⋯ (ι y)𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧ ι_apply,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑bosonicProjFree ⋯ (ι x) + Quotient.lift ⇑bosonicProjFree ⋯ (ι y)𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧ ι_apply,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ (ι y)𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧ ι_apply𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧]𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦x + y⟧ = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧
    rw [Quotient.lift_mk,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = Quotient.lift ⇑bosonicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = bosonicProjFree x + bosonicProjFree y Quotient.lift_mk,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = bosonicProjFree x + Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = bosonicProjFree x + bosonicProjFree y Quotient.lift_mk𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = bosonicProjFree x + bosonicProjFree y𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = bosonicProjFree x + bosonicProjFree y]𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ bosonicProjFree (x + y) = bosonicProjFree x + bosonicProjFree y
    simpAll goals completed! 🐙
  map_smul' c y := by𝓕:FieldSpecificationc:ℂy:𝓕.WickAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ (c • y) = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ y
    obtain ⟨y, hy⟩ := ι_surjective y𝓕:FieldSpecificationc:ℂy✝:𝓕.WickAlgebray:𝓕.FieldOpFreeAlgebrahy:ι y = y✝⊢ Quotient.lift ⇑bosonicProjFree ⋯ (c • y) = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ y
    subst hy𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ (c • ι y) = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ (ι y)
    rw [← map_smul,𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ (ι (c • y)) = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ (ι y)𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧ ι_apply,𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ (ι y)𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧ ι_apply𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧]𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑bosonicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑bosonicProjFree ⋯ ⟦y⟧
    simpAll goals completed! 🐙

lemma bosonicProj_eq_bosonicProjFree (a : 𝓕.FieldOpFreeAlgebra) :
    bosonicProj (ι a) = bosonicProjFree a := rfl

Defining fermionicProj

The projection of 𝓕.FieldOpFreeAlgebra to statSubmodule (𝓕 := 𝓕) fermionic.

def fermionicProjFree : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] statSubmodule (𝓕 := 𝓕) fermionic :=
  ιStateSubmodule .fermionic ∘ₗ fermionicProjF

              lemma fermionicProjFree_eq_ι_fermionicProjF (a : 𝓕.FieldOpFreeAlgebra) :
    (fermionicProjFree a).1 = ι (fermionicProjF a) := rfl

lemma fermionicProjFree_zero_of_ι_zero (a : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) :
    fermionicProjFree a = 0 := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι a = 0⊢ fermionicProjFree a = 0
  rw [ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ fermionicProjFree a = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ fermionicProjFree a = 0] at h𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ fermionicProjFree a = 0
  apply Subtype.ext𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ↑(fermionicProjFree a) = ↑0
  rw [fermionicProjFree_eq_ι_fermionicProjF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ι ↑(fermionicProjF a) = ↑0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ι ↑(fermionicProjF a) = ↑0]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF a) = 0 ∧ ι ↑(fermionicProjF a) = 0⊢ ι ↑(fermionicProjF a) = ↑0
  exact h.2All goals completed! 🐙

lemma fermionicProjFree_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
    fermionicProjFree a = fermionicProjFree b := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:a ≈ b⊢ fermionicProjFree a = fermionicProjFree b
  rw [equiv_iff_sub_mem_ideal,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:a - b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ fermionicProjFree a = fermionicProjFree b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ fermionicProjFree a = fermionicProjFree b ← ι_eq_zero_iff_mem_ideal𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ fermionicProjFree a = fermionicProjFree b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ fermionicProjFree a = fermionicProjFree b] at h𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ fermionicProjFree a = fermionicProjFree b
  rw [LinearMap.sub_mem_ker_iff.mp𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ fermionicProjFree ?m.35 = fermionicProjFree b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ a - ?m.35 ∈ fermionicProjFree.ker𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ 𝓕.FieldOpFreeAlgebra𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ a - b ∈ fermionicProjFree.ker]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ a - b ∈ fermionicProjFree.ker
  simp only [LinearMap.mem_ker]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι (a - b) = 0⊢ fermionicProjFree (a - b) = 0
  exact fermionicProjFree_zero_of_ι_zero (a - b) hAll goals completed! 🐙

The projection of 𝓕.WickAlgebra to statSubmodule (𝓕 := 𝓕) fermionic.


def fermionicProj : 𝓕.WickAlgebra →ₗ[ℂ] statSubmodule (𝓕 := 𝓕) fermionic where
  toFun := Quotient.lift fermionicProjFree fermionicProjFree_eq_of_equiv
  map_add' x y := by𝓕:FieldSpecificationx:𝓕.WickAlgebray:𝓕.WickAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ (x + y) = Quotient.lift ⇑fermionicProjFree ⋯ x + Quotient.lift ⇑fermionicProjFree ⋯ y
    obtain ⟨x, hx⟩ := ι_surjective x𝓕:FieldSpecificationx✝:𝓕.WickAlgebray:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebrahx:ι x = x✝⊢ Quotient.lift ⇑fermionicProjFree ⋯ (x + y) = Quotient.lift ⇑fermionicProjFree ⋯ x + Quotient.lift ⇑fermionicProjFree ⋯ y
    obtain ⟨y, hy⟩ := ι_surjective y𝓕:FieldSpecificationx✝:𝓕.WickAlgebray✝:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebrahx:ι x = x✝y:𝓕.FieldOpFreeAlgebrahy:ι y = y✝⊢ Quotient.lift ⇑fermionicProjFree ⋯ (x + y) = Quotient.lift ⇑fermionicProjFree ⋯ x + Quotient.lift ⇑fermionicProjFree ⋯ y
    subst hx hy𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ (ι x + ι y) =
  Quotient.lift ⇑fermionicProjFree ⋯ (ι x) + Quotient.lift ⇑fermionicProjFree ⋯ (ι y)
    rw [← map_add,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ (ι (x + y)) =
  Quotient.lift ⇑fermionicProjFree ⋯ (ι x) + Quotient.lift ⇑fermionicProjFree ⋯ (ι y)𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧ ι_apply,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ (ι x) + Quotient.lift ⇑fermionicProjFree ⋯ (ι y)𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧ ι_apply,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ (ι y)𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧ ι_apply𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧]𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦x + y⟧ =
  Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧
    rw [Quotient.lift_mk,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = Quotient.lift ⇑fermionicProjFree ⋯ ⟦x⟧ + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = fermionicProjFree x + fermionicProjFree y Quotient.lift_mk,𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = fermionicProjFree x + Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = fermionicProjFree x + fermionicProjFree y Quotient.lift_mk𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = fermionicProjFree x + fermionicProjFree y𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = fermionicProjFree x + fermionicProjFree y]𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ fermionicProjFree (x + y) = fermionicProjFree x + fermionicProjFree y
    simpAll goals completed! 🐙
  map_smul' c y := by𝓕:FieldSpecificationc:ℂy:𝓕.WickAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ (c • y) = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ y
    obtain ⟨y, hy⟩ := ι_surjective y𝓕:FieldSpecificationc:ℂy✝:𝓕.WickAlgebray:𝓕.FieldOpFreeAlgebrahy:ι y = y✝⊢ Quotient.lift ⇑fermionicProjFree ⋯ (c • y) = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ y
    subst hy𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ (c • ι y) = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ (ι y)
    rw [← map_smul,𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ (ι (c • y)) = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ (ι y)𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧ ι_apply,𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ (ι y)𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧ ι_apply𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧]𝓕:FieldSpecificationc:ℂy:𝓕.FieldOpFreeAlgebra⊢ Quotient.lift ⇑fermionicProjFree ⋯ ⟦c • y⟧ = (RingHom.id ℂ) c • Quotient.lift ⇑fermionicProjFree ⋯ ⟦y⟧
    simpAll goals completed! 🐙

lemma fermionicProj_eq_fermionicProjFree (a : 𝓕.FieldOpFreeAlgebra) :
    fermionicProj (ι a) = fermionicProjFree a := rfl

Interaction between bosonicProj and fermionicProj

              

lemma bosonicProj_add_fermionicProj (a : 𝓕.WickAlgebra) :
    bosonicProj a + (fermionicProj a).1 = a := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ ↑(bosonicProj a) + ↑(fermionicProj a) = a
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ↑(bosonicProj (ι a)) + ↑(fermionicProj (ι a)) = ι a
  rw [fermionicProj_eq_fermionicProjFree,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ↑(bosonicProj (ι a)) + ↑(fermionicProjFree a) = ι a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ↑(bosonicProjFree a) + ↑(fermionicProjFree a) = ι a bosonicProj_eq_bosonicProjFree𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ↑(bosonicProjFree a) + ↑(fermionicProjFree a) = ι a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ↑(bosonicProjFree a) + ↑(fermionicProjFree a) = ι a]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ↑(bosonicProjFree a) + ↑(fermionicProjFree a) = ι a
  rw [bosonicProjFree_eq_ι_bosonicProjF,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι ↑(bosonicProjF a) + ↑(fermionicProjFree a) = ι a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι ↑(bosonicProjF a) + ι ↑(fermionicProjF a) = ι a fermionicProjFree_eq_ι_fermionicProjF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι ↑(bosonicProjF a) + ι ↑(fermionicProjF a) = ι a𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι ↑(bosonicProjF a) + ι ↑(fermionicProjF a) = ι a]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι ↑(bosonicProjF a) + ι ↑(fermionicProjF a) = ι a
  rw [← map_add,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι (↑(bosonicProjF a) + ↑(fermionicProjF a)) = ι aAll goals completed! 🐙 bosonicProjF_add_fermionicProjF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebra⊢ ι a = ι aAll goals completed! 🐙]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma bosonicProj_mem_bosonic (a : 𝓕.WickAlgebra) (ha : a ∈ statSubmodule .bosonic) :
    bosonicProj a = ⟨a, ha⟩ := by𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonic⊢ bosonicProj a = ⟨a, ha⟩
  let p (a : 𝓕.WickAlgebra) (hx : a ∈ statSubmodule bosonic) : Prop :=
    (bosonicProj a) = ⟨a, hx⟩𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ bosonicProj a = ⟨a, ha⟩
  change p a ha𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ p a ha
  apply Submodule.span_inductionmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}), p x ⋯zero𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ p 0 ⋯add𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ ∀ (x y : 𝓕.WickAlgebra) (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}),
  p x hx → p y hy → p (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}), p x hx → p (a • x) ⋯
  ·mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}), p x ⋯ intro x hxmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩x:𝓕.WickAlgebrahx:x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}⊢ p x ⋯
    obtain ⟨φs, rfl, h⟩ := hxmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ p (ofCrAnList φs) ⋯
    simp only [p]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ bosonicProj (ofCrAnList φs) = ⟨ofCrAnList φs, ⋯⟩
    apply Subtype.extmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProj (ofCrAnList φs)) = ↑⟨ofCrAnList φs, ⋯⟩
    simp onlymem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProj (ofCrAnList φs)) = ofCrAnList φs
    rw [ofCrAnListmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProj (ι (ofCrAnListF φs))) = ι (ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProj (ι (ofCrAnListF φs))) = ι (ofCrAnListF φs)]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProj (ι (ofCrAnListF φs))) = ι (ofCrAnListF φs)
    rw [bosonicProj_eq_bosonicProjFreemem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProjFree (ofCrAnListF φs)) = ι (ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProjFree (ofCrAnListF φs)) = ι (ofCrAnListF φs)]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ↑(bosonicProjFree (ofCrAnListF φs)) = ι (ofCrAnListF φs)
    rw [bosonicProjFree_eq_ι_bosonicProjFmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ι ↑(bosonicProjF (ofCrAnListF φs)) = ι (ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ι ↑(bosonicProjF (ofCrAnListF φs)) = ι (ofCrAnListF φs)]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ι ↑(bosonicProjF (ofCrAnListF φs)) = ι (ofCrAnListF φs)
    rw [bosonicProjF_of_mem_bosonicmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ι ↑⟨ofCrAnListF φs, ?mem.h⟩ = ι (ofCrAnListF φs)mem.h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ofCrAnListF φs ∈ statisticSubmodule bosonicmem.h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ofCrAnListF φs ∈ statisticSubmodule bosonic]mem.h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = bosonic⊢ ofCrAnListF φs ∈ statisticSubmodule bosonic
    exact ofCrAnListF_mem_statisticSubmodule_of _ _ hAll goals completed! 🐙
  ·zero𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ p 0 ⋯ simp only [map_zero, p]zero𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ 0 = ⟨0, ⋯⟩
    rflAll goals completed! 🐙
  ·add𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ ∀ (x y : 𝓕.WickAlgebra) (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}),
  p x hx → p y hy → p (x + y) ⋯ intro x y hx hy hpx hpyadd𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩x:𝓕.WickAlgebray:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hpx:p x hxhpy:p y hy⊢ p (x + y) ⋯
    simp_all [p]All goals completed! 🐙
  ·smul𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}), p x hx → p (a • x) ⋯ intro a x hx hysmul𝓕:FieldSpecificationa✝:𝓕.WickAlgebraha:a ∈ statSubmodule bosonicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule bosonic → Prop := fun a hx => bosonicProj a = ⟨a, hx⟩a:ℂx:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic}hy:p x hx⊢ p (a • x) ⋯
    simp_all [p]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma fermionicProj_mem_fermionic (a : 𝓕.WickAlgebra) (ha : a ∈ statSubmodule .fermionic) :
    fermionicProj a = ⟨a, ha⟩ := by𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionic⊢ fermionicProj a = ⟨a, ha⟩
  let p (a : 𝓕.WickAlgebra) (hx : a ∈ statSubmodule fermionic) : Prop :=
    (fermionicProj a) = ⟨a, hx⟩𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ fermionicProj a = ⟨a, ha⟩
  change p a ha𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ p a ha
  apply Submodule.span_inductionmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}), p x ⋯zero𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ p 0 ⋯add𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ ∀ (x y : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p y hy → p (x + y) ⋯smul𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p (a • x) ⋯
  ·mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}), p x ⋯ intro x hxmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩x:𝓕.WickAlgebrahx:x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}⊢ p x ⋯
    obtain ⟨φs, rfl, h⟩ := hxmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ p (ofCrAnList φs) ⋯
    simp only [p]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ fermionicProj (ofCrAnList φs) = ⟨ofCrAnList φs, ⋯⟩
    apply Subtype.extmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProj (ofCrAnList φs)) = ↑⟨ofCrAnList φs, ⋯⟩
    simp onlymem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProj (ofCrAnList φs)) = ofCrAnList φs
    rw [ofCrAnListmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProj (ι (ofCrAnListF φs))) = ι (ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProj (ι (ofCrAnListF φs))) = ι (ofCrAnListF φs)]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProj (ι (ofCrAnListF φs))) = ι (ofCrAnListF φs)
    rw [fermionicProj_eq_fermionicProjFreemem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProjFree (ofCrAnListF φs)) = ι (ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProjFree (ofCrAnListF φs)) = ι (ofCrAnListF φs)]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ↑(fermionicProjFree (ofCrAnListF φs)) = ι (ofCrAnListF φs)
    rw [fermionicProjFree_eq_ι_fermionicProjFmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ι ↑(fermionicProjF (ofCrAnListF φs)) = ι (ofCrAnListF φs)mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ι ↑(fermionicProjF (ofCrAnListF φs)) = ι (ofCrAnListF φs)]mem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ι ↑(fermionicProjF (ofCrAnListF φs)) = ι (ofCrAnListF φs)
    rw [fermionicProjF_of_mem_fermionicmem𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ι ↑⟨ofCrAnListF φs, ?mem.h⟩ = ι (ofCrAnListF φs)mem.h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ofCrAnListF φs ∈ statisticSubmodule fermionicmem.h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ofCrAnListF φs ∈ statisticSubmodule fermionic]mem.h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = fermionic⊢ ofCrAnListF φs ∈ statisticSubmodule fermionic
    exact ofCrAnListF_mem_statisticSubmodule_of _ _ hAll goals completed! 🐙
  ·zero𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ p 0 ⋯ simp only [map_zero, p]zero𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ 0 = ⟨0, ⋯⟩
    rflAll goals completed! 🐙
  ·add𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ ∀ (x y : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p y hy → p (x + y) ⋯ intro x y hx hy hpx hpyadd𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩x:𝓕.WickAlgebray:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hpx:p x hxhpy:p y hy⊢ p (x + y) ⋯
    simp_all [p]All goals completed! 🐙
  ·smul𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}),
  p x hx → p (a • x) ⋯ intro a x hx hysmul𝓕:FieldSpecificationa✝:𝓕.WickAlgebraha:a ∈ statSubmodule fermionicp:(a : 𝓕.WickAlgebra) → a ∈ statSubmodule fermionic → Prop := fun a hx => fermionicProj a = ⟨a, hx⟩a:ℂx:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic}hy:p x hx⊢ p (a • x) ⋯
    simp_all [p]All goals completed! 🐙

lemma bosonicProj_mem_fermionic (a : 𝓕.WickAlgebra) (ha : a ∈ statSubmodule .fermionic) :
    bosonicProj a = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionic⊢ bosonicProj a = 0
  have h := bosonicProj_add_fermionicProj a𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionich:↑(bosonicProj a) + ↑(fermionicProj a) = a⊢ bosonicProj a = 0
  rw [fermionicProj_mem_fermionic a ha𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionich:↑(bosonicProj a) + ↑⟨a, ha⟩ = a⊢ bosonicProj a = 0𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionich:↑(bosonicProj a) + ↑⟨a, ha⟩ = a⊢ bosonicProj a = 0] at h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule fermionich:↑(bosonicProj a) + ↑⟨a, ha⟩ = a⊢ bosonicProj a = 0
  simpa using hAll goals completed! 🐙

lemma fermionicProj_mem_bosonic (a : 𝓕.WickAlgebra) (ha : a ∈ statSubmodule .bosonic) :
    fermionicProj a = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonic⊢ fermionicProj a = 0
  have h := bosonicProj_add_fermionicProj a𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonich:↑(bosonicProj a) + ↑(fermionicProj a) = a⊢ fermionicProj a = 0
  rw [bosonicProj_mem_bosonic a ha𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonich:↑⟨a, ha⟩ + ↑(fermionicProj a) = a⊢ fermionicProj a = 0𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonich:↑⟨a, ha⟩ + ↑(fermionicProj a) = a⊢ fermionicProj a = 0] at h𝓕:FieldSpecificationa:𝓕.WickAlgebraha:a ∈ statSubmodule bosonich:↑⟨a, ha⟩ + ↑(fermionicProj a) = a⊢ fermionicProj a = 0
  simpa using hAll goals completed! 🐙

lemma mem_bosonic_iff_fermionicProj_eq_zero (a : 𝓕.WickAlgebra) :
    a ∈ statSubmodule bosonic ↔ fermionicProj a = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ a ∈ statSubmodule bosonic ↔ fermionicProj a = 0
  apply Iff.intromp𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ a ∈ statSubmodule bosonic → fermionicProj a = 0mpr𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ fermionicProj a = 0 → a ∈ statSubmodule bosonic
  ·mp𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ a ∈ statSubmodule bosonic → fermionicProj a = 0 intro hmp𝓕:FieldSpecificationa:𝓕.WickAlgebrah:a ∈ statSubmodule bosonic⊢ fermionicProj a = 0
    exact fermionicProj_mem_bosonic a hAll goals completed! 🐙
  ·mpr𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ fermionicProj a = 0 → a ∈ statSubmodule bosonic intro hmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0⊢ a ∈ statSubmodule bosonic
    have ha := bosonicProj_add_fermionicProj ampr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) + ↑(fermionicProj a) = a⊢ a ∈ statSubmodule bosonic
    rw [hmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) + ↑0 = a⊢ a ∈ statSubmodule bosonicmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) + ↑0 = a⊢ a ∈ statSubmodule bosonic] at hampr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) + ↑0 = a⊢ a ∈ statSubmodule bosonic
    simp_allmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) = a⊢ a ∈ statSubmodule bosonic
    rw [← hampr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) = a⊢ ↑(bosonicProj a) ∈ statSubmodule bosonicmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) = a⊢ ↑(bosonicProj a) ∈ statSubmodule bosonic]mpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:fermionicProj a = 0ha:↑(bosonicProj a) = a⊢ ↑(bosonicProj a) ∈ statSubmodule bosonic
    exact (bosonicProj a).2All goals completed! 🐙

lemma mem_fermionic_iff_bosonicProj_eq_zero (a : 𝓕.WickAlgebra) :
    a ∈ statSubmodule fermionic ↔ bosonicProj a = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ a ∈ statSubmodule fermionic ↔ bosonicProj a = 0
  apply Iff.intromp𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ a ∈ statSubmodule fermionic → bosonicProj a = 0mpr𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ bosonicProj a = 0 → a ∈ statSubmodule fermionic
  ·mp𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ a ∈ statSubmodule fermionic → bosonicProj a = 0 intro hmp𝓕:FieldSpecificationa:𝓕.WickAlgebrah:a ∈ statSubmodule fermionic⊢ bosonicProj a = 0
    exact bosonicProj_mem_fermionic a hAll goals completed! 🐙
  ·mpr𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ bosonicProj a = 0 → a ∈ statSubmodule fermionic intro hmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0⊢ a ∈ statSubmodule fermionic
    have ha := bosonicProj_add_fermionicProj ampr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑(bosonicProj a) + ↑(fermionicProj a) = a⊢ a ∈ statSubmodule fermionic
    rw [hmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑0 + ↑(fermionicProj a) = a⊢ a ∈ statSubmodule fermionicmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑0 + ↑(fermionicProj a) = a⊢ a ∈ statSubmodule fermionic] at hampr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑0 + ↑(fermionicProj a) = a⊢ a ∈ statSubmodule fermionic
    simp_allmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑(fermionicProj a) = a⊢ a ∈ statSubmodule fermionic
    rw [← hampr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑(fermionicProj a) = a⊢ ↑(fermionicProj a) ∈ statSubmodule fermionicmpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑(fermionicProj a) = a⊢ ↑(fermionicProj a) ∈ statSubmodule fermionic]mpr𝓕:FieldSpecificationa:𝓕.WickAlgebrah:bosonicProj a = 0ha:↑(fermionicProj a) = a⊢ ↑(fermionicProj a) ∈ statSubmodule fermionic
    exact (fermionicProj a).2All goals completed! 🐙

lemma eq_zero_of_bosonic_and_fermionic {a : 𝓕.WickAlgebra}
    (hb : a ∈ statSubmodule bosonic) (hf : a ∈ statSubmodule fermionic) : a = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebrahb:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionic⊢ a = 0
  have ha := bosonicProj_mem_bosonic a hb𝓕:FieldSpecificationa:𝓕.WickAlgebrahb:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩⊢ a = 0
  have hb := fermionicProj_mem_fermionic a hf𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩⊢ a = 0
  have hc := (bosonicProj_add_fermionicProj a)𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩hc:↑(bosonicProj a) + ↑(fermionicProj a) = a⊢ a = 0
  rw [ha,𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩hc:↑⟨a, hb✝⟩ + ↑(fermionicProj a) = a⊢ a = 0𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩hc:↑⟨a, hb✝⟩ + ↑⟨a, hf⟩ = a⊢ a = 0 hb𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩hc:↑⟨a, hb✝⟩ + ↑⟨a, hf⟩ = a⊢ a = 0𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩hc:↑⟨a, hb✝⟩ + ↑⟨a, hf⟩ = a⊢ a = 0] at hc𝓕:FieldSpecificationa:𝓕.WickAlgebrahb✝:a ∈ statSubmodule bosonichf:a ∈ statSubmodule fermionicha:bosonicProj a = ⟨a, hb⟩hb:fermionicProj a = ⟨a, hf⟩hc:↑⟨a, hb✝⟩ + ↑⟨a, hf⟩ = a⊢ a = 0
  simpa using hcAll goals completed! 🐙@[simp]
lemma bosonicProj_fermionicProj_eq_zero (a : 𝓕.WickAlgebra) :
    bosonicProj (fermionicProj a).1 = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ bosonicProj ↑(fermionicProj a) = 0
  apply bosonicProj_mem_fermionic𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ ↑(fermionicProj a) ∈ statSubmodule fermionic
  exact Submodule.coe_mem (fermionicProj a)All goals completed! 🐙@[simp]
lemma fermionicProj_bosonicProj_eq_zero (a : 𝓕.WickAlgebra) :
    fermionicProj (bosonicProj a).1 = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ fermionicProj ↑(bosonicProj a) = 0
  apply fermionicProj_mem_bosonic𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ ↑(bosonicProj a) ∈ statSubmodule bosonic
  exact Submodule.coe_mem (bosonicProj a)All goals completed! 🐙@[simp]
lemma bosonicProj_bosonicProj_eq_bosonicProj (a : 𝓕.WickAlgebra) :
    bosonicProj (bosonicProj a).1 = bosonicProj a := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ bosonicProj ↑(bosonicProj a) = bosonicProj a
  apply bosonicProj_mem_bosonicAll goals completed! 🐙@[simp]
lemma fermionicProj_fermionicProj_eq_fermionicProj (a : 𝓕.WickAlgebra) :
    fermionicProj (fermionicProj a).1 = fermionicProj a := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ fermionicProj ↑(fermionicProj a) = fermionicProj a
  apply fermionicProj_mem_fermionicAll goals completed! 🐙@[simp]
lemma bosonicProj_of_bosonic_part
    (a : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i))) :
    bosonicProj (a bosonic).1 = (a bosonic) := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ bosonicProj ↑(a bosonic) = a bosonic
  apply bosonicProj_mem_bosonicAll goals completed! 🐙@[simp]
lemma bosonicProj_of_fermionic_part
    (a : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i))) :
    bosonicProj (a fermionic).1 = 0 := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ bosonicProj ↑(a fermionic) = 0
  apply bosonicProj_mem_fermionic𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ ↑(a fermionic) ∈ statSubmodule fermionic
  exact Submodule.coe_mem (a.toFun fermionic)All goals completed! 🐙@[simp]
lemma fermionicProj_of_bosonic_part
    (a : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i))) :
    fermionicProj (a bosonic).1 = 0 := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ fermionicProj ↑(a bosonic) = 0
  apply fermionicProj_mem_bosonic𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ ↑(a bosonic) ∈ statSubmodule bosonic
  exact Submodule.coe_mem (a.toFun bosonic)All goals completed! 🐙@[simp]
lemma fermionicProj_of_fermionic_part
    (a : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i))) :
    fermionicProj (a fermionic).1 = (a fermionic) := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ fermionicProj ↑(a fermionic) = a fermionic
  apply fermionicProj_mem_fermionicAll goals completed! 🐙

The grading



lemma coeAddMonoidHom_apply_eq_bosonic_plus_fermionic
    (a : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i))) :
    DirectSum.coeAddMonoidHom statSubmodule a = a.1 bosonic + a.1 fermionic := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)
  let C : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i)) → Prop :=
    fun a => DirectSum.coeAddMonoidHom statSubmodule a = a.1 bosonic + a.1 fermionic𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)
  change C a𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ C a
  apply DirectSum.induction_onzero𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ C 0of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ ∀ (i : FieldStatistic) (x : ↥(statSubmodule i)), C ((DirectSum.of (fun i => ↥(statSubmodule i)) i) x)add𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ ∀ (x y : DirectSum FieldStatistic fun i => ↥(statSubmodule i)), C x → C y → C (x + y)
  ·zero𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ C 0 simp [C]All goals completed! 🐙
  ·of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ ∀ (i : FieldStatistic) (x : ↥(statSubmodule i)), C ((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) intro i xof𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ C ((DirectSum.of (fun i => ↥(statSubmodule i)) i) x)
    simp only [DFinsupp.toFun_eq_coe, DirectSum.coeAddMonoidHom_of, C]of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ ↑x =
  ↑(((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) bosonic) +
    ↑(((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) fermionic)
    rw [DirectSum.of_apply,of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ ↑x = ↑(if h : i = bosonic then Eq.recOn h x else 0) + ↑(((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) fermionic)of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ ↑x = ↑(if h : i = bosonic then Eq.recOn h x else 0) + ↑(if h : i = fermionic then Eq.recOn h x else 0) DirectSum.of_applyof𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ ↑x = ↑(if h : i = bosonic then Eq.recOn h x else 0) + ↑(if h : i = fermionic then Eq.recOn h x else 0)of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ ↑x = ↑(if h : i = bosonic then Eq.recOn h x else 0) + ↑(if h : i = fermionic then Eq.recOn h x else 0)]of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ ↑x = ↑(if h : i = bosonic then Eq.recOn h x else 0) + ↑(if h : i = fermionic then Eq.recOn h x else 0)
    match i with
    | bosonic =>𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ ↑x = ↑(if h : bosonic = bosonic then Eq.recOn h x else 0) + ↑(if h : bosonic = fermionic then Eq.recOn h x else 0) simpAll goals completed! 🐙
    | fermionic =>𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ ↑x = ↑(if h : fermionic = bosonic then Eq.recOn h x else 0) + ↑(if h : fermionic = fermionic then Eq.recOn h x else 0) simpAll goals completed! 🐙
  ·add𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊢ ∀ (x y : DirectSum FieldStatistic fun i => ↥(statSubmodule i)), C x → C y → C (x + y) intro x y hx hyadd𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)x:DirectSum FieldStatistic fun i => ↥(statSubmodule i)y:DirectSum FieldStatistic fun i => ↥(statSubmodule i)hx:C xhy:C y⊢ C (x + y)
    simp_all only [C, DFinsupp.toFun_eq_coe, map_add, DirectSum.add_apply, Submodule.coe_add]add𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := fun a => (DirectSum.coeAddMonoidHom statSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)x:DirectSum FieldStatistic fun i => ↥(statSubmodule i)y:DirectSum FieldStatistic fun i => ↥(statSubmodule i)hx:(DirectSum.coeAddMonoidHom statSubmodule) x = ↑(x bosonic) + ↑(x fermionic)hy:(DirectSum.coeAddMonoidHom statSubmodule) y = ↑(y bosonic) + ↑(y fermionic)⊢ ↑(x bosonic) + ↑(x fermionic) + (↑(y bosonic) + ↑(y fermionic)) =
  ↑(x bosonic) + ↑(y bosonic) + (↑(x fermionic) + ↑(y fermionic))
    abelAll goals completed! 🐙



lemma directSum_eq_bosonic_plus_fermionic
    (a : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i))) :
    a = (DirectSum.of (fun i => ↥(statSubmodule (𝓕 := 𝓕) i)) bosonic) (a bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule (𝓕 := 𝓕) i)) fermionic) (a fermionic) := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ a =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)
  let C : DirectSum FieldStatistic (fun i => (statSubmodule (𝓕 := 𝓕) i)) → Prop :=
    fun a => a = (DirectSum.of (fun i => ↥(statSubmodule (𝓕 := 𝓕) i)) bosonic) (a bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule (𝓕 := 𝓕) i)) fermionic) (a fermionic)𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ a =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)
  change C a𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ C a
  apply DirectSum.induction_onzero𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ C 0of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ ∀ (i : FieldStatistic) (x : ↥(statSubmodule i)), C ((DirectSum.of (fun i => ↥(statSubmodule i)) i) x)add𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ ∀ (x y : DirectSum FieldStatistic fun i => ↥(statSubmodule i)), C x → C y → C (x + y)
  ·zero𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ C 0 simp [C]All goals completed! 🐙
  ·of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ ∀ (i : FieldStatistic) (x : ↥(statSubmodule i)), C ((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) intro i xof𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ C ((DirectSum.of (fun i => ↥(statSubmodule i)) i) x)
    simp only [C]of𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule i)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) i) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) i) x) fermionic)
    match i with
    | bosonic =>𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x) bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x) fermionic)
      simp only [DirectSum.of_eq_same]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x) fermionic)
      rw [DirectSum.of_eq_of_ne𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x + (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) 0h𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ fermionic ≠ bosonic𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x + (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) 0h𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ fermionic ≠ bosonic]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x + (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) 0h𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ fermionic ≠ bosonic
      simp only [map_zero]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x = (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) x + 0h𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ fermionic ≠ bosonic
      grindh𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule bosonic)⊢ fermionic ≠ bosonic
      grindAll goals completed! 🐙
    | fermionic =>𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x) bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x) fermionic)
      simp only [DirectSum.of_eq_same]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic)
      (((DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x) bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x
      rw [DirectSum.of_eq_of_ne𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) 0 + (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) xh𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ bosonic ≠ fermionic𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) 0 + (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) xh𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ bosonic ≠ fermionic]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) 0 + (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) xh𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ bosonic ≠ fermionic
      simp only [map_zero, zero_add]h𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:↥(statSubmodule fermionic)⊢ bosonic ≠ fermionic
      grindAll goals completed! 🐙
  ·add𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)⊢ ∀ (x y : DirectSum FieldStatistic fun i => ↥(statSubmodule i)), C x → C y → C (x + y) intro x y hx hyadd𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)x:DirectSum FieldStatistic fun i => ↥(statSubmodule i)y:DirectSum FieldStatistic fun i => ↥(statSubmodule i)hx:C xhy:C y⊢ C (x + y)
    simp only [DirectSum.add_apply, map_add, C] at hx hy ⊢add𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)x:DirectSum FieldStatistic fun i => ↥(statSubmodule i)y:DirectSum FieldStatistic fun i => ↥(statSubmodule i)hx:x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (x bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (x fermionic)hy:y =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (y bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (y fermionic)⊢ x + y =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (x bosonic) +
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (y bosonic) +
    ((DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (x fermionic) +
      (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (y fermionic))
    conv_lhs => rw [hx, hy]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)C:(DirectSum FieldStatistic fun i => ↥(statSubmodule i)) → Prop := 
  fun a =>
    a =
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)x:DirectSum FieldStatistic fun i => ↥(statSubmodule i)y:DirectSum FieldStatistic fun i => ↥(statSubmodule i)hx:x =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (x bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (x fermionic)hy:y =
  (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (y bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (y fermionic)| (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (x bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (x fermionic) +
  ((DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (y bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (y fermionic))
    abelAll goals completed! 🐙

For a field statistic 𝓕, the algebra 𝓕.WickAlgebra is graded by FieldStatistic. Those ofCrAnList φs for which φs has an overall bosonic statistic (i.e. 𝓕 |>ₛ φs = bosonic) span bosonic submodule, whilst those ofCrAnList φs for which φs has an overall fermionic statistic (i.e. 𝓕 |>ₛ φs = fermionic) span the fermionic submodule.


instance WickAlgebraGrade : GradedAlgebra (A := 𝓕.WickAlgebra) statSubmodule where
  one_mem := by𝓕:FieldSpecification⊢ 1 ∈ statSubmodule 0
    simp only [statSubmodule]𝓕:FieldSpecification⊢ 1 ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0}
    refine Submodule.mem_span.mpr fun p a => a ?_𝓕:FieldSpecificationp:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0} ⊆ ↑p⊢ 1 ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0}
    simp only [Set.mem_setOf_eq]𝓕:FieldSpecificationp:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0} ⊆ ↑p⊢ ∃ φs, 1 = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0
    use []h𝓕:FieldSpecificationp:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0} ⊆ ↑p⊢ 1 = ofCrAnList [] ∧ ofList 𝓕.crAnStatistics [] = 0
    simp only [ofCrAnList, ofCrAnListF_nil, map_one, ofList_empty, true_and]h𝓕:FieldSpecificationp:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = 0} ⊆ ↑p⊢ bosonic = 0
    rflAll goals completed! 🐙
  mul_mem f1 f2 a1 a2 h1 h2 := by𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2⊢ a1 * a2 ∈ statSubmodule (f1 + f2)
    let p (a2 : 𝓕.WickAlgebra) (hx : a2 ∈ statSubmodule f2) : Prop :=
      a1 * a2 ∈ statSubmodule (f1 + f2)𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ a1 * a2 ∈ statSubmodule (f1 + f2)
    change p a2 h2𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ p a2 h2
    apply Submodule.span_inductionmem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}), p x ⋯zero𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ p 0 ⋯add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ ∀ (x y : 𝓕.WickAlgebra) (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}),
  p x hx → p y hy → p (x + y) ⋯smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}), p x hx → p (a • x) ⋯
    ·mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}), p x ⋯ intro x hxmem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)x:𝓕.WickAlgebrahx:x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}⊢ p x ⋯
      simp only [Set.mem_setOf_eq] at hxmem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)x:𝓕.WickAlgebrahx:∃ φs, x = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2⊢ p x ⋯
      obtain ⟨φs, rfl, h⟩ := hxmem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2⊢ p (ofCrAnList φs) ⋯
      simp only [p]mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2⊢ a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)
      let p (a1 : 𝓕.WickAlgebra) (hx : a1 ∈ statSubmodule f1) : Prop :=
        a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)
      change p a1 h1mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ p a1 h1
      apply Submodule.span_induction (p := p)mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}), p x ⋯mem.zero𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ p 0 ⋯mem.add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ ∀ (x y : 𝓕.WickAlgebra) (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}),
  p x hx → p y hy → p (x + y) ⋯mem.smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}), p x hx → p (a • x) ⋯mem.hx𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ a1 ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}
      ·mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ ∀ (x : 𝓕.WickAlgebra) (h : x ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}), p x ⋯ intro y hymem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)y:𝓕.WickAlgebrahy:y ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}⊢ p y ⋯
        obtain ⟨φs', rfl, h'⟩ := hymem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1⊢ p (ofCrAnList φs') ⋯
        simp only [p]mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1⊢ ofCrAnList φs' * ofCrAnList φs ∈ statSubmodule (f1 + f2)
        rw [← ofCrAnList_appendmem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1⊢ ofCrAnList (φs' ++ φs) ∈ statSubmodule (f1 + f2)mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1⊢ ofCrAnList (φs' ++ φs) ∈ statSubmodule (f1 + f2)]mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1⊢ ofCrAnList (φs' ++ φs) ∈ statSubmodule (f1 + f2)
        refine Submodule.mem_span.mpr fun p a => a ?_mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝¹:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1p:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1 + f2} ⊆ ↑p⊢ ofCrAnList (φs' ++ φs) ∈ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1 + f2}
        simp only [Set.mem_setOf_eq]mem.mem𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝¹:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1p:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1 + f2} ⊆ ↑p⊢ ∃ φs_1, ofCrAnList (φs' ++ φs) = ofCrAnList φs_1 ∧ ofList 𝓕.crAnStatistics φs_1 = f1 + f2
        use φs' ++ φsh𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝¹:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1p:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1 + f2} ⊆ ↑p⊢ ofCrAnList (φs' ++ φs) = ofCrAnList (φs' ++ φs) ∧ ofList 𝓕.crAnStatistics (φs' ++ φs) = f1 + f2
        simp only [ofList_append, h', h, true_and]h𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝¹:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)φs':List 𝓕.CrAnFieldOph':ofList 𝓕.crAnStatistics φs' = f1p:Submodule ℂ 𝓕.WickAlgebraa:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1 + f2} ⊆ ↑p⊢ (if f1 = f2 then bosonic else fermionic) = f1 + f2
        cases f1h.bosonic𝓕:FieldSpecificationf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah2:a2 ∈ statSubmodule f2φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2φs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule bosonicp✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (bosonic + f2)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (bosonic + f2)h':ofList 𝓕.crAnStatistics φs' = bosonica:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic + f2} ⊆ ↑p✝¹⊢ (if bosonic = f2 then bosonic else fermionic) = bosonic + f2h.fermionic𝓕:FieldSpecificationf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah2:a2 ∈ statSubmodule f2φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2φs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule fermionicp✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (fermionic + f2)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (fermionic + f2)h':ofList 𝓕.crAnStatistics φs' = fermionica:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic + f2} ⊆ ↑p✝¹⊢ (if fermionic = f2 then bosonic else fermionic) = fermionic + f2 <;>h.bosonic𝓕:FieldSpecificationf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah2:a2 ∈ statSubmodule f2φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2φs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule bosonicp✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (bosonic + f2)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (bosonic + f2)h':ofList 𝓕.crAnStatistics φs' = bosonica:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic + f2} ⊆ ↑p✝¹⊢ (if bosonic = f2 then bosonic else fermionic) = bosonic + f2h.fermionic𝓕:FieldSpecificationf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah2:a2 ∈ statSubmodule f2φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2φs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule fermionicp✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (fermionic + f2)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (fermionic + f2)h':ofList 𝓕.crAnStatistics φs' = fermionica:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic + f2} ⊆ ↑p✝¹⊢ (if fermionic = f2 then bosonic else fermionic) = fermionic + f2 cases f2h.fermionic.bosonic𝓕:FieldSpecificationa1:𝓕.WickAlgebraa2:𝓕.WickAlgebraφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule fermionich':ofList 𝓕.crAnStatistics φs' = fermionich2:a2 ∈ statSubmodule bosonich:ofList 𝓕.crAnStatistics φs = bosonicp✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (fermionic + bosonic)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (fermionic + bosonic)a:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic + bosonic} ⊆ ↑p✝¹⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic + bosonich.fermionic.fermionic𝓕:FieldSpecificationa1:𝓕.WickAlgebraa2:𝓕.WickAlgebraφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule fermionich':ofList 𝓕.crAnStatistics φs' = fermionich2:a2 ∈ statSubmodule fermionich:ofList 𝓕.crAnStatistics φs = fermionicp✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (fermionic + fermionic)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (fermionic + fermionic)a:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic + fermionic} ⊆ ↑p✝¹⊢ (if fermionic = fermionic then bosonic else fermionic) = fermionic + fermionic <;>h.bosonic.bosonic𝓕:FieldSpecificationa1:𝓕.WickAlgebraa2:𝓕.WickAlgebraφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule bosonich':ofList 𝓕.crAnStatistics φs' = bosonich2:a2 ∈ statSubmodule bosonich:ofList 𝓕.crAnStatistics φs = bosonicp✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (bosonic + bosonic)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (bosonic + bosonic)a:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic + bosonic} ⊆ ↑p✝¹⊢ (if bosonic = bosonic then bosonic else fermionic) = bosonic + bosonich.bosonic.fermionic𝓕:FieldSpecificationa1:𝓕.WickAlgebraa2:𝓕.WickAlgebraφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule bosonich':ofList 𝓕.crAnStatistics φs' = bosonich2:a2 ∈ statSubmodule fermionich:ofList 𝓕.crAnStatistics φs = fermionicp✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (bosonic + fermionic)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (bosonic + fermionic)a:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = bosonic + fermionic} ⊆ ↑p✝¹⊢ (if bosonic = fermionic then bosonic else fermionic) = bosonic + fermionich.fermionic.bosonic𝓕:FieldSpecificationa1:𝓕.WickAlgebraa2:𝓕.WickAlgebraφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule fermionich':ofList 𝓕.crAnStatistics φs' = fermionich2:a2 ∈ statSubmodule bosonich:ofList 𝓕.crAnStatistics φs = bosonicp✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule bosonic → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (fermionic + bosonic)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (fermionic + bosonic)a:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic + bosonic} ⊆ ↑p✝¹⊢ (if fermionic = bosonic then bosonic else fermionic) = fermionic + bosonich.fermionic.fermionic𝓕:FieldSpecificationa1:𝓕.WickAlgebraa2:𝓕.WickAlgebraφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpp✝¹:Submodule ℂ 𝓕.WickAlgebrah1:a1 ∈ statSubmodule fermionich':ofList 𝓕.crAnStatistics φs' = fermionich2:a2 ∈ statSubmodule fermionich:ofList 𝓕.crAnStatistics φs = fermionicp✝:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (fermionic + fermionic)p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule fermionic → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (fermionic + fermionic)a:{a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = fermionic + fermionic} ⊆ ↑p✝¹⊢ (if fermionic = fermionic then bosonic else fermionic) = fermionic + fermionic rflAll goals completed! 🐙
      ·mem.zero𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ p 0 ⋯ simp [p]All goals completed! 🐙
      ·mem.add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ ∀ (x y : 𝓕.WickAlgebra) (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}),
  p x hx → p y hy → p (x + y) ⋯ intro x y hx hy hx1 hx2mem.add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)x:𝓕.WickAlgebray:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}hx1:p x hxhx2:p y hy⊢ p (x + y) ⋯
        simp only [add_mul, p]mem.add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)x:𝓕.WickAlgebray:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}hx1:p x hxhx2:p y hy⊢ x * ofCrAnList φs + y * ofCrAnList φs ∈ statSubmodule (f1 + f2)
        exact Submodule.add_mem _ hx1 hx2All goals completed! 🐙
      ·mem.smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}), p x hx → p (a • x) ⋯ intro c a hx h1mem.smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1✝:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)c:ℂa:𝓕.WickAlgebrahx:a ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}h1:p a hx⊢ p (c • a) ⋯
        simp only [Algebra.smul_mul_assoc, p]mem.smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1✝:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)c:ℂa:𝓕.WickAlgebrahx:a ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1}h1:p a hx⊢ c • (a * ofCrAnList φs) ∈ statSubmodule (f1 + f2)
        exact Submodule.smul_mem _ _ h1All goals completed! 🐙
      ·mem.hx𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p✝:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics φs = f2p:(a1 : 𝓕.WickAlgebra) → a1 ∈ statSubmodule f1 → Prop := fun a1 hx => a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)⊢ a1 ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f1} exact h1All goals completed! 🐙
    ·zero𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ p 0 ⋯ simp [p]All goals completed! 🐙
    ·add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ ∀ (x y : 𝓕.WickAlgebra) (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2})
  (hy : y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}),
  p x hx → p y hy → p (x + y) ⋯ intro x y hx hy hx1 hx2add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)x:𝓕.WickAlgebray:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}hx1:p x hxhx2:p y hy⊢ p (x + y) ⋯
      simp only [mul_add, p]add𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)x:𝓕.WickAlgebray:𝓕.WickAlgebrahx:x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}hy:y ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}hx1:p x hxhx2:p y hy⊢ a1 * x + a1 * y ∈ statSubmodule (f1 + f2)
      exact Submodule.add_mem _ hx1 hx2All goals completed! 🐙
    ·smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)⊢ ∀ (a : ℂ) (x : 𝓕.WickAlgebra)
  (hx : x ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}), p x hx → p (a • x) ⋯ intro c a hx h1smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1✝:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)c:ℂa:𝓕.WickAlgebrahx:a ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}h1:p a hx⊢ p (c • a) ⋯
      simp only [Algebra.mul_smul_comm, p]smul𝓕:FieldSpecificationf1:FieldStatisticf2:FieldStatistica1:𝓕.WickAlgebraa2:𝓕.WickAlgebrah1✝:a1 ∈ statSubmodule f1h2:a2 ∈ statSubmodule f2p:(a2 : 𝓕.WickAlgebra) → a2 ∈ statSubmodule f2 → Prop := fun a2 hx => a1 * a2 ∈ statSubmodule (f1 + f2)c:ℂa:𝓕.WickAlgebrahx:a ∈ Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ ofList 𝓕.crAnStatistics φs = f2}h1:p a hx⊢ c • (a1 * a) ∈ statSubmodule (f1 + f2)
      exact Submodule.smul_mem _ _ h1All goals completed! 🐙
  decompose' a := DirectSum.of (fun i => (statSubmodule (𝓕 := 𝓕) i)) bosonic (bosonicProj a)
    + DirectSum.of (fun i => (statSubmodule (𝓕 := 𝓕) i)) fermionic (fermionicProj a)
  left_inv a := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ (DirectSum.coeAddMonoidHom statSubmodule)
    ((fun a =>
        (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
          (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
      a) =
  a
    trans a.bosonicProj + a.fermionicProj𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ (DirectSum.coeAddMonoidHom statSubmodule)
    ((fun a =>
        (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
          (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
      a) =
  ↑(bosonicProj a) + ↑(fermionicProj a)𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ ↑(bosonicProj a) + ↑(fermionicProj a) = a
    ·𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ (DirectSum.coeAddMonoidHom statSubmodule)
    ((fun a =>
        (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
          (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
      a) =
  ↑(bosonicProj a) + ↑(fermionicProj a) simpAll goals completed! 🐙
    ·𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ ↑(bosonicProj a) + ↑(fermionicProj a) = a exact bosonicProj_add_fermionicProj aAll goals completed! 🐙
  right_inv a := by𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ (fun a =>
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
    ((DirectSum.coeAddMonoidHom statSubmodule) a) =
  a
    rw [coeAddMonoidHom_apply_eq_bosonic_plus_fermionic𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ (fun a =>
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
    (↑(a.toFun bosonic) + ↑(a.toFun fermionic)) =
  a𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ (fun a =>
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
    (↑(a.toFun bosonic) + ↑(a.toFun fermionic)) =
  a]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ (fun a =>
      (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (bosonicProj a) +
        (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (fermionicProj a))
    (↑(a.toFun bosonic) + ↑(a.toFun fermionic)) =
  a
    simp only [DFinsupp.toFun_eq_coe, map_add, bosonicProj_of_bosonic_part,
      bosonicProj_of_fermionic_part, add_zero, fermionicProj_of_bosonic_part,
      fermionicProj_of_fermionic_part, zero_add]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)⊢ (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
    (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic) =
  a
    conv_rhs => rw [directSum_eq_bosonic_plus_fermionic a]𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => ↥(statSubmodule i)| (DirectSum.of (fun i => ↥(statSubmodule i)) bosonic) (a bosonic) +
  (DirectSum.of (fun i => ↥(statSubmodule i)) fermionic) (a fermionic)