awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
⊢ sum ξ ⟂ₘ ν

Tactic:
have hξ : .sum ξ ⟂ₘ ν := by
    refine MutuallySingular.sum_left.2 fun n ↦ ?_
    rw [← ν.restrict_add_restrict_compl (hsm n)]
    refine (mutuallySingular_singularPart ..).add_right (.singularPart ?_ _)
    refine ⟨(s n)ᶜ, (hsm n).compl, ?_⟩
    simp [hsm]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
rw : (sum ξ + sum fun (n : ℕ) ↦ ν.withDensity (f n)) = sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n))
    (sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n))
⊢ sum ξ + ν.withDensity (∑' (n : ℕ), f n) = sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)

Tactic:
rw [withDensity_tsum hfm, Measure.sum_add_sum]

Premises used: MeasureTheory.withDensity_tsum, MeasureTheory.Measure.sum_add_sum
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
simp_rw :
  Eq.{u_1 + 1} (α := Measure α)
    (sum fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n)) + ν.withDensity (f n))
    (sum fun (n : ℕ) ↦ μ.restrict (s n))
simp_rw₁ :
  Eq.{u_1 + 1} (α := Measure α)
    (sum fun (n : ℕ) ↦
      (μ.restrict (s n)).singularPart (ν.restrict (s n)) +
        ν.withDensity ((s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))))
    (sum fun (n : ℕ) ↦ μ.restrict (s n))
simp_rw₂ :
  Eq.{u_1 + 1} (α := Measure α)
    (sum fun (n : ℕ) ↦
      (μ.restrict (s n)).singularPart (ν.restrict (s n)) +
        (ν.restrict (s n)).withDensity ((μ.restrict (s n)).rnDeriv (ν.restrict (s n))))
    (sum fun (n : ℕ) ↦ μ.restrict (s n))
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)) (sum fun (n : ℕ) ↦ μ.restrict (s n))

Tactic:
simp_rw [ξ, f, withDensity_indicator (hsm _), singularPart_add_rnDeriv]

Premises used: MeasureTheory.withDensity_indicator, MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
⊢ sum ξ + ν.withDensity (∑' (n : ℕ), f n) = μ

Tactic:
have hadd : .sum ξ + ν.withDensity (∑' n, f n) = μ := calc
    .sum ξ + ν.withDensity (∑' n, f n) = .sum fun n ↦ ξ n + ν.withDensity (f n) := by
      rw [withDensity_tsum hfm, Measure.sum_add_sum]
    _ = .sum fun n ↦ .restrict μ (s n) := by
      simp_rw [ξ, f, withDensity_indicator (hsm _), singularPart_add_rnDeriv]
    _ = μ := sum_restrict_disjointed_spanningSets ..
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
hadd : sum ξ + ν.withDensity (∑' (n : ℕ), f n) = μ
⊢ Measurable (α := α) (β := ℝ≥0∞) (sum ξ, ∑' (n : ℕ), f n).2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
hadd : sum ξ + ν.withDensity (∑' (n : ℕ), f n) = μ
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
exact ⟨⟨(.sum ξ, ∑' n, f n), by fun_prop, hξ, hadd.symm⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
hf : AEMeasurable ((r • ν).rnDeriv μ) μ
hg : AEMeasurable (r • ν.rnDeriv μ) μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite]

Premises used: MeasureTheory.withDensity_eq_iff_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = μ.withDensity ((↑r : ℝ≥0∞) • ν.rnDeriv μ)

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

Premises used: MeasureTheory.withDensity_smul, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
this :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : μ.withDensity ((r • ν).rnDeriv μ) = r • μ.withDensity (ν.rnDeriv μ)),
    μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)

Tactic:
rwa [Measure.add_right_inj] at this

Premises used: MeasureTheory.Measure.add_right_inj
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
suffices :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)

Tactic:
suffices (r • ν).singularPart μ + withDensity μ (rnDeriv (r • ν) μ)
        = (r • ν).singularPart μ + r • withDensity μ (rnDeriv ν μ) by
      rwa [Measure.add_right_inj] at this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₂ : r • ν = r • (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ))
rw₃ rw₄ : r • ν = r • ν
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)

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

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, HSMul.hSMul, smul_add, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ AEMeasurable ((r • ν).rnDeriv μ) μ

Tactic:
(measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ AEMeasurable ((r • ν).rnDeriv μ) μ

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ AEMeasurable (r • ν.rnDeriv μ) μ

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

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ AEMeasurable (r • ν.rnDeriv μ) μ

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

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ

Tactic:
have h : (r.toNNReal • ν).rnDeriv μ =ᵐ[μ] r.toNNReal • ν.rnDeriv μ :=
    rnDeriv_smul_left' ν μ r.toNNReal
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ ∞
h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
simpa [ENNReal.smul_def, ENNReal.coe_toNNReal hr] using h

Premises used: ENNReal.coe_toNNReal, ENNReal.smul_def
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
(absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le
    (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)

Premises used: Iff.mpr, Filter.Eventually, Filter.EventuallyEq, ENNReal.coe_ne_zero, MeasureTheory.Measure.absolutelyContinuous_smul, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
refine : ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
refine (absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le
    (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)

Premises used: Iff.mpr, ENNReal.coe_ne_zero, MeasureTheory.Measure.absolutelyContinuous_smul, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
hg : AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite]

Premises used: MeasureTheory.withDensity_eq_iff_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
rw :
  ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    ((↑r : ℝ≥0∞) • μ).withDensity ((↑r⁻¹ : ℝ≥0∞) • ν.rnDeriv μ)

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

Premises used: MeasureTheory.withDensity_smul, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (r • μ).withDensity (ν.rnDeriv (r • μ)) = r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)),
    ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
      (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

Premises used: MeasureTheory.Measure.add_right_inj
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
suffices :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)

Tactic:
suffices ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ))
        = ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ) by
      rwa [add_right_inj] at this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
