Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.Koszul.KoszulSignInsert public import Physlib.Mathematics.List.InsertionSort import all Physlib.Mathematics.List

Koszul sign

@[expose] public section

Gives a factor of - 1 for every fermion-fermion (q is 1) crossing that occurs when sorting a list of based on r.

def koszulSign (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] : List 𝓕 → ℂ | [] => 1 | a :: l => koszulSignInsert q le a l * koszulSign q le l
@[simp] lemma koszulSign_singleton (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) : koszulSign q le [φ] = 1 := 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leφ:𝓕⊢ koszulSign q le [φ] = 1 All goals completed! 🐙All goals completed! 🐙@[simp] lemma koszulSign_freeMonoid_of (φ : 𝓕) : koszulSign q le (FreeMonoid.of φ) = 1 := 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leφ:𝓕⊢ koszulSign q le (FreeMonoid.of φ) = 1 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leφ:𝓕⊢ koszulSign q le [φ] = 1 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leφ:𝓕⊢ koszulSignInsert q le φ [] = 1 All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs:List 𝓕n:ℕh:n + 1 ≤ (φ1 :: φs).lengthrs:List 𝓕 := List.insertionSort le (φs.insertIdx n φ)hnsL:n < (φs.insertIdx n φ).lengthni:Fin rs.length := (insertionSortEquiv le (φs.insertIdx n φ)) ⟨n, hnsL⟩nro:Fin (rs.length + 1) := ⟨↑(orderedInsertPos le rs φ1), ⋯⟩hns:rs.get ni = φhc1:ni.castSucc < nro → ¬le φ1 φhc2:¬ni.castSucc < nro → le φ1 φhn:¬ni.castSucc < nro⊢ (if le φ1 φ then 1 else if q φ1 = fermionic ∧ q φ = fermionic then -1 else 1) = 1 All goals completed! 🐙 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs:List 𝓕n:ℕh:n + 1 ≤ (φ1 :: φs).lengthrs:List 𝓕 := List.insertionSort le (φs.insertIdx n φ)hnsL:n < (φs.insertIdx n φ).lengthni:Fin rs.length := (insertionSortEquiv le (φs.insertIdx n φ)) ⟨n, hnsL⟩nro:Fin (rs.length + 1) := ⟨↑(orderedInsertPos le rs φ1), ⋯⟩hns:rs.get ni = φhc1:ni.castSucc < nro → ¬le φ1 φhc2:¬ni.castSucc < nro → le φ1 φhn:¬ni.castSucc < nro⊢ ↑nro ≤ ↑ni All goals completed! 🐙 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs:List 𝓕n:ℕh:n + 1 ≤ (φ1 :: φs).lengthrs:List 𝓕 := List.insertionSort le (φs.insertIdx n φ)hnsL:n < (φs.insertIdx n φ).lengthni:Fin rs.length := (insertionSortEquiv le (φs.insertIdx n φ)) ⟨n, hnsL⟩nro:Fin (rs.length + 1) := ⟨↑(orderedInsertPos le rs φ1), ⋯⟩hns:rs.get ni = φhc1:ni.castSucc < nro → ¬le φ1 φhc2:¬ni.castSucc < nro → le φ1 φhn:¬ni.castSucc < nro⊢ ↑nro ≤ rs.length All goals completed! 🐙lemma insertIdx_eraseIdx {I : Type} : (n : ℕ) → (r : List I) → (hn : n < r.length) → List.insertIdx (r.eraseIdx n) n (r.get ⟨n, hn⟩) = r I:Typen:ℕhn:n < [].length⊢ ([].eraseIdx n).insertIdx n ([].get ⟨n, hn⟩) = [] I:Typen:ℕhn:n < [].length⊢ ([].eraseIdx n).insertIdx n ([].get ⟨n, hn⟩) = [] All goals completed! 🐙 I:Typer0:Ir:List Ihn:0 < (r0 :: r).length⊢ ((r0 :: r).eraseIdx 0).insertIdx 0 ((r0 :: r).get ⟨0, hn⟩) = r0 :: r I:Typer0:Ir:List Ihn:0 < (r0 :: r).length⊢ ((r0 :: r).eraseIdx 0).insertIdx 0 ((r0 :: r).get ⟨0, hn⟩) = r0 :: r All goals completed! 🐙 I:Typen:ℕr0:Ir:List Ihn:n + 1 < (r0 :: r).length⊢ ((r0 :: r).eraseIdx (n + 1)).insertIdx (n + 1) ((r0 :: r).get ⟨n + 1, hn⟩) = r0 :: r I:Typen:ℕr0:Ir:List Ihn:n + 1 < (r0 :: r).length⊢ ((r0 :: r).eraseIdx (n + 1)).insertIdx (n + 1) ((r0 :: r).get ⟨n + 1, hn⟩) = r0 :: r I:Typen:ℕr0:Ir:List Ihn:n + 1 < (r0 :: r).length⊢ (r.eraseIdx n).insertIdx n r[n] = r All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs⊢ koszulSign q le (φs.eraseIdx ↑n) * ((exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) (φs.eraseIdx ↑n))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) φs))) * ((exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs)))) = (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) (φs.eraseIdx ↑n))) * koszulSign q le (φs.eraseIdx ↑n) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑((Fin.castOrderIso ⋯).toEquiv ((insertionSortEquiv le φs) ((Fin.castOrderIso ⋯).toEquiv ⟨↑n, ⋯⟩)))) (List.insertionSort le φs))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) φs)) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs⊢ koszulSign q le (φs.eraseIdx ↑n) * ((exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) (φs.eraseIdx ↑n))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) φs))) * ((exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs)))) = (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) (φs.eraseIdx ↑n))) * koszulSign q le (φs.eraseIdx ↑n) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) φs)) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) All goals completed! 🐙 conv_rhs => 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| 1 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs⊢ koszulSign q le (φs.eraseIdx ↑n) = koszulSign q le (φs.eraseIdx ↑n) * ((exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) (φs.eraseIdx ↑n))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) φs))) conv_rhs => 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) (φs.eraseIdx ↑n))) * (exchangeSign (q φs[↑n])) (ofList q (List.take (↑n) φs)) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx ↑nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| 1 All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕⊢ koszulSign q le (φ :: φs) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑((insertionSortEquiv le (φ :: φs)) (insertionSortMinPos le φ φs))) (List.insertionSort le (φ :: φs)))) = koszulSign q le (φ :: φs) * (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) conv_lhs => 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑((insertionSortEquiv le (φ :: φs)) (insertionSortMinPos le φ φs))) (List.insertionSort le (φ :: φs)))) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| ofList q (List.take (↑((insertionSortEquiv le (φ :: φs)) (insertionSortMinPos le φ φs))) (List.insertionSort le (φ :: φs))) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| q 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| q erw [𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕⊢ koszulSign q le (φ :: φs) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑⟨0, ⋯⟩) (List.insertionSort le (φ :: φs)))) = koszulSign q le (φ :: φs) * (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs)))𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕⊢ koszulSign q le (φ :: φs) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑⟨0, ⋯⟩) (List.insertionSort le (φ :: φs)))) = koszulSign q le (φ :: φs) * (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕⊢ (exchangeSign (q (φ :: φs)[↑(insertionSortMinPos le φ φs)])) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) = (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) ∨ koszulSign q le (φ :: φs) = 0 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕⊢ (exchangeSign (q (φ :: φs)[↑(insertionSortMinPos le φ φs)])) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) = (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφs':List 𝓕⊢ koszulSignInsert q le ψ φs' * koszulSignInsert q le φ (ψ :: φs') = koszulSignInsert q le ψ (φ :: φs') * koszulSignInsert q le φ φs' All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφ'':𝓕φs:List 𝓕φs':List 𝓕⊢ koszulSignInsert q le φ'' (φs ++ φ :: ψ :: φs') * koszulSign q le (φs ++ ψ :: φ :: φs') = koszulSignInsert q le φ'' (φs ++ ψ :: φ :: φs') * koszulSign q le (φs ++ ψ :: φ :: φs') 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφ'':𝓕φs:List 𝓕φs':List 𝓕⊢ koszulSignInsert q le φ'' (φs ++ φ :: ψ :: φs') = koszulSignInsert q le φ'' (φs ++ ψ :: φ :: φs') 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφ'':𝓕φs:List 𝓕φs':List 𝓕⊢ (φs ++ φ :: ψ :: φs').Perm (φs ++ ψ :: φ :: φs') All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leψ:𝓕φ:𝓕inst✝:IsTrans 𝓕 leh1:le φ ψh2:le ψ φhq:q ψ = q φφs:List 𝓕⊢ koszulSignInsert q le ψ φs * koszulSignInsert q le ψ φs = 1 All goals completed! 🐙All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leφ:𝓕φs:List 𝓕h:(∀ a' ∈ φs, le φ a') ∧ List.Pairwise le φs⊢ koszulSignInsert q le φ φs * 1 = 1 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝:DecidableRel leφ:𝓕φs:List 𝓕h:(∀ a' ∈ φs, le φ a') ∧ List.Pairwise le φs⊢ koszulSignInsert q le φ φs = 1 All goals completed! 🐙@[simp] lemma koszulSign_of_insertionSort [Std.Total le] [IsTrans 𝓕 le] (φs : List 𝓕) : koszulSign q le (List.insertionSort le φs) = 1 := 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕⊢ koszulSign q le (List.insertionSort le φs) = 1 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕⊢ List.Pairwise le (List.insertionSort le φs) All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕φ:𝓕φs':List 𝓕h1:φs ++ φ :: φs' = (φs ++ φs').insertIdx φs.length φh2:List.insertionSort le φs ++ φ :: φs' = (List.insertionSort le φs ++ φs').insertIdx (List.insertionSort le φs).length φ⊢ List.insertionSort le (φs ++ φ :: φs') = List.insertionSort le (List.insertionSort le φs ++ φ :: φs') 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕φ:𝓕φs':List 𝓕h1:φs ++ φ :: φs' = (φs ++ φs').insertIdx φs.length φh2:List.insertionSort le φs ++ φ :: φs' = (List.insertionSort le φs ++ φs').insertIdx (List.insertionSort le φs).length φ⊢ List.insertionSort le (List.insertionSort le φs ++ φ :: φs') = List.insertionSort le (φs ++ φ :: φs') All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕⊢ koszulSignInsert q le φ'' (φs'' ++ φs ++ φs') * koszulSign q le (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le φs = koszulSignInsert q le φ'' (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le φs 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕⊢ koszulSignInsert q le φ'' (φs'' ++ φs ++ φs') = koszulSignInsert q le φ'' (φs'' ++ List.insertionSort le φs ++ φs') 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕⊢ (φs'' ++ φs ++ φs').Perm (φs'' ++ List.insertionSort le φs ++ φs') 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕⊢ (φs'' ++ φs).Perm (φs'' ++ List.insertionSort le φs) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕⊢ φs.Perm (List.insertionSort le φs) All goals completed! 🐙

koszulSign with permutations

lemma koszulSign_perm_eq_append [IsTrans 𝓕 le] (φ : 𝓕) (φs φs' φs2 : List 𝓕) (hp : φs.Perm φs') : (h : ∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) := 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'⊢ (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ motive φs φs' hp 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ motive [] [] ⋯𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ ∀ (x : 𝓕) {l₁ l₂ : List 𝓕} (a : l₁.Perm l₂), motive l₁ l₂ a → motive (x :: l₁) (x :: l₂) ⋯𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ ∀ (x y : 𝓕) (l : List 𝓕), motive (y :: x :: l) (x :: y :: l) ⋯𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ ∀ {l₁ l₂ l₃ : List 𝓕} (a : l₁.Perm l₂) (a_1 : l₂.Perm l₃), motive l₁ l₂ a → motive l₂ l₃ a_1 → motive l₁ l₃ ⋯ 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ motive [] [] ⋯ All goals completed! 🐙 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ ∀ (x : 𝓕) {l₁ l₂ : List 𝓕} (a : l₁.Perm l₂), motive l₁ l₂ a → motive (x :: l₁) (x :: l₂) ⋯ 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:motive l1 l2 hhxφ:∀ φ' ∈ x :: l1, le φ φ' ∧ le φ' φ⊢ koszulSign q le (x :: l1 ++ φs2) = koszulSign q le (x :: l2 ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x ∧ le x φ) ∧ ∀ a ∈ l1, le φ a ∧ le a φ⊢ koszulSign q le (x :: (l1 ++ φs2)) = koszulSign q le (x :: (l2 ++ φs2)) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x ∧ le x φ) ∧ ∀ a ∈ l1, le φ a ∧ le a φ⊢ koszulSignInsert q le x (l1 ++ φs2) = koszulSignInsert q le x (l2 ++ φs2) ∨ koszulSign q le (l2 ++ φs2) = 0 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x ∧ le x φ) ∧ ∀ a ∈ l1, le φ a ∧ le a φ⊢ koszulSignInsert q le x (l1 ++ φs2) = koszulSignInsert q le x (l2 ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x ∧ le x φ) ∧ ∀ a ∈ l1, le φ a ∧ le a φ⊢ (l1 ++ φs2).Perm (l2 ++ φs2) All goals completed! 🐙 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ ∀ (x y : 𝓕) (l : List 𝓕), motive (y :: x :: l) (x :: y :: l) ⋯ 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:∀ φ' ∈ y :: x :: l, le φ φ' ∧ le φ' φ⊢ koszulSign q le (y :: x :: l ++ φs2) = koszulSign q le (x :: y :: l ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y ∧ le y φ) ∧ (le φ x ∧ le x φ) ∧ ∀ a ∈ l, le φ a ∧ le a φ⊢ koszulSign q le (y :: x :: (l ++ φs2)) = koszulSign q le (x :: y :: (l ++ φs2)) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y ∧ le y φ) ∧ (le φ x ∧ le x φ) ∧ ∀ a ∈ l, le φ a ∧ le a φ⊢ le y x𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y ∧ le y φ) ∧ (le φ x ∧ le x φ) ∧ ∀ a ∈ l, le φ a ∧ le a φ⊢ le x y 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y ∧ le y φ) ∧ (le φ x ∧ le x φ) ∧ ∀ a ∈ l, le φ a ∧ le a φ⊢ le y x All goals completed! 🐙 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y ∧ le y φ) ∧ (le φ x ∧ le x φ) ∧ ∀ a ∈ l, le φ a ∧ le a φ⊢ le x y All goals completed! 🐙 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)⊢ ∀ {l₁ l₂ l₃ : List 𝓕} (a : l₁.Perm l₂) (a_1 : l₂.Perm l₃), motive l₁ l₂ a → motive l₂ l₃ a_1 → motive l₁ l₃ ⋯ 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:motive l1 l2 h1ih2:motive l2 l3 h2h:∀ φ' ∈ l1, le φ φ' ∧ le φ' φ⊢ koszulSign q le (l1 ++ φs2) = koszulSign q le (l3 ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' ∈ l2, le φ φ' ∧ le φ' φ) → koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h:∀ φ' ∈ l1, le φ φ' ∧ le φ' φ⊢ koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' ∈ l2, le φ φ' ∧ le φ' φ) → koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h:∀ φ' ∈ l1, le φ φ' ∧ le φ' φ⊢ ∀ φ' ∈ l2, le φ φ' ∧ le φ' φ 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' ∈ l2, le φ φ' ∧ le φ' φ) → koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h:∀ φ' ∈ l1, le φ φ' ∧ le φ' φφ':𝓕hφ:φ' ∈ l2⊢ le φ φ' ∧ le φ' φ 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) → φs.Perm φs' → Prop := fun φs φs' hp => (∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) → koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' ∈ l2, le φ φ' ∧ le φ' φ) → koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h:∀ φ' ∈ l1, le φ φ' ∧ le φ' φφ':𝓕hφ:φ' ∈ l2⊢ φ' ∈ l1 All goals completed! 🐙𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h:∀ φ' ∈ φs, le φ φ' ∧ le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)⊢ koszulSignInsert q le φ1 (φs1 ++ φs ++ φs2) * koszulSign q le (φs1 ++ φs' ++ φs2) = koszulSignInsert q le φ1 (φs1 ++ φs' ++ φs2) * koszulSign q le (φs1 ++ φs' ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h:∀ φ' ∈ φs, le φ φ' ∧ le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)⊢ koszulSignInsert q le φ1 (φs1 ++ φs ++ φs2) = koszulSignInsert q le φ1 (φs1 ++ φs' ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h:∀ φ' ∈ φs, le φ φ' ∧ le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)⊢ (φs1 ++ φs ++ φs2).Perm (φs1 ++ φs' ++ φs2) 𝓕:Typeq:𝓕 → FieldStatisticle:𝓕 → 𝓕 → Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h:∀ φ' ∈ φs, le φ φ' ∧ le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)⊢ (φs1 ++ φs).Perm (φs1 ++ φs') All goals completed! 🐙