no goals
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f = (mass μ)⁻¹ * testAgainstNN μ f
simp [μ.testAgainstNN_eq_mass_mul, inv_mul_cancel_left₀ <| μ.mass_nonzero_iff.mpr nonzero]