no goals
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.39681
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : FiniteMeasure Ω
A : Set Ω
⊢ mass (restrict μ A) = (fun s => ENNReal.toNNReal (↑↑↑μ s)) A
simp only [mass, restrict_apply μ A MeasurableSet.univ, univ_inter]