Time Order F eq max Time Field mul finset

lemma timeOrderF_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :    𝓣ᶠ(ofFieldOpListF (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,      (Finset.filter (fun x =>        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •      ofFieldOpF (maxTimeField φ φs) * 𝓣ᶠ(ofFieldOpListF (eraseMaxTimeField φ φs)) := by  rw [timeOrderF_eq_maxTimeField_mul]  congr 3  apply FieldStatistic.ofList_perm  nth_rewrite 1 [← List.map_get_finRange (φ :: φs)]  simp only [List.length_cons, eraseMaxTimeField, insertionSortDropMinPos]  rw [eraseIdx_get, ← List.map_take, ← List.map_map]  refine List.Perm.map (φ :: φs).get ?_  apply (List.perm_ext_iff_of_nodup _ _).mpr  · intro i    simp only [List.length_cons, maxTimeFieldPos, mem_take_finrange, Fin.val_fin_lt, List.mem_map,      Finset.mem_sort, Finset.mem_filter, Finset.mem_univ, true_and, Function.comp_apply]    refine Iff.intro (fun hi => ?_) (fun h => ?_)    · have h2 := (maxTimeFieldPosFin φ φs).2      simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,        maxTimeFieldPosFin, insertionSortMinPosFin] at h2      use ⟨i, by omega⟩      apply And.intro      · simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, maxTimeFieldPosFin,        insertionSortMinPosFin, Nat.succ_eq_add_one, Fin.mk_lt_mk, Fin.val_fin_lt, Fin.succ_mk]        rw [Fin.lt_def]        split        · simp only [Fin.val_fin_lt]          omega        · omega      · simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, Fin.succ_mk, Fin.ext_iff,        Fin.val_cast]        split        · simp        · simp_all [Fin.lt_def]    · obtain ⟨j, h1, h2⟩ := h      subst h2      simp only [Fin.lt_def, Fin.val_cast]      exact h1  · exact List.Sublist.nodup (List.take_sublist _ _) <|      List.nodup_finRange (φs.length + 1)  · refine List.Nodup.map ?_ ?_    · refine Function.Injective.comp ?hf.hg Fin.succAbove_right_injective      exact Fin.cast_injective (eraseIdx_length (φ :: φs) (insertionSortMinPos timeOrderRel φ φs))    · exact Finset.sort_nodup        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)          Finset.univ) (fun x1 x2 => x1 ≤ x2)