-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_smul_left (ν μ : Measure α) [IsFiniteMeasure ν]
    [ν.HaveLebesgueDecomposition μ] (r : ℝ≥0) :
    (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = μ.withDensity (↑r • ν.rnDeriv μ)

Tactic:
rw [withDensity_smul _ (measurable_rnDeriv _ _)]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = ↑r • μ.withDensity (ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = ↑r • μ.withDensity (ν.rnDeriv μ)

Tactic:
suffices (r • ν).singularPart μ + withDensity μ (rnDeriv (r • ν) μ)
    = (r • ν).singularPart μ + r • withDensity μ (rnDeriv ν μ) by
  rwa [Measure.add_right_inj] at this

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)

Tactic:
rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
  ← ν.haveLebesgueDecomposition_add μ]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)

Tactic:
simp_rw [ENNReal.smul_def]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = μ.withDensity (↑r • ν.rnDeriv μ)

Proof state:
case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ ∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ⊤

Tactic:
exact (lintegral_rnDeriv_lt_top (r • ν) μ).ne

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ AEMeasurable ((r • ν).rnDeriv μ) μ

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ AEMeasurable (r • ν.rnDeriv μ) μ

case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ ∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
this :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = ↑r • μ.withDensity (ν.rnDeriv μ)

Tactic:
rwa [Measure.add_right_inj] at this

Result:
no goals

Proof state:
case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ AEMeasurable (r • ν.rnDeriv μ) μ

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable.const_smul _

Result:
no goals

Proof state:
case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ AEMeasurable ((r • ν).rnDeriv μ) μ

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Result:
no goals