α : Type u_1
β : Type ?u.1755336
γ : Type ?u.1755339
δ : Type ?u.1755342
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ f) s = ↑↑(withDensity μ g) s
α : Type u_1
β : Type ?u.1755336
γ : Type ?u.1755339
δ : Type ?u.1755342
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ withDensity μ f = withDensity μ g
refine Measure.ext fun s hs => ?_
α : Type u_1
β : Type ?u.1755336
γ : Type ?u.1755339
δ : Type ?u.1755342
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, f a ∂μ) = ∫⁻ (a : α) in s, g a ∂μ
α : Type u_1
β : Type ?u.1755336
γ : Type ?u.1755339
δ : Type ?u.1755342
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ f) s = ↑↑(withDensity μ g) s
rw [withDensity_apply _ hs, withDensity_apply _ hs]
no goals
α : Type u_1
β : Type ?u.1755336
γ : Type ?u.1755339
δ : Type ?u.1755342
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, f a ∂μ) = ∫⁻ (a : α) in s, g a ∂μ
exact lintegral_congr_ae (ae_restrict_of_ae h)