∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [inst : LinearOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m},
  MeasureTheory.IsStoppingTime f τ → (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}