Class DL locally class D

lemma ClassDL.locally_classD [SecondCountableTopology ι] [PseudoMetrizableSpace ι]    (hX : ClassDL X 𝓕 P) :    Locally (ClassD · 𝓕 P) 𝓕 X P := by  rcases topOrderOrNoTopOrder ι with ha | hb  · exact .of_prop hX.classD  obtain ⟨v, hv1, hv2⟩ := exists_seq_monotone_tendsto_atTop_atTop ι  refine ⟨fun n ω => v n, ⟨⟨fun n => ?_, ?_⟩, ?_⟩, fun n => ⟨?_, ?_⟩⟩  · simp [isStoppingTime_const]  · filter_upwards with ω    simp only [tendsto_atTop_atTop] at hv2    refine tendsto_atTop_isLUB (fun _ _ h => mod_cast hv1 h) ⟨top_mem_upperBounds _, fun x hx => ?_⟩    simp only [top_le_iff, WithTop.eq_top_iff_forall_gt]    simp only [mem_upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hx    intro a    obtain ⟨c, hc⟩ := (NoTopOrder.to_noMaxOrder ι).exists_gt a    obtain ⟨n, hn⟩ := hv2 c    exact lt_of_lt_of_le (WithTop.coe_lt_coe.mpr (lt_of_lt_of_le hc (hn n le_rfl))) (hx n)  · filter_upwards with ω    exact fun _ _ h => WithTop.coe_le_coe.mpr (hv1 h)  · refine IsStronglyProgressive.stoppedProcess (fun t => ?_) (by simp [isStoppingTime_const])    by_cases hb : ⊥ < (v n : WithTop ι)    · simp [hb, hX.1 t]    · simp [hb, stronglyMeasurable_const]  · let A := {T : Ω → WithTop ι | IsStoppingTime 𝓕 T ∧ ∀ ω, T ω ≠ ⊤}    let Y := fun T : A ↦ stoppedValue (stoppedProcess X (fun _ ↦ v n)) T    refine uniformIntegrable_of_dominated (Y := Y) ?_ (fun T => ?_) (fun T => ?_)    · let B := {T : Ω → WithTop ι | IsStoppingTime 𝓕 T ∧ ∀ ω, T ω ≤ v n}      let f : A → B := fun T => ⟨T.1 ⊓ (fun ω => ↑(v n)), ⟨T.2.1.min_const (v n), by simp⟩⟩      have : Y = (fun T : B ↦ stoppedValue X T) ∘ f := by        ext T        exact stoppedValue_stoppedProcess_apply (T.2.2 _)      rw [this]      exact UniformIntegrable.comp (hX.2 (v n)) f    · by_cases hb : ⊥ < (v n : WithTop ι)      · simp only [hb, Set.ofPred_true, Set.indicator_univ, ne_eq, Set.mem_ofPred_eq]        refine AEStronglyMeasurable.congr ?_ (stoppedValue_stoppedProcess_ae_eq ?_).symm        · refine (StronglyMeasurable.mono ?_ (𝓕.le' (v n))).aestronglyMeasurable          refine stronglyMeasurable_stoppedValue_of_le hX.1 ((T.2.1).min_const _) (fun ω => ?_)          grind        · exact ae_of_all P T.2.2      · unfold stoppedValue        simp only [hb, Set.ofPred_false, Set.indicator_empty, ne_eq, Set.mem_ofPred_eq,          stoppedProcess_const]        fun_prop    · by_cases hb : ⊥ < (v n : WithTop ι)      · simpa [hb, Y] using ⟨T.1, T.2, ae_of_all P fun ω => rfl.le⟩      · simpa [hb, Y, stoppedValue] using ⟨T.1, T.2⟩