no goals
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑(normalize μ) s)) s = (mass μ)⁻¹ * (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
simp only [μ.self_eq_mass_mul_normalize, μ.mass_nonzero_iff.mpr nonzero, inv_mul_cancel_left₀,
  Ne.def, not_false_iff]