∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {inst : Preorder ι} {μ : MeasureTheory.Measure Ω}
  {f : MeasureTheory.Filtration ι m} [self : MeasureTheory.SigmaFiniteFiltration μ f] (i : ι),
  MeasureTheory.SigmaFinite (μ.trim ⋯)