rw : ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
⊢ ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)

Tactic:
rw [← ν.haveLebesgueDecomposition_add (r • μ), singularPart_smul_right _ _ _ hr,
      ENNReal.smul_def r, withDensity_smul_measure, ← ENNReal.smul_def, ← smul_assoc,
      smul_eq_mul, inv_mul_cancel₀ hr, one_smul]

Premises used: ENNReal.smul_def, smul_assoc, MeasureTheory.Measure.haveLebesgueDecomposition_add, one_smul, HSMul.hSMul, MeasureTheory.withDensity_smul_measure, smul_eq_mul, MeasureTheory.Measure.singularPart_smul_right, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Tactic:
ν.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Tactic:
exact ν.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

Tactic:
(measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

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

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

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

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
rnDeriv_smul_right' ν μ ?_

Premises used: MeasureTheory.Measure.rnDeriv_smul_right'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
refine : r.toNNReal ≠ 0
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
refine rnDeriv_smul_right' ν μ ?_

Premises used: MeasureTheory.Measure.rnDeriv_smul_right'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
rw : ¬(r = 0 ∨ r = ∞)
⊢ r.toNNReal ≠ 0

Tactic:
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]

Premises used: ENNReal.toNNReal_eq_zero_iff, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ¬(r = 0 ∨ r = ∞)

Tactic:
simp [hr, hr_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
have h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ := by
    refine rnDeriv_smul_right' ν μ ?_
    rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
    simp [hr, hr_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
rwa :
  ∀ (h : ν.rnDeriv ((↑r.toNNReal : ℝ≥0∞) • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ),
    ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₁ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₂ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹.toNNReal • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₃ :
  ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] (↑r⁻¹.toNNReal : ℝ≥0∞) • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
    ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h

Premises used: ENNReal.coe_toNNReal, Iff.mpr, ENNReal.smul_def, ENNReal.inv_ne_top, ENNReal.toNNReal_inv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
hf : AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
hg : AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite]

Premises used: MeasureTheory.withDensity_eq_iff_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)),
    μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

Premises used: MeasureTheory.Measure.add_right_inj
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
suffices :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

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