Time Contract insert some of not lt

lemma timeContract_insert_some_of_not_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_not_timeOrderRel, timeContract_of_timeOrderRel]  simp only [Algebra.smul_mul_assoc, smul_smul]  congr  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, filter_uncontractedList]  rw [h1]  trans 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, {k.1}⟩)  · rw [exchangeSign_symm, ofFinset_singleton]    simp  rw [← map_mul]  congr  rw [ofFinset_union]  congr  ext a  simp only [Finset.mem_singleton, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter,    Finset.mem_inter, not_and, not_lt, and_imp]  apply Iff.intro  · intro h    subst h    simp  · intro h    have h1 := h.1    rcases h1 with h1 | h1    · have h2' := h.2 h1.1 h1.2 h1.1      omega    · have h2' := h.2 h1.1 (by omega) h1.1      omega  have ht := Std.Total.total (r := timeOrderRel) φs[k.1] φ  simp_all only [Fin.getElem_fin, Nat.succ_eq_add_one, not_lt, false_or]  exact ht