∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [Nonempty Z]
  [inst : TopologicalSpace Z] [TopologicalSpace.IsCompletelyMetrizableSpace Z],
  MeasureTheory.StronglyMeasurable g → ∃ h, MeasureTheory.StronglyMeasurable h ∧ g = h ∘ f