Mul static Wick Term eq sum

lemma mul_staticWickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (φsΛ : WickContraction φs.length) :    ofFieldOp φ * φsΛ.staticWickTerm =    ∑ (k : Option φsΛ.uncontracted), (φsΛ ↩Λ φ 0 k).staticWickTerm := by  trans (φsΛ.sign • φsΛ.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [φsΛ]ᵘᶜ)))  · have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)      (φsΛ.staticContract).2 φsΛ.sign)    conv_rhs => rw [← mul_assoc, ← ht]    simp [mul_assoc, staticWickTerm]  rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, Finset.mul_sum,    uncontractedFieldOpEquiv_list_sum]  refine Finset.sum_congr rfl (fun n _ => ?_)  match n with  | none =>    simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,      Equiv.coe_trans, Option.map_none, one_mul, Algebra.smul_mul_assoc, Nat.succ_eq_add_one,      Fin.val_zero, List.insertIdx_zero]    rw [staticWickTerm_insert_zero_none]    simp only [Algebra.smul_mul_assoc]    rfl  | some n =>    simp only [Algebra.smul_mul_assoc, Nat.succ_eq_add_one, Fin.val_zero,      List.insertIdx_zero]    rw [staticWickTerm_insert_zero_some]