no goals
Ω : Type u_2
inst✝⁵ : MeasurableSpace Ω
R : Type u_1
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
s : Set Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑(c • μ) s)) s = c • (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
rw [coeFn_smul, Pi.smul_apply]