Measure Theory Submartingale class DL

lemma _root_.MeasureTheory.Submartingale.classDL    (hX1 : Submartingale X 𝓕 P) (hX2 : ∀ ω, IsRightContinuous (X · ω))    (hX3 : 0 ≤ X) : ClassDL X 𝓕 P := by  refine ⟨StronglyAdapted.isStronglyProgressive_of_rightContinuous hX1.1 hX2, fun t => ?_⟩  have := (hX1.2.2 t).uniformIntegrable_condExp' (fun T :    {T | IsStoppingTime 𝓕 T ∧ ∀ (ω : Ω), T ω ≤ t} => IsStoppingTime.measurableSpace_le T.2.1)  refine uniformIntegrable_of_dominated this (fun T => ?_) (fun T => ⟨T, ?_⟩)  · exact ((stronglyMeasurable_stoppedValue_of_le (hX1.1.isStronglyProgressive_of_rightContinuous      hX2) T.2.1 T.2.2).mono (𝓕.le' t)).aestronglyMeasurable  · have : stoppedValue X T.1 ≤ᵐ[P] P[stoppedValue X (fun ω => t)|T.2.1.measurableSpace] := by      suffices lem : stoppedValue X ((fun ω => t) ⊓ T.1) ≤ᵐ[P]        P[stoppedValue X (fun ω => t)|T.2.1.measurableSpace] from by        have : T.1 ⊓ (fun ω => t) = T.1 := by simp only [inf_eq_left]; exact T.2.2        simpa [inf_comm, this] using lem      exact hX1.stoppedValue_min_ae_le_condExp 𝓕 hX2        (Eventually.of_forall (fun ω => le_rfl)) T.2.1 (isStoppingTime_const 𝓕 t)    simp only [stoppedValue_const] at this    filter_upwards [this] with ω hω    have p1 : 0 ≤ stoppedValue X T.1 ω := by simpa [stoppedValue] using (hX3 (T.1 ω).untopA ω)    have p2 := abs_of_nonneg (le_trans p1 hω)    rw [← abs_of_nonneg p1, ← p2] at hω    exact norm_le_norm_of_abs_le_abs hω