-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
/-- Auxiliary lemma for `rnDeriv_withDensity_left`. -/
lemma rnDeriv_withDensity_withDensity_rnDeriv_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
    (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : SigmaFinite ((μ.singularPart ν).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Tactic:
have : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f) :=
  SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.withDensity_rnDeriv_le _ _) hf_ne_top)

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this✝ : SigmaFinite ((μ.singularPart ν).withDensity f)
this : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν

Tactic:
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Tactic:
have : SigmaFinite ((μ.singularPart ν).withDensity f) :=
  SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.singularPart_le _ _) hf_ne_top)

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : SigmaFinite ((μ.singularPart ν).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this✝ : SigmaFinite ((μ.singularPart ν).withDensity f)
this : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Tactic:
exact (rnDeriv_add_of_mutuallySingular _ _ _ (mutuallySingular_singularPart μ ν).withDensity).symm

Result:
no goals