MeasureTheory.aemeasurable_Ici_of_forall_Icc

theorem aemeasurable_Ici_of_forall_Icc {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type*}  {mβ : MeasurableSpace β} [LinearOrder α] [(atTop : Filter α).IsCountablyGenerated] {x : α} {g : α → β}  (g_meas : ∀ t ≥ x, AEMeasurable g (μ.restrict (Set.Icc x t))) : AEMeasurable g (μ.restrict (Set.Ici x)) := by  haveI : Nonempty α := ⟨x⟩  obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (atTop : Filter α)  have Ici_eq_iUnion : Ici x = ⋃ n : ℕ, Icc x (u n) := by    rw [iUnion_Icc_eq_Ici_self_iff.mpr _]    exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists  rw [Ici_eq_iUnion, aemeasurable_iUnion_iff]  intro n  rcases le_or_gt x (u n) with h | h  · exact g_meas (u n) h  · rw [Icc_eq_empty (not_le.mpr h), Measure.restrict_empty]    exact aemeasurable_zero_measure