no goals
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.54872
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
c : ℝ≥0
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN (c • μ) f = c • testAgainstNN μ f
simp only [testAgainstNN, toMeasure_smul, smul_eq_mul, ← ENNReal.smul_toNNReal, ENNReal.smul_def,
  lintegral_smul_measure]