Mul wick Term eq sum

lemma mul_wickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ)    (φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])    (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :    ofFieldOp φ * φsΛ.wickTerm =    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •    ∑ (k : Option φsΛ.uncontracted), (φsΛ ↩Λ φ i k).wickTerm := by  trans (φsΛ.sign • φsΛ.timeContract) * ((ofFieldOp φ) * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ))  · have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)      (WickContraction.timeContract φsΛ).2 (φsΛ.sign))    rw [wickTerm]    rw [← mul_assoc, ht, mul_assoc]  rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, Finset.mul_sum,    uncontractedFieldOpEquiv_list_sum, Finset.smul_sum]  simp only [Nat.succ_eq_add_one]  congr 1  funext n  match n with  | none =>    rw [wickTerm_insert_none]    simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,      Equiv.coe_trans, Option.map_none, one_mul, Algebra.smul_mul_assoc, smul_smul]    congr 1    rw [← mul_assoc, exchangeSign_mul_self]    simp  | some n =>    rw [wickTerm_insert_some _ _ _ _ _      (fun k => hlt k) (fun k a => hn k a)]    simp only [uncontractedFieldOpEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some,      Function.comp_apply, finCongr_apply, Algebra.smul_mul_assoc, smul_smul]    congr 1    · rw [← mul_assoc, exchangeSign_mul_self]      rw [one_mul]    · rw [← mul_assoc]      congr 1      have ht := (WickContraction.timeContract φsΛ).prop      rw [@Subalgebra.mem_center_iff] at ht      rw [ht]