Null Measurable debut

lemma nullMeasurable_debut {ι : Type}    [ConditionallyCompleteLinearOrder ι] [DenselyOrdered ι] [NoMaxOrder ι]    [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [PolishSpace ι] [BorelSpace ι]    {P : Measure Ω} [IsFiniteMeasure P] {s : Set (ι × Ω)}    (hs : IsPavingAnalytic MeasurableSet s) (u : ι) :    NullMeasurable (debut s u) P := by  have h_lt (r : ι) : NullMeasurableSet {ω | debut s u ω < r} P :=    hs.nullMeasurableSet_debut_lt u r  refine nullMeasurable_of_Iio fun x ↦ ?_  cases x with  | top =>    obtain ⟨v, hv⟩ := exists_seq_tendsto (atTop : Filter ι)    have : debut s u ⁻¹' Set.Iio (⊤ : WithTop ι) = ⋃ (n : ℕ), {ω | debut s u ω < v n} := by      ext ω      simp only [Set.mem_preimage, Set.mem_Iio, Set.mem_iUnion, Set.mem_ofPred_eq]      refine ⟨fun h_debut ↦ ?_, fun ⟨i, h_lt⟩ ↦ lt_top_of_lt h_lt⟩      lift debut s u ω to ι using h_debut.ne with x      norm_cast      exact (Tendsto.eventually_gt_atTop hv x).exists    rw [this]    exact NullMeasurableSet.iUnion fun n ↦ mod_cast h_lt (v n)  | coe r => exact h_lt r