∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : β → α) [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.comap f μ)