case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ↑(weightedSMul (c • μ) s) x = ↑(ENNReal.toReal c • weightedSMul μ s) x
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ weightedSMul (c • μ) s = ENNReal.toReal c • weightedSMul μ s
ext1 x
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ↑(weightedSMul (c • μ) s) x = (ENNReal.toReal c • ↑(weightedSMul μ s)) x
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ↑(weightedSMul (c • μ) s) x = ↑(ENNReal.toReal c • weightedSMul μ s) x
push_cast
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ENNReal.toReal (↑↑(c • μ) s) • x = ENNReal.toReal c • ENNReal.toReal (↑↑μ s) • x
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ↑(weightedSMul (c • μ) s) x = (ENNReal.toReal c • ↑(weightedSMul μ s)) x
simp_rw [Pi.smul_apply, weightedSMul_apply]
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ENNReal.toReal ((c • ↑↑μ) s) • x = ENNReal.toReal c • ENNReal.toReal (↑↑μ s) • x
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ENNReal.toReal (↑↑(c • μ) s) • x = ENNReal.toReal c • ENNReal.toReal (↑↑μ s) • x
push_cast
no goals
case h
α : Type u_1
E : Type ?u.30268
F : Type u_2
𝕜 : Type ?u.30274
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ENNReal.toReal ((c • ↑↑μ) s) • x = ENNReal.toReal c • ENNReal.toReal (↑↑μ s) • x
simp_rw [Pi.smul_apply, smul_eq_mul, toReal_mul, smul_smul]