-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_mul_rnDeriv' {κ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite κ]
    (hνκ : ν ≪ κ) :
    μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[ν] μ.rnDeriv κ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ

Tactic:
obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ

Tactic:
filter_upwards [hνκ <| Measure.rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) κ,
  hνκ <| Measure.rnDeriv_withDensity_left_of_absolutelyContinuous hνκ h_meas.aemeasurable,
  Measure.rnDeriv_eq_zero_of_mutuallySingular h_sing hνκ] with x hx1 hx2 hx3

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x

Tactic:
rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x

Tactic:
nth_rw 2 [hμν]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x