∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
  [inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal]
  (c : R) (μ : MeasureTheory.FiniteMeasure Ω), c • ⇑μ = ⇑(c • μ)