α : Type u_1
β : Type ?u.1758951
γ : Type ?u.1758954
δ : Type ?u.1758957
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (r • f)) s = ↑↑(r • withDensity μ f) s
α : Type u_1
β : Type ?u.1758951
γ : Type ?u.1758954
δ : Type ?u.1758957
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ withDensity μ (r • f) = r • withDensity μ f
refine' Measure.ext fun s hs => _
α : Type u_1
β : Type ?u.1758951
γ : Type ?u.1758954
δ : Type ?u.1758957
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, (r • f) a ∂μ) = ∫⁻ (a : α) in s, r * f a ∂μ
α : Type u_1
β : Type ?u.1758951
γ : Type ?u.1758954
δ : Type ?u.1758957
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (r • f)) s = ↑↑(r • withDensity μ f) s
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
  smul_eq_mul, ← lintegral_const_mul r hf]
no goals
α : Type u_1
β : Type ?u.1758951
γ : Type ?u.1758954
δ : Type ?u.1758957
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, (r • f) a ∂μ) = ∫⁻ (a : α) in s, r * f a ∂μ
rfl