no goals
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.53064
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0
simp only [testAgainstNN, toMeasure_zero, lintegral_zero_measure, ENNReal.zero_toNNReal]