awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = μ.real s
⊢ μ.real t = μ.real s
have rw₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [measureReal_def, measureReal_def, measure_toMeasurable s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = μ.real s
rw₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
⊢ μ.real t = μ.real s
have rw₂ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [measureReal_def, measureReal_def, measure_toMeasurable s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
have calc : LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)
Tactic: calc ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν
    ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν := by
        refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
        · exact integrableOn_toReal_rnDeriv hμt
        · exact ae_of_all _ (by simp)
  _ = (withDensity ν (rnDeriv μ ν)).real t := setIntegral_toReal_rnDeriv_eq_withDensity' ht_m
  _ ≤ μ.real t := by
        simp only [measureReal_def]
        gcongr
        apply withDensity_rnDeriv_le
  _ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
calc : LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
have calc₁ : (ν.withDensity (μ.rnDeriv ν)).real t ≤ μ.real t
Tactic: calc ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν
    ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν := by
        refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
        · exact integrableOn_toReal_rnDeriv hμt
        · exact ae_of_all _ (by simp)
  _ = (withDensity ν (rnDeriv μ ν)).real t := setIntegral_toReal_rnDeriv_eq_withDensity' ht_m
  _ ≤ μ.real t := by
        simp only [measureReal_def]
        gcongr
        apply withDensity_rnDeriv_le
  _ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
calc : LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)
calc₁ : (ν.withDensity (μ.rnDeriv ν)).real t ≤ μ.real t
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
have calc₂ : μ.real t = μ.real s
Tactic: calc ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν
    ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν := by
        refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
        · exact integrableOn_toReal_rnDeriv hμt
        · exact ae_of_all _ (by simp)
  _ = (withDensity ν (rnDeriv μ ν)).real t := setIntegral_toReal_rnDeriv_eq_withDensity' ht_m
  _ ≤ μ.real t := by
        simp only [measureReal_def]
        gcongr
        apply withDensity_rnDeriv_le
  _ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
have rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
Tactic: rw [setIntegral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν,
    measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
have rw₁ : μ.real s = μ.real s
Tactic: rw [setIntegral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν,
    measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
rw₁ : μ.real s = μ.real s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
have rw₂ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [setIntegral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν,
    measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
have rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
Tactic: rw [setIntegral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
have rw₁ : μ.real s = μ.real s
Tactic: rw [setIntegral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ
have rw : ∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ
Tactic: rw [← setIntegral_univ, setIntegral_toReal_rnDeriv hμν Set.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
rw : ∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ
have rw₁ : μ.real Set.univ = μ.real Set.univ
Tactic: rw [← setIntegral_univ, setIntegral_toReal_rnDeriv hμν Set.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₁ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₂ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₂ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₃ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((μ - μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₂ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
rw₃ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((μ - μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₄ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) Set.univ)
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₂ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
rw₃ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((μ - μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₄ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) Set.univ)
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₅ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real Set.univ
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₂ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
rw₃ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((μ - μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₄ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) Set.univ)
rw₅ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real Set.univ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₆ : Eq (α := ℝ) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν)
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₂ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
rw₃ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((μ - μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₄ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) Set.univ)
rw₅ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real Set.univ
rw₆ : Eq (α := ℝ) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν)
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
have rw₇ : Eq (α := ℝ) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν)
Tactic: rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
have refine_1 : AEMeasurable (μ.rnDeriv ν) κ
Tactic: refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
refine_1 : AEMeasurable (μ.rnDeriv ν) κ
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
have refine_2 : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞
Tactic: refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
refine_1 : AEMeasurable (μ.rnDeriv ν) κ
refine_2 : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
have refine_3 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
Tactic: refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
have refine_3 : μ.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
Tactic: rw [Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ
have h_meas : Measurable (μ.rnDeriv ν)
Tactic: obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ
have h_sing : μ.singularPart ν ⟂ₘ ν
Tactic: obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ
have hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ
have h : ∀ (x : α)
  (hx1 :
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
      ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x)
  (hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x)
  (hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x), (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x
Tactic: filter_upwards [hνκ <| Measure.rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) κ,
    hνκ <| Measure.rnDeriv_withDensity_left_of_absolutelyContinuous hνκ h_meas.aemeasurable,
    Measure.rnDeriv_eq_zero_of_mutuallySingular h_sing hνκ] with x hx1 hx2 hx3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x
have h : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
Tactic: nth_rw 2 [hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]