∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} (f : β → α),
  Monotone m ∨ Function.Surjective f →
    (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) =
      MeasureTheory.OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