Class D of uniform Integrable bounded stopping Time

lemma classD_of_uniformIntegrable_bounded_stoppingTime    (hX : UniformIntegrable (fun T : {T | IsStoppingTime 𝓕 T ∧ ∃ t : ι, ∀ ω, T ω ≤ t}      ↦ stoppedValue X T) 1 P) (hm : IsStronglyProgressive 𝓕 X) :    ClassD X 𝓕 P := by  have (T : {T | IsStoppingTime 𝓕 T ∧ ∀ ω, T ω ≠ ⊤}) :      ∃ N : ℕ → {T | IsStoppingTime 𝓕 T ∧ ∃ t : ι, ∀ ω, T ω ≤ t},      ∀ᵐ ω ∂P, Tendsto (fun n ↦ stoppedValue X (N n).1 ω) atTop (𝓝 (stoppedValue X T.1 ω)) := by    obtain ⟨v, hv⟩ := exists_seq_monotone_tendsto_atTop_atTop ι    refine ⟨fun n => ⟨(fun ω => v n) ⊓ T.1, ⟨IsStoppingTime.min ?_ T.2.1, ?_⟩⟩, ?_⟩    · exact (isStoppingTime_const 𝓕 (v n))    · exact ⟨v n, fun ω => by simp⟩    · filter_upwards with ω      simp_all only [tendsto_atTop_atTop, tendsto_atTop_nhds]      intro U hU _      obtain ⟨N, hN⟩ := hv.2 (T.1 ω).untopA      refine ⟨N, fun n hn => ?_⟩      have : (T.1 ω).untopA = T.1 ω := by simp [WithTop.untopA_eq_untop (T.2.2 ω)]      rw [stoppedValue, Pi.inf_apply, ← this, ← WithTop.coe_min (v n) (T.1 ω).untopA,        min_eq_right (hN n hn)]      exact hU  exact ⟨hm, (hX.uniformIntegrable_of_ae_tendsto _).comp    (fun T : {T | IsStoppingTime 𝓕 T ∧ ∀ ω, T ω ≠ ⊤} => ⟨stoppedValue X T.1, this T⟩)⟩