Wick Term insert none

lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :    (φsΛ ↩Λ φ i none).wickTerm =    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)    • (φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ))) := by  rw [wickTerm]  by_cases hg : GradingCompliant φs φsΛ  · rw [normalOrder_uncontracted_none, sign_insert_none _ _ _ _ hg]    simp only [Nat.succ_eq_add_one, timeContract_insert_none,      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]    congr 1    rw [← mul_assoc]    congr 1    rw [← map_mul]    congr    rw [ofFinset_union]    congr    ext a    simp only [Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and,      Finset.mem_inter, not_and, not_lt, and_imp]    apply Iff.intro    · intro ha      have ha1 := ha.1      rcases ha1 with ha1 | ha1      · exact ha1.2      · exact ha1.2    · intro ha      simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and, ha, and_true,        forall_const]      have hx : φsΛ.getDual? a = none ↔ ¬ (φsΛ.getDual? a).isSome := by        simp      rw [hx]      simp only [Bool.not_eq_true, Bool.eq_false_or_eq_true_self, true_and]      intro h1 h2      simp_all  · simp only [Nat.succ_eq_add_one, timeContract_insert_none, Algebra.smul_mul_assoc]    rw [timeContract_of_not_gradingCompliant]    simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero]    exact hg