α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
⊢ singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ) = SignedMeasure.toComplexMeasure (↑re c) (↑im c)
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
⊢ singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ) = c
conv_rhs => rw [← c.toComplexMeasure_to_signedMeasure]
case h
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
⊢ MeasurableSet i →
    ↑(singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ)) i = ↑(SignedMeasure.toComplexMeasure (↑re c) (↑im c)) i
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
⊢ singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ) = SignedMeasure.toComplexMeasure (↑re c) (↑im c)
ext i : 1
case h
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ)) i = ↑(SignedMeasure.toComplexMeasure (↑re c) (↑im c)) i
case h
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
⊢ MeasurableSet i →
    ↑(singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ)) i = ↑(SignedMeasure.toComplexMeasure (↑re c) (↑im c)) i
intro hi
case h
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(singularPart c μ) i + ↑(Measure.withDensityᵥ μ (rnDeriv c μ)) i = { re := ↑(↑re c) i, im := ↑(↑im c) i }
case h
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(singularPart c μ + Measure.withDensityᵥ μ (rnDeriv c μ)) i = ↑(SignedMeasure.toComplexMeasure (↑re c) (↑im c)) i
rw [VectorMeasure.add_apply, SignedMeasure.toComplexMeasure_apply]
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ (↑(singularPart c μ) i + ↑(Measure.withDensityᵥ μ (rnDeriv c μ)) i).re = { re := ↑(↑re c) i, im := ↑(↑im c) i }.re

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

α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun a => (rnDeriv c μ a).re
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ (↑(singularPart c μ) i + ↑(Measure.withDensityᵥ μ (rnDeriv c μ)) i).re = { re := ↑(↑re c) i, im := ↑(↑im c) i }.re
rw [Complex.add_re, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← IsROrC.re_eq_complex_re,
  ← integral_re (c.integrable_rnDeriv μ).integrableOn, IsROrC.re_eq_complex_re,
  ← withDensityᵥ_apply _ hi]
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(SignedMeasure.singularPart (↑re c) μ + Measure.withDensityᵥ μ (SignedMeasure.rnDeriv (↑re c) μ)) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.re
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ (↑(singularPart c μ) i).re + ↑(Measure.withDensityᵥ μ fun a => (rnDeriv c μ a).re) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.re
change (c.re.singularPart μ + μ.withDensityᵥ (c.re.rnDeriv μ)) i = _
no goals
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(SignedMeasure.singularPart (↑re c) μ + Measure.withDensityᵥ μ (SignedMeasure.rnDeriv (↑re c) μ)) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.re
rw [c.re.singularPart_add_withDensity_rnDeriv_eq μ]
no goals
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun a => (rnDeriv c μ a).re
exact SignedMeasure.integrable_rnDeriv _ _
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ (↑(singularPart c μ) i).im + ↑(Measure.withDensityᵥ μ fun a => (rnDeriv c μ a).im) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.im

α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun a => (rnDeriv c μ a).im
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ (↑(singularPart c μ) i + ↑(Measure.withDensityᵥ μ (rnDeriv c μ)) i).im = { re := ↑(↑re c) i, im := ↑(↑im c) i }.im
rw [Complex.add_im, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← IsROrC.im_eq_complex_im,
  ← integral_im (c.integrable_rnDeriv μ).integrableOn, IsROrC.im_eq_complex_im,
  ← withDensityᵥ_apply _ hi]
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(SignedMeasure.singularPart (↑im c) μ + Measure.withDensityᵥ μ (SignedMeasure.rnDeriv (↑im c) μ)) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.im
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ (↑(singularPart c μ) i).im + ↑(Measure.withDensityᵥ μ fun a => (rnDeriv c μ a).im) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.im
change (c.im.singularPart μ + μ.withDensityᵥ (c.im.rnDeriv μ)) i = _
no goals
case h.a
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ ↑(SignedMeasure.singularPart (↑im c) μ + Measure.withDensityᵥ μ (SignedMeasure.rnDeriv (↑im c) μ)) i =
    { re := ↑(↑re c) i, im := ↑(↑im c) i }.im
rw [c.im.singularPart_add_withDensity_rnDeriv_eq μ]
no goals
α : Type u_1
β : Type ?u.660548
m : MeasurableSpace α
μ ν : Measure α
c : ComplexMeasure α
inst✝ : HaveLebesgueDecomposition c μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun a => (rnDeriv c μ a).im
exact SignedMeasure.integrable_rnDeriv _ _