case h
Ω : 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 Ω
x✝ : Set Ω
⊢ ENNReal.toNNReal (↑↑↑(c • μ) x✝) = (c • fun s => ENNReal.toNNReal (↑↑↑μ s)) x✝
Ω : 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 Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑(c • μ) s)) = c • fun s => ENNReal.toNNReal (↑↑↑μ s)
funext
case h
Ω : 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 Ω
x✝ : Set Ω
⊢ ↑↑↑(c • μ) x✝ = c • ↑↑↑μ x✝
case h
Ω : 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 Ω
x✝ : Set Ω
⊢ ENNReal.toNNReal (↑↑↑(c • μ) x✝) = (c • fun s => ENNReal.toNNReal (↑↑↑μ s)) x✝
simp [← ENNReal.coe_eq_coe,  ENNReal.coe_smul]
no goals
case h
Ω : 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 Ω
x✝ : Set Ω
⊢ ↑↑↑(c • μ) x✝ = c • ↑↑↑μ x✝
norm_cast