case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑↑↑(normalize μ) s = ↑↑↑((mass μ)⁻¹ • μ) s
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ↑(normalize μ) = ↑((mass μ)⁻¹ • μ)
ext1 s _s_mble
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑(mass μ)⁻¹ * ↑↑↑μ s = ↑↑↑((mass μ)⁻¹ • μ) s
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑↑↑(normalize μ) s = ↑↑↑((mass μ)⁻¹ • μ) s
rw [← μ.normalize.ennreal_coeFn_eq_coeFn_toMeasure s, μ.normalize_eq_of_nonzero nonzero s,
  ENNReal.coe_mul, ennreal_coeFn_eq_coeFn_toMeasure]
no goals
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑(mass μ)⁻¹ * ↑↑↑μ s = ↑↑↑((mass μ)⁻¹ • μ) s
exact Measure.coe_nnreal_smul_apply _ _ _