Is Stopping Time debut

theorem isStoppingTime_debut [MeasurableSpace ι] [ConditionallyCompleteLinearOrder ι]    [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] [BorelSpace ι]    (P : Measure Ω) [IsFiniteMeasure P]    {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous]    {E : Set (ι × Ω)} (hE : ProgMeasurableSet E 𝓕) (n : ι) :    IsStoppingTime 𝓕 (debut E n) := by  intro t  rcases lt_or_ge t n with htn | hnt  · convert MeasurableSet.empty    ext ω    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false, not_le]    refine (mod_cast htn : (t : WithTop ι) < n).trans_le ?_    exact le_debut ω  -- case on whether `t` is isolated on the right or not  by_cases ht_gt : (𝓝[>] t).NeBot  swap  -- if it's isolated then `{debut ≤} = {debut <} ∪ {(t, ω) ∈ E}`  · have h_eq : {ω | debut E n ω ≤ t} = {ω | debut E n ω < t} ∪ {ω | (t, ω) ∈ E} := by      ext ω      simp only [Set.mem_ofPred_eq, Set.mem_union]      rw [le_iff_lt_or_eq]      rcases lt_or_ge (debut E n ω) t with h_lt | h_ge      · simp [h_lt]      -- `⊢ debut E n ω = ↑t ↔ (t, ω) ∈ E`; use `𝓝[>] t = ⊥`      congr!      rw [debut_eq_iff_of_nhdsGT_eq_bot E hnt ?_ _ h_ge]      simpa using ht_gt    rw [h_eq]    exact (hE.measurableSet_debut_lt P n t).union (hE.measurableSet_preimage_prodMk P t)  -- now `t` is a limit point on the right  obtain ⟨s, hs_gt, hs_tendsto⟩ : ∃ s : ℕ → ι, (∀ n, t < s n) ∧ Tendsto s atTop (𝓝 t) := by    have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx    have := exists_seq_forall_of_frequently h_freq    simp_rw [tendsto_nhdsWithin_iff] at this    obtain ⟨s, ⟨hs_tendsto, _⟩, hs_gt⟩ := this    exact ⟨s, hs_gt, hs_tendsto⟩  have h_exists_lt (u : ι) (hu : t < u) : ∃ i, s i < u :=    Eventually.exists (f := atTop) (hs_tendsto.eventually_lt_const hu)  have h_exists_lt' (u : WithTop ι) (hu : t < u) : ∃ i, s i < u := by    refine Eventually.exists (f := atTop) ?_    have hs_tendsto' : Tendsto (fun n ↦ (s n : WithTop ι)) atTop (𝓝 (t : WithTop ι)) :=      WithTop.continuous_coe.continuousAt.tendsto.comp hs_tendsto    exact hs_tendsto'.eventually_lt_const hu  -- we write `{debut ≤ t}` as a countable intersection of `{debut < s n}`  have h_eq_iInter : {ω | debut E n ω ≤ t} = ⋂ m, {ω | debut E n ω < s m} := by    ext ω    simp only [Set.mem_ofPred_eq, Set.mem_iInter]    refine ⟨fun h_le m ↦ h_le.trans_lt (mod_cast (hs_gt m)), fun h_lt ↦ ?_⟩    refine le_of_forall_gt fun u hu ↦ ?_    obtain ⟨i, hi⟩ : ∃ i, s i < u := h_exists_lt' u hu    exact (h_lt i).trans hi  rw [h_eq_iInter]  have h_meas_lt m : MeasurableSet[𝓕 (s m)] {ω | debut E n ω < s m} :=    hE.measurableSet_debut_lt P n (s m)  have h𝓕_eq_iInf : 𝓕 t = ⨅ m, 𝓕 (s m) := by    have ht_cont : 𝓕 t = 𝓕.rightCont t := by      congr      exact Filtration.IsRightContinuous.eq.symm    rw [ht_cont, Filtration.rightCont_eq_of_neBot_nhdsGT]    refine le_antisymm ?_ ?_    · simp only [gt_iff_lt, le_iInf_iff]      exact fun i ↦ iInf₂_le (s i) (hs_gt i)    · simp only [gt_iff_lt, le_iInf_iff]      intro i hti      obtain ⟨m, hm⟩ := h_exists_lt i hti      exact (iInf_le _ m).trans (𝓕.mono hm.le)  rw [h𝓕_eq_iInf]  simp only [MeasurableSpace.measurableSet_sInf, Set.mem_range, forall_exists_index,    forall_apply_eq_imp_iff]  intro k  have h_eq_k : ⋂ m, {ω | debut E n ω < s m} =      ⋂ (m) (hm : s m ≤ s k), {ω | debut E n ω < s m} := by    ext x    simp only [Set.mem_iInter, Set.mem_ofPred_eq]    refine ⟨fun h m _ ↦ h m, fun h m ↦ ?_⟩    rcases le_total (s m) (s k) with hmk | hkm    · exact h m hmk    · exact (h k le_rfl).trans_le (mod_cast hkm)  rw [h_eq_k]  refine MeasurableSet.iInter fun m ↦ MeasurableSet.iInter fun hm ↦ ?_  exact 𝓕.mono hm _ (h_meas_lt m)