awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
refine_2₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
rw : AEMeasurable (μ.rnDeriv ν) (ν.restrict s)
⊢ ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

Tactic:
rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]

Premises used: MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∀ (x : α), (μ.rnDeriv ν * f) x = f x * μ.rnDeriv ν x
⊢ ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
x : α
refine_2 : (f * μ.rnDeriv ν) x = f x * μ.rnDeriv ν x
⊢ (μ.rnDeriv ν * f) x = f x * μ.rnDeriv ν x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
x : α
⊢ (f * μ.rnDeriv ν) x = f x * μ.rnDeriv ν x

Tactic:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
ae_restrict_of_ae ?_

Premises used: MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ∞
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
refine ae_restrict_of_ae ?_

Premises used: MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ∞

Tactic:
Measure.rnDeriv_lt_top _ _

Premises used: MeasureTheory.Measure.rnDeriv_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ∞

Tactic:
exact Measure.rnDeriv_lt_top _ _

Premises used: MeasureTheory.Measure.rnDeriv_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

Tactic:
(Measure.measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

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

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
⊢ μ' ≪ ν

Tactic:
have hμ'ν : μ' ≪ ν := withDensity_absolutelyContinuous _ _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
⊢ μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
have h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν :=
    Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
⊢ (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν

Tactic:
rnDeriv_withDensity_withDensity_rnDeriv_left μ ν hf_ne_top

Premises used: MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
⊢ (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν

Tactic:
exact rnDeriv_withDensity_withDensity_rnDeriv_left μ ν hf_ne_top

Premises used: MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
⊢ (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν

Tactic:
have h2 : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν := by
    exact rnDeriv_withDensity_withDensity_rnDeriv_left μ ν hf_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
h2 : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν
h₁ :
  ∀ (x : α) (hx : (μ'.withDensity f).rnDeriv ν x = f x * μ'.rnDeriv ν x) (hx1 : μ'.rnDeriv ν x = μ.rnDeriv ν x)
    (hx2 : (μ'.withDensity f).rnDeriv ν x = (μ.withDensity f).rnDeriv ν x),
    (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x

Tactic:
filter_upwards [h, h1, h2] with x hx hx1 hx2
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
h2 : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν
x : α
hx : (μ'.withDensity f).rnDeriv ν x = f x * μ'.rnDeriv ν x
hx1 : μ'.rnDeriv ν x = μ.rnDeriv ν x
hx2 : (μ'.withDensity f).rnDeriv ν x = (μ.withDensity f).rnDeriv ν x
h₁ : (μ'.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
h₂ : f x * μ'.rnDeriv ν x = f x * μ.rnDeriv ν x
h₃ h₄ : f x * μ.rnDeriv ν x = f x * μ.rnDeriv ν x
⊢ (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x

Tactic:
rw [← hx2, hx, hx1]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ SigmaFinite (ν.withDensity f)

Tactic:
have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
(withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_

Premises used: MeasureTheory.withDensity_absolutelyContinuous', MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
refine : μ.rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
refine (withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_

Premises used: MeasureTheory.withDensity_absolutelyContinuous', MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
(Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm

Premises used: MeasureTheory.Measure.eq_rnDeriv₀, MeasureTheory.Measure.MutuallySingular.zero_left, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
refine_1 : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)
refine_2 : μ = 0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm

Premises used: MeasureTheory.Measure.eq_rnDeriv₀, MeasureTheory.Measure.MutuallySingular.zero_left, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)

Tactic:
(hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul
      (Measure.measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, AEMeasurable.mul, AEMeasurable.mono_ac, MeasureTheory.withDensity_absolutelyContinuous, AEMeasurable.inv, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)

Tactic:
exact (hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul
      (Measure.measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, AEMeasurable.mul, AEMeasurable.mono_ac, MeasureTheory.withDensity_absolutelyContinuous, AEMeasurable.inv, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
refine_2 :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = 0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
rw : ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
| ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
refine_2 :
  Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
refine_2 : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]

Premises used: zero_add, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
refine_2 :
  ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν =
    ∫⁻ (a : α) in s, HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * μ.rnDeriv ν a) a ∂ν
refine_2₁ : ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞
rw : AEMeasurable f (ν.restrict s)
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f

Tactic:
rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]

Premises used: MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
h : ∀ (x : α) (hx1 : f x ≠ 0) (hx2 : f x ≠ ∞), f x * ((f x)⁻¹ * μ.rnDeriv ν x) = μ.rnDeriv ν x
⊢ (fun (a : α) ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
x : α
hx1 : f x ≠ 0
hx2 : f x ≠ ∞
⊢ f x * ((f x)⁻¹ * μ.rnDeriv ν x) = μ.rnDeriv ν x

Tactic:
simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]

Premises used: mul_assoc, ENNReal.mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ (fun (a : α) ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
have : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν := by
        filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
        simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this_1 : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
this : (fun (a : α) ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᶠ[ae ν] μ.rnDeriv ν
refine_2 refine_2₁ : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, f a * ((f a)⁻¹ * μ.rnDeriv ν a) ∂ν

Tactic:
rw [lintegral_congr_ae (ae_restrict_of_ae this)]

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

Tactic:
ae_restrict_of_ae ?_

Premises used: MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
refine_2 : ∀ᵐ (x : α) ∂ν, f x < ∞
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

Tactic:
refine ae_restrict_of_ae ?_

Premises used: MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
x : α
hx : f x ≠ ∞
⊢ f x < ∞

Tactic:
hx.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≠ ∞) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x < ∞) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : f x ≠ ∞), f x < ∞
⊢ ∀ᵐ (x : α) ∂ν, f x < ∞

Tactic:
filter_upwards [hf_ne_top] with x hx using hx.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
hf.restrict

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
exact hf.restrict

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
⊢ μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)

Tactic:
have h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f) :=
    rnDeriv_withDensity_withDensity_rnDeriv_right μ ν hf hf_ne_zero hf_ne_top