-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem eq_singularPart (t : SignedMeasure α) (f : α → ℝ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure)
    (hadd : s = t + μ.withDensityᵥ f) : t = s.singularPart μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ s = t + μ.withDensityᵥ (AEStronglyMeasurable.mk f ⋯)

Tactic:
convert hadd using 2

Result:
case h.e'_3.h.e'_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ μ.withDensityᵥ (AEStronglyMeasurable.mk f ⋯) = μ.withDensityᵥ f

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ t = s.singularPart μ

Tactic:
by_cases hfi : Integrable f μ

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

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0

Tactic:
rwa [withDensityᵥ_zero, add_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Proof state:
case h.e'_3.h.e'_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ μ.withDensityᵥ (AEStronglyMeasurable.mk f ⋯) = μ.withDensityᵥ f

Tactic:
exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ t = s.singularPart μ

Tactic:
refine eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ ?_

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ s = t + μ.withDensityᵥ (AEStronglyMeasurable.mk f ⋯)

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
refine eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0