no goals
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.47387
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
c : ℝ≥0
⊢ testAgainstNN μ (const Ω c) = c * mass μ
simp [← ENNReal.coe_eq_coe]