Measure Theory Submartingale tau Mesh lt top eq lt predictable Seq Top

lemma MeasureTheory.Submartingale.tauMesh_lt_top_eq_lt_predictableSeqTop {ι Ω : Type*}    [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]    {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ}    (hs : Submartingale S 𝓕 P) (n : ℕ) {c : ℝ} (hc : 0 ≤ c) :    {ω | tauMesh S 𝓕 P n c ω < (⊤ : mesh ι n)} =ᵐ[P] {ω | c < predictableSeqTop S 𝓕 P n ω} := by  refine eventuallyEq_set.2 ?_  have hs_mesh : Submartingale (S ∘ Subtype.val) (meshFiltration 𝓕 n) P :=    hs.indexComap (Subtype.mono_coe (SetLike.coe (mesh ι n)))  filter_upwards [hs_mesh.monotone_predictablePart_ae] with ω hmono  let A : mesh ι n → Ω → ℝ := _root_.predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P  by_cases htop_bot : (⊤ : mesh ι n) = ⊥  · simp [tauMesh, predictableSeqTop, htop_bot, hc]  · refine ⟨fun hω => ?_, fun htop_gt => ?_⟩    · simp_all only [tauMesh, WithTop.coe_lt_coe, Std.le_refl, hittingBtwn_lt_iff, Set.Ico_bot,        Set.mem_Iio, Set.mem_Ioi, predictableSeqTop]      obtain ⟨j, _, hj⟩ := hω      exact lt_of_lt_of_le hj (hmono le_top)    · have hnot_min : ¬ IsMin (⊤ : mesh ι n) := by simpa [isMin_iff_eq_bot] using htop_bot      have hmem : A (succ (pred ⊤)) ω ∈ Set.Ioi c := by        simpa [A, succ_pred_of_not_isMin hnot_min, predictableSeqTop] using htop_gt      have hhit : hittingBtwn (fun (t : mesh ι n) ω ↦ A (succ t) ω) (Set.Ioi c) ⊥ ⊤ ω < ⊤ := by        rw [hittingBtwn_lt_iff ⊤ le_rfl]        exact ⟨pred ⊤, ⟨bot_le, (pred_lt_iff_ne_bot).2 htop_bot⟩, hmem⟩      simpa [tauMesh, A] using hhit