∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : α ≃ᵐ β) [MeasureTheory.SigmaFinite μ], MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (⇑f) μ)