Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN (mass μ • ProbabilityMeasure.toFiniteMeasure (normalize μ)) f =
    mass μ * testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN μ f = mass μ * testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f
nth_rw 1 [μ.self_eq_mass_smul_normalize]
no goals
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN (mass μ • ProbabilityMeasure.toFiniteMeasure (normalize μ)) f =
    mass μ * testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f
rw [μ.normalize.toFiniteMeasure.smul_testAgainstNN_apply μ.mass f, smul_eq_mul]