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