-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma _root_.MeasurableEmbedding.singularPart_map (hf : MeasurableEmbedding f)
    (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
    (μ.map f).singularPart (ν.map f) = (μ.singularPart ν).map f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ map f (μ.singularPart ν) ⟂ₘ map f ν

Tactic:
exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Tactic:
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Tactic:
rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)

Tactic:
refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ map f (μ.singularPart ν) ⟂ₘ map f ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)

Tactic:
have h_add : μ.map f = (μ.singularPart ν).map f
    + (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) := by
  conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
  rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)