Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.51970
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ ENNReal.toNNReal (↑↑↑μ univ) = mass μ
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.51970
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ testAgainstNN μ 1 = mass μ
simp only [testAgainstNN, coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_one]
no goals
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.51970
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ ENNReal.toNNReal (↑↑↑μ univ) = mass μ
rfl