awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h :
  ∀ (A : Set α) (hA : MeasurableSet A),
    Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
ext1 A hA
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
rw : LE.le (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
⊢ LE.le (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
withDensity_absolutelyContinuous ν (μ.rnDeriv ν) hνinter ▸
        measure_mono inter_subset_right

Premises used: MeasureTheory.Measure.rnDeriv, Eq.rec, MeasureTheory.measure_mono, MeasureTheory.withDensity_absolutelyContinuous, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
⊢ LE.le (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact
      withDensity_absolutelyContinuous ν (μ.rnDeriv ν) hνinter ▸
        measure_mono inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hνrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 := by
    rw [← nonpos_iff_eq_zero]
    exact
      withDensity_absolutelyContinuous ν (μ.rnDeriv ν) hνinter ▸
        measure_mono inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
rw :
  ∀ (hadd : μ = s + ν.withDensity (AEMeasurable.mk f hf)),
    ν.withDensity (AEMeasurable.mk f hf) = ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [withDensity_congr_ae hf.ae_eq_mk] at hadd ⊢

Premises used: MeasureTheory.withDensity_congr_ae, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity (AEMeasurable.mk f hf)
⊢ ν.withDensity (AEMeasurable.mk f hf) = ν.withDensity (μ.rnDeriv ν)

Tactic:
eq_withDensity_rnDeriv hf.measurable_mk hs hadd

Premises used: MeasureTheory.Measure.eq_withDensity_rnDeriv, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity (AEMeasurable.mk f hf)
⊢ ν.withDensity (AEMeasurable.mk f hf) = ν.withDensity (μ.rnDeriv ν)

Tactic:
exact eq_withDensity_rnDeriv hf.measurable_mk hs hadd

Premises used: MeasureTheory.Measure.eq_withDensity_rnDeriv, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
(withDensity_eq_iff_of_sigmaFinite hf (measurable_rnDeriv _ _).aemeasurable).mp
    (eq_withDensity_rnDeriv₀ hf hs hadd)

Premises used: Measurable.aemeasurable, Iff.mp, MeasureTheory.Measure.eq_withDensity_rnDeriv₀, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
eq_rnDeriv₀ hf.aemeasurable hs hadd

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.eq_rnDeriv₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
rw rw₁ : ν.withDensity f = ν.withDensity f
⊢ ν.withDensity f = 0 + ν.withDensity f

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
f : α → ℝ≥0∞
hf : Measurable f
⊢ (ν.withDensity f).rnDeriv ν =ᶠ[ae ν] f

Tactic:
rnDeriv_withDensity₀ ν hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.rnDeriv_withDensity₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator (μ.rnDeriv ν)

Tactic:
(eq_rnDeriv (s := (μ.restrict s).singularPart ν)
    ((measurable_rnDeriv _ _).indicator hs) (mutuallySingular_singularPart _ _) ?_).symm

Premises used: MeasureTheory.Measure.eq_rnDeriv, Measurable.indicator, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
s : Set α
hs : MeasurableSet s
refine : μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))
⊢ (μ.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator (μ.rnDeriv ν)

Tactic:
refine (eq_rnDeriv (s := (μ.restrict s).singularPart ν)
    ((measurable_rnDeriv _ _).indicator hs) (mutuallySingular_singularPart _ _) ?_).symm

Premises used: MeasureTheory.Measure.eq_rnDeriv, Measurable.indicator, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
s : Set α
hs : MeasurableSet s
rw : μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
rw₁ : μ.restrict s = (μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν)
rw₂ : μ.restrict s = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
rw₃ : μ.restrict s = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
rw₄ rw₅ : μ.restrict s = μ.restrict s
⊢ μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))

Tactic:
rw [singularPart_restrict _ _ hs, withDensity_indicator hs, ← restrict_withDensity hs,
    ← Measure.restrict_add, ← μ.haveLebesgueDecomposition_add ν]

Premises used: MeasureTheory.Measure.restrict_add, MeasureTheory.withDensity_indicator, MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.Measure.singularPart_restrict, MeasureTheory.restrict_withDensity
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
s : Set α
hs : MeasurableSet s
rw : (ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1
⊢ (ν.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator 1

Tactic:
rw [← withDensity_indicator_one hs]

Premises used: MeasureTheory.withDensity_indicator_one
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1

Tactic:
rnDeriv_withDensity _ (measurable_one.indicator hs)

Premises used: Measurable.indicator, measurable_one, MeasureTheory.Measure.rnDeriv_withDensity
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1

Tactic:
exact rnDeriv_withDensity _ (measurable_one.indicator hs)

Premises used: Measurable.indicator, measurable_one, MeasureTheory.Measure.rnDeriv_withDensity
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
hf : AEMeasurable ((r • ν).rnDeriv μ) μ
hg : AEMeasurable (r • ν.rnDeriv μ) μ
hfi : ∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ∞
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff]

Premises used: MeasureTheory.withDensity_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ ∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ∞

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

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, HSMul.hSMul, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ ∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ∞

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

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, HSMul.hSMul, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
hg : AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
hfi : ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ∞
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff]

Premises used: MeasureTheory.withDensity_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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 : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ∞

Tactic:
(lintegral_rnDeriv_lt_top ν _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top ν _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : IsFiniteMeasure ν
inst_1 : ν.HaveLebesgueDecomposition μ
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