awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  (μ.singularPart ν : (a : Set X) → ENNReal) s =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have rw₁ : (μ.singularPart ν : (a : Set X) → ENNReal) s =
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: rw [← measure_add_measure_compl hsm, hμs, add_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  (μ.singularPart ν : (a : Set X) → ENNReal) s =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal)
rw₁ :
  (μ.singularPart ν : (a : Set X) → ENNReal) s =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have rw₂ : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
  ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [← measure_add_measure_compl hsm, hμs, add_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have ν₁ : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
  ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
Tactic: calc
      μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) := by
        rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
      _ = μ.singularPart ν s := by
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = μ.singularPart ν univ := by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
ν₁ :
  Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have ν₂ : Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
  ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
Tactic: calc
      μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) := by
        rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
      _ = μ.singularPart ν s := by
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = μ.singularPart ν univ := by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
ν₁ :
  Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
ν₂ :
  Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have ν₃ : Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
  ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
Tactic: calc
      μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) := by
        rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
      _ = μ.singularPart ν s := by
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = μ.singularPart ν univ := by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
ν₁ :
  Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
ν₂ :
  Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
ν₃ :
  Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have ν₄ : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
  ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
Tactic: calc
      μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) := by
        rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
      _ = μ.singularPart ν s := by
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = μ.singularPart ν univ := by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν))
have map_eq : map f (ν.withDensity (μ.rnDeriv ν)) = ν.withDensity (μ.rnDeriv ν)
Tactic: use hfμ.measurable
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ map f (ν.withDensity (μ.rnDeriv ν)) = ν.withDensity (μ.rnDeriv ν)
have map_eq : ∀ (s : Set X) (hs : MeasurableSet s),
  Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq : HAdd.hAdd (α := ENNReal) (β := ENNReal)
    (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
map_eq :
  HAdd.hAdd (α := ENNReal) (β := ENNReal)
      (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq₁ : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
map_eq :
  HAdd.hAdd (α := ENNReal) (β := ENNReal)
      (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq₂ : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
  (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
map_eq :
  HAdd.hAdd (α := ENNReal) (β := ENNReal)
      (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₂ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq₃ : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
  (μ : (a : Set X) → ENNReal) s
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
map_eq :
  HAdd.hAdd (α := ENNReal) (β := ENNReal)
      (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₂ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s
map_eq₃ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ : (a : Set X) → ENNReal) s
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq₄ : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) =
  (μ : (a : Set X) → ENNReal) s
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
map_eq :
  HAdd.hAdd (α := ENNReal) (β := ENNReal)
      (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₂ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s
map_eq₃ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ : (a : Set X) → ENNReal) s
map_eq₄ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) =
    (μ : (a : Set X) → ENNReal) s
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq₅ : Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
  ((μ : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
map_eq :
  HAdd.hAdd (α := ENNReal) (β := ENNReal)
      (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
map_eq₂ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s
map_eq₃ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ : (a : Set X) → ENNReal) s
map_eq₄ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) =
    (μ : (a : Set X) → ENNReal) s
map_eq₅ :
  Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) (((map f (ν.withDensity (μ.rnDeriv ν)) : Measure X) : (a : Set X) → ENNReal) s : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
have map_eq₆ : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]