-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_add_withDensity_rnDeriv_eq [c.HaveLebesgueDecomposition μ] :
    c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c

Proof state:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i).re = { re := ↑(re c) i, im := ↑(im c) i }.re

Tactic:
rw [Complex.add_re, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.re_eq_complex_re,
  ← integral_re (c.integrable_rnDeriv μ).integrableOn, RCLike.re_eq_complex_re,
  ← withDensityᵥ_apply _ hi]

Result:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i).re + ↑(μ.withDensityᵥ fun x => (c.rnDeriv μ x).re) i = { re := ↑(re c) i, im := ↑(im c) i }.re

α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x => (c.rnDeriv μ x).re) μ

Proof state:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑((re c).singularPart μ + μ.withDensityᵥ ((re c).rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }.re

Tactic:
rw [c.re.singularPart_add_withDensity_rnDeriv_eq μ]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c

Tactic:
conv_rhs => rw [← c.toComplexMeasure_to_signedMeasure]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = (re c).toComplexMeasure (im c)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x => (c.rnDeriv μ x).im) μ

Tactic:
exact SignedMeasure.integrable_rnDeriv _ _

Result:
no goals

Proof state:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i).im + ↑(μ.withDensityᵥ fun x => (c.rnDeriv μ x).im) i = { re := ↑(re c) i, im := ↑(im c) i }.im

Tactic:
change (c.im.singularPart μ + μ.withDensityᵥ (c.im.rnDeriv μ)) i = _

Result:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑((im c).singularPart μ + μ.withDensityᵥ ((im c).rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }.im

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑(c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ)) i = ↑((re c).toComplexMeasure (im c)) i

Tactic:
rw [VectorMeasure.add_apply, SignedMeasure.toComplexMeasure_apply]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }

Proof state:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑((im c).singularPart μ + μ.withDensityᵥ ((im c).rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }.im

Tactic:
rw [c.im.singularPart_add_withDensity_rnDeriv_eq μ]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }

Tactic:
apply Complex.ext

Result:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i).re = { re := ↑(re c) i, im := ↑(im c) i }.re

case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i).im = { re := ↑(re c) i, im := ↑(im c) i }.im

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x => (c.rnDeriv μ x).re) μ

Tactic:
exact SignedMeasure.integrable_rnDeriv _ _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = (re c).toComplexMeasure (im c)

Tactic:
ext i hi : 1

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑(c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ)) i = ↑((re c).toComplexMeasure (im c)) i

Proof state:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i).im = { re := ↑(re c) i, im := ↑(im c) i }.im

Tactic:
rw [Complex.add_im, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.im_eq_complex_im,
  ← integral_im (c.integrable_rnDeriv μ).integrableOn, RCLike.im_eq_complex_im,
  ← withDensityᵥ_apply _ hi]

Result:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i).im + ↑(μ.withDensityᵥ fun x => (c.rnDeriv μ x).im) i = { re := ↑(re c) i, im := ↑(im c) i }.im

α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x => (c.rnDeriv μ x).im) μ

Proof state:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) i).re + ↑(μ.withDensityᵥ fun x => (c.rnDeriv μ x).re) i = { re := ↑(re c) i, im := ↑(im c) i }.re

Tactic:
change (c.re.singularPart μ + μ.withDensityᵥ (c.re.rnDeriv μ)) i = _

Result:
case h.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ↑((re c).singularPart μ + μ.withDensityᵥ ((re c).rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }.re