Static Wick Term insert zero some

lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (φsΛ : WickContraction φs.length) (k : { x // x ∈ φsΛ.uncontracted }) :    (φsΛ ↩Λ φ 0 k).staticWickTerm =    sign φs φsΛ • (↑φsΛ.staticContract *    (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *    𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedFieldOpEquiv φs φsΛ k))))) := by  symm  rw [staticWickTerm, normalOrder_uncontracted_some]  simp only [← mul_assoc]  rw [← smul_mul_assoc]  congr 1  rw [staticContract_insert_some_of_lt (hik := by simp), smul_smul]  by_cases hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[k.1])  · congr 1    · rw [sign_insert_some_zero _ _ _ _ hn, mul_comm, ← mul_assoc]      simp    · rw [Subalgebra.mem_center_iff.mp φsΛ.staticContract.2]  · simp only [Fin.getElem_fin, not_and] at hn    by_cases h0 : ¬ GradingCompliant φs φsΛ    · rw [staticContract_of_not_gradingCompliant _ _ h0]      simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero, mul_zero]    · simp_all only [not_not, forall_const]      have h1 : contractStateAtIndex φ [φsΛ]ᵘᶜ (uncontractedFieldOpEquiv φs φsΛ k) = 0 := by        simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,          Equiv.coe_trans, Option.map_some, Function.comp_apply, finCongr_apply,          Fin.val_cast, Fin.getElem_fin, smul_eq_zero]        right        simp only [uncontractedListGet, List.getElem_map,          uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem]        rw [superCommute_anPart_ofFieldOpF_diff_grade_zero (h := hn)]      simp [h1]