Wick Term insert some

lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)    (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])    (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) :    (φsΛ ↩Λ φ i (some k)).wickTerm =    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩)    • (φsΛ.sign • (contractStateAtIndex φ [φsΛ]ᵘᶜ      ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * φsΛ.timeContract)    * 𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedFieldOpEquiv φs φsΛ k)))) := by  rw [wickTerm]  by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])  · by_cases hk : i.succAbove k < i    · rw [WickContraction.timeContract_insert_some_of_not_lt]      swap      · exact hn _ hk      · rw [normalOrder_uncontracted_some, sign_insert_some_of_lt φ φs φsΛ i k hk hg]        simp only [smul_smul, Algebra.smul_mul_assoc]        congr 1        rw [mul_assoc, mul_assoc, mul_comm, mul_assoc, mul_assoc]        simp      · omega    · have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k      rw [timeContract_insert_some_of_lt]      swap      · exact hlt _      · rw [normalOrder_uncontracted_some]        rw [sign_insert_some_of_not_lt φ φs φsΛ i k hk hg]        simp only [smul_smul, Algebra.smul_mul_assoc]        congr 1        rw [mul_assoc, mul_assoc, mul_comm, mul_assoc, mul_assoc]        simp      · omega  · rw [timeContract_insertAndContract_some]    simp only [Fin.getElem_fin, not_and] at hg    by_cases hg' : GradingCompliant φs φsΛ    · have hg := hg hg'      simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, Algebra.smul_mul_assoc,        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,        uncontractedListGet]      by_cases h1 : i < i.succAbove ↑k      · simp only [h1, ↓reduceIte, MulMemClass.coe_mul]        rw [timeContract_zero_of_diff_grade]        simp only [zero_mul, smul_zero]        rw [superCommute_anPart_ofFieldOpF_diff_grade_zero]        simp only [zero_mul, smul_zero]        exact hg        exact hg      · simp only [h1, ↓reduceIte, MulMemClass.coe_mul]        rw [timeContract_zero_of_diff_grade]        simp only [zero_mul, smul_zero]        rw [superCommute_anPart_ofFieldOpF_diff_grade_zero]        simp only [zero_mul, smul_zero]        exact hg        exact fun a => hg (id (Eq.symm a))    · rw [timeContract_of_not_gradingCompliant]      simp only [Nat.succ_eq_add_one, Fin.getElem_fin, mul_zero, ZeroMemClass.coe_zero, smul_zero,        zero_mul]      exact hg'