Normal Order uncontracted none

lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :    𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ)    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •    𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := by  simp only [Nat.succ_eq_add_one]  rw [ofFieldOpList_normalOrder_insert φ [φsΛ]ᵘᶜ    ⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩,    smul_smul]  refine (one_smul ℂ _).symm.trans ?_  congr 1  simp only [uncontractedListGet]  rw [← List.map_take, take_uncontractedListOrderPos_eq_filter]  have h1 : (𝓕 |>ₛ List.map φs.get (List.filter (fun x => decide (↑x < i.1)) φsΛ.uncontractedList))        = 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x.val < i.1))⟩ := by      simp only [Nat.succ_eq_add_one, ofFinset]      congr      rw [uncontractedList_eq_sort]      have hdup : (List.filter (fun x => decide (x.1 < i.1))          (φsΛ.uncontracted.sort (fun x1 x2 => x1 ≤ x2))).Nodup :=        List.Nodup.filter _ (φsΛ.uncontracted.sort_nodup (fun x1 x2 => x1 ≤ x2))      have hsort : (List.filter (fun x => decide (x.1 < i.1))          (φsΛ.uncontracted.sort (fun x1 x2 => x1 ≤ x2))).Pairwise (· ≤ ·) :=        List.Pairwise.filter _ (φsΛ.uncontracted.pairwise_sort (fun x1 x2 => x1 ≤ x2))      rw [← (List.toFinset_sort (· ≤ ·) hdup).mpr hsort]      congr      ext a      simp  rw [h1]  simp only [Nat.succ_eq_add_one]  have h2 : (Finset.filter (fun x => x.1 < i.1) φsΛ.uncontracted) =    (Finset.filter (fun x => i.succAbove x < i) φsΛ.uncontracted) := by    refine Finset.filter_congr fun a _ => ?_    rw [Fin.succAbove_lt_iff_castSucc_lt, Fin.lt_def, Fin.val_castSucc]  rw [h2]  simp only [exchangeSign_mul_self]  congr  rw [insertAndContract_uncontractedList_none_map]