∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] (f : Ω → Ω')
  (μ : MeasureTheory.FiniteMeasure Ω'), MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.comap f ↑μ)