α : Type u_1
β : Type ?u.1755617
γ : Type ?u.1755620
δ : Type ?u.1755623
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (f + g)) s = ↑↑(withDensity μ f + withDensity μ g) s
α : Type u_1
β : Type ?u.1755617
γ : Type ?u.1755620
δ : Type ?u.1755623
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ withDensity μ (f + g) = withDensity μ f + withDensity μ g
refine' Measure.ext fun s hs => _
α : Type u_1
β : Type ?u.1755617
γ : Type ?u.1755620
δ : Type ?u.1755623
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, (f + g) a ∂μ) = ∫⁻ (a : α) in s, f a + g a ∂μ
α : Type u_1
β : Type ?u.1755617
γ : Type ?u.1755620
δ : Type ?u.1755623
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (f + g)) s = ↑↑(withDensity μ f + withDensity μ g) s
rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
  ← lintegral_add_left hf]
no goals
α : Type u_1
β : Type ?u.1755617
γ : Type ?u.1755620
δ : Type ?u.1755623
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, (f + g) a ∂μ) = ∫⁻ (a : α) in s, f a + g a ∂μ
rfl