awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
have h₁ : (μ'.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
Tactic: rw [← hx2, hx, hx1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
have h₂ : f x * μ'.rnDeriv ν x = f x * μ.rnDeriv ν x
Tactic: rw [← hx2, hx, hx1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
have h₃ : f x * μ.rnDeriv ν x = f x * μ.rnDeriv ν x
Tactic: rw [← hx2, hx, hx1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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 ≠ ∞
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have this : SigmaFinite (ν.withDensity f)
Tactic: have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
have refine : μ.rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
Tactic: refine (withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
have refine_1 : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)
Tactic: refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have refine_2 : μ = 0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
Tactic: refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)
⊢ μ = 0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
| ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + (ν.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine_2 : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f
Tactic: rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f
have refine_2 : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν =
  ∫⁻ (a : α) in s, HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * μ.rnDeriv ν a) a ∂ν
Tactic: rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 ∂ν
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f
have refine_2₁ : ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞
Tactic: rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 < ∞
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f
have rw : AEMeasurable f (ν.restrict s)
Tactic: rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 ν
have h : ∀ (x : α) (hx1 : f x ≠ 0) (hx2 : f x ≠ ∞), f x * ((f x)⁻¹ * μ.rnDeriv ν x) = μ.rnDeriv ν x
Tactic: filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, f a * ((f a)⁻¹ * μ.rnDeriv ν a) ∂ν
have this₁ : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 ν
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, f a * ((f a)⁻¹ * μ.rnDeriv ν a) ∂ν
have refine_2 : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν
Tactic: rw [lintegral_congr_ae (ae_restrict_of_ae this)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 < ∞
have refine_2 : ∀ᵐ (x : α) ∂ν, f x < ∞
Tactic: refine ae_restrict_of_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 : α) ∂ν, f x < ∞
have 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
Tactic: filter_upwards [hf_ne_top] with x hx using hx.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ ∀ᵐ (x : α) ∂ν, f x < ∞
have h₁ : ∀ (a : α), f a ≠ ∞ → f a < ∞
Tactic: filter_upwards [hf_ne_top] with x hx using hx.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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 ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have h₁ : μ'.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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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 ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
Tactic: have h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν :=
    (Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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 ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have hμ' : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
  (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
Tactic: have hμ' := rnDeriv_withDensity_right_of_absolutelyContinuous
    (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) hf hf_ne_zero hf_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x
have h : ∀ (x : α) (hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x) (hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x)
  (hx_eq :
    (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x),
  μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
Tactic: filter_upwards [h₁, h₂, hμ'] with x hx₁ hx₂ hx_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
have h : μ'.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
Tactic: rw [← hx₁, hx₂, hx_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
h : μ'.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
h₃ : μ'.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ'.rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
have h₄ : (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x = (f x)⁻¹ * μ'.rnDeriv ν x
Tactic: rw [← hx₁, hx₂, hx_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
⊢ μ.rnDeriv ν' =ᶠ[ae ν] 0
have ht : MeasurableSet t
Tactic: have ht : MeasurableSet t := h.measurableSet_nullSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᶠ[ae ν] 0
have refine : ∀ᵐ (x : α) ∂ν.restrict t, μ.rnDeriv ν' x = 0 x
Tactic: refine ae_of_ae_restrict_of_ae_restrict_compl t ?_ (by simp [t])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
have h₁ : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
Tactic: have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') :=
      hνν'.ae_le (rnDeriv_restrict μ ν' ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
have rw : ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
have h₁ : ∀ (x : α) (hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x) (hxt : x ∈ t),
  μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
Tactic: filter_upwards [h] with x hx hxt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
⊢ μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
have h₁ : μ.rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
Tactic: rw [hx, Set.indicator_of_mem hxt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
h₁ : μ.rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
⊢ μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
have h₂ : μ.rnDeriv ν' x = μ.rnDeriv ν' x
Tactic: rw [hx, Set.indicator_of_mem hxt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0
have this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
Tactic: have : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν' := by
    have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') :=
      hνν'.ae_le (rnDeriv_restrict μ ν' ht)
    rw [Filter.EventuallyEq, ae_restrict_iff' ht]
    filter_upwards [h] with x hx hxt
    rw [hx, Set.indicator_of_mem hxt]