∀ {α : Type u_2} {β : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  (f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β)
  (hf : ∀ (μ : MeasureTheory.Measure α), inst ≤ (f μ.toOuterMeasure).caratheodory) (c : ENNReal)
  (μ : MeasureTheory.Measure α) (s : Set β),
  MeasurableSet s →
    ((f (c • μ).toOuterMeasure).toMeasure ⋯) s = ((RingHom.id ENNReal) c • (f μ.toOuterMeasure).toMeasure ⋯) s