Time Contract insert some of lt

lemma timeContract_insert_some_of_lt    (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)    (ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :    (φsΛ ↩Λ φ i (some k)).timeContract =    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)    • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *      φsΛ.timeContract) := by  rw [timeContract_insertAndContract_some]  simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul,    contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,    Equiv.coe_trans, Option.map_some, Function.comp_apply, finCongr_apply, Fin.val_cast,    List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,    Algebra.smul_mul_assoc, uncontractedListGet]  · simp only [hik, ↓reduceIte, MulMemClass.coe_mul]    rw [timeContract_of_timeOrderRel]    trans (1 : ℂ) • ((superCommute (anPart φ)) (ofFieldOp φs[k.1]) * ↑φsΛ.timeContract)    · simp    simp only [smul_smul]    congr 1    have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))        (List.map φs.get φsΛ.uncontractedList))        = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by      simp only [ofFinset]      congr      rw [← List.map_take]      congr      rw [take_uncontractedIndexEquiv_symm]      rw [filter_uncontractedList]    rw [h1]    simp only [exchangeSign_mul_self]    · exact ht