Insert And Contract snd Field Of Contract some incl

@[simp]lemma insertAndContract_sndFieldOfContract_some_incl (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :    (φsΛ ↩Λ φ i (some j)).sndFieldOfContract    (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by      simp [insertAndContractNat]⟩) =    if i < i.succAbove j.1 then    finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j.1) else    finCongr (insertIdx_length_fin φ φs i).symm i := by  split  · rename_i h    refine (φsΛ ↩Λ φ i (some j)).eq_sndFieldOfContract_of_mem      (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by        simp [insertAndContractNat]⟩)      (i := finCongr (insertIdx_length_fin φ φs i).symm i) (j :=        finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_    · simp [congrLift]    · simp [congrLift]    · rw [Fin.lt_def] at h ⊢      simp_all  · rename_i h    refine (φsΛ ↩Λ φ i (some j)).eq_sndFieldOfContract_of_mem      (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by        simp [insertAndContractNat]⟩)      (i := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))      (j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_    · simp [congrLift]    · simp [congrLift]    · rw [Fin.lt_def] at h ⊢      simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.val_cast]      have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j      omega