case pos
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ t = singularPart s μ

case neg
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : ¬Integrable f
⊢ t = singularPart s μ
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ t = singularPart s μ
by_cases hfi : Integrable f μ
case pos
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ s = t + withDensityᵥ μ (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ))
case pos
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ t = singularPart s μ
refine' eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ _
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ withDensityᵥ μ (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) = withDensityᵥ μ f
case pos
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ s = t + withDensityᵥ μ (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ))
convert hadd using 2
no goals
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ withDensityᵥ μ (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) = withDensityᵥ μ f
exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
case neg
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ t = singularPart s μ
case neg
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : ¬Integrable f
⊢ t = singularPart s μ
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
case neg
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ s = t + withDensityᵥ μ 0
case neg
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ t = singularPart s μ
refine' eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ _
no goals
case neg
α : Type u_1
β : Type ?u.582150
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ s = t + withDensityᵥ μ 0
rwa [withDensityᵥ_zero, add_zero]