Time Order have Eq Time split

lemma timeOrder_haveEqTime_split (φs : List 𝓕.FieldOp) :    𝓣(ofFieldOpList φs) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),    φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))    + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), φsΛ.1.sign • φsΛ.1.timeContract *    (∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },      φssucΛ.1.wickTerm) := by  rw [wicks_theorem]  simp only [wickTerm]  let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} :=    (Equiv.sumCompl HaveEqTime).symm  rw [← e1.symm.sum_comp]  simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type,    Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, ne_eq, e1]  rw [add_comm]  congr 1  let f : WickContraction φs.length → 𝓕.WickAlgebra := fun φsΛ =>    φsΛ.sign • (φsΛ.timeContract.1 * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ))  change ∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ.1 = _  rw [sum_haveEqTime]  congr  funext φsΛ  simp only [f]  conv_lhs =>    enter [2, φsucΛ]    rw [← Algebra.smul_mul_assoc, join_sign_timeContract φsΛ.1 φsucΛ.1, mul_assoc]  rw [← Finset.mul_sum, ← Algebra.smul_mul_assoc]  congr  funext φsΛ'  simp only [ne_eq, Algebra.smul_mul_assoc]  congr 1  rw [@join_uncontractedListGet]