∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β}
  {μ : MeasureTheory.Measure β} (c : ENNReal),
  MeasureTheory.Measure.comap f (c • μ) = c • MeasureTheory.Measure.comap f μ