Measure Theory Is Strongly Progressive has Strongly Measurable Sup Process

lemma _root_.MeasureTheory.IsStronglyProgressive.hasStronglyMeasurableSupProcess {ι : Type*}    [MeasurableSpace ι] [ConditionallyCompleteLinearOrder ι]    [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] [BorelSpace ι]    {X : ι → Ω → E} (P : Measure Ω) [IsFiniteMeasure P]    {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous]    (hX_prog : IsStronglyProgressive 𝓕 X) :    HasStronglyMeasurableSupProcess (mΩ := mΩ) X := by  refine Measurable.stronglyMeasurable ?_ -- todo: change the def to use measurable  refine measurable_of_Ioi fun a ↦ ?_  by_cases ha_top : a = ⊤  · simp [ha_top]  let τ a := leastGT (fun t ω ↦ ‖X t ω‖) a  have hτ a : IsStoppingTime 𝓕 (τ a) := isStoppingTime_leastGT P hX_prog.norm _  have : ((fun tω : ι × Ω ↦ ⨆ s ≤ tω.1, ‖X s tω.2‖ₑ) ⁻¹' Set.Ioi a)      = {tω | τ a.toReal tω.2 < tω.1} ∪ {tω | a < ‖X tω.1 tω.2‖ₑ} := by    calc ((fun tω : ι × Ω ↦ ⨆ s ≤ tω.1, ‖X s tω.2‖ₑ) ⁻¹' Set.Ioi a)    _ = {tω | ∃ s ≤ tω.1, a < ‖X s tω.2‖ₑ} := by ext ⟨t, ω⟩; simp [lt_iSup_iff]    _ = {tω | ∃ s < tω.1, a < ‖X s tω.2‖ₑ} ∪ {tω | a < ‖X tω.1 tω.2‖ₑ} := by ext; simp; grind    _ = {tω | τ a.toReal tω.2 < tω.1} ∪ {tω | a < ‖X tω.1 tω.2‖ₑ} := by      ext ⟨t, ω⟩      simp only [Set.mem_union, Set.mem_ofPred_eq, τ]      rw [leastGT_lt_iff]      simp_rw [← toReal_enorm, ENNReal.toReal_lt_toReal ha_top enorm_ne_top]  rw [this]  refine (measurableSet_lt ?_ (by fun_prop)).union ?_  · exact (hτ a.toReal).measurable'.comp measurable_snd  · refine (measurableSet_Ioi (a := a)).preimage ?_    suffices Measurable (fun tω : ι × Ω ↦ ‖X tω.1 tω.2‖) by      simp_rw [← ofReal_norm]      fun_prop    refine StronglyMeasurable.measurable ?_    exact ProgMeasurable.stronglyMeasurable_uncurry_of_isCountablyGenerated_atTop hX_prog.norm