awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ MeasurePreserving.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) μ) μ

Tactic:
(e.measurable.measurePreserving μ).symm _

Premises used: MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.measurable
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
rcases :
  ∀ (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)),
    MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)
⊢ MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)

Tactic:
rcases (μ.mutuallySingular_singularPart ν).symm with ⟨s, hsm, hνs, hμs⟩

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
⊢ MeasurePreserving f (μ.restrict (f ⁻¹' s)) (μ.restrict s)

Tactic:
hfμ.restrict_preimage hsm

Premises used: MeasureTheory.MeasurePreserving.restrict_preimage
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
h : μ.singularPart ν = μ.restrict (f ⁻¹' s)
h₁ : μ.singularPart ν = μ.restrict s
⊢ MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)

Tactic:
convert! hfμ.restrict_preimage hsm using 1

Premises used: MeasureTheory.MeasurePreserving.restrict_preimage
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)

Tactic:
singularPart_eq_restrict ?_ (hfν.preimage_null hνs)

Premises used: MeasureTheory.MeasurePreserving.preimage_null, MeasureTheory.Measure.singularPart_eq_restrict
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
h : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s)ᶜ : ENNReal) (0 : ENNReal)
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)

Tactic:
refine singularPart_eq_restrict ?_ (hfν.preimage_null hνs)

Premises used: MeasureTheory.MeasurePreserving.preimage_null, MeasureTheory.Measure.singularPart_eq_restrict
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
h :
  Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s)ᶜ : ENNReal) (0 : ENNReal)

Tactic:
rw [← mem_ae_iff, ← Filter.eventuallyEq_univ,
      ae_eq_univ_iff_measure_eq (hfμ.measurable hsm).nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.ae_eq_univ_iff_measure_eq, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.mem_ae_iff, Filter.eventuallyEq_univ
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) (0 : ENNReal)

Tactic:
rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
hνs₁ : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)

Tactic:
rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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) (f ⁻¹' s) : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
rw₁ :
  (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
rw₂ rw₃ :
  Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)

Tactic:
rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]

Premises used: MeasureTheory.Measure.add_apply, zero_add, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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 : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
rw₁ rw₂ : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)

Tactic:
rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.rnDeriv_add_singularPart, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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 :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ.singularPart ν : (a : Set X) → ENNReal) s
rw₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ.singularPart ν : (a : Set X) → ENNReal) s
rw₂ rw₃ :
  Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.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)

Tactic:
rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]

Premises used: MeasureTheory.Measure.add_apply, zero_add, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
rw₂ rw₃ :
  Eq (α := 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)

Tactic:
rw [← measure_add_measure_compl hsm, hμs, add_zero]

Premises used: MeasureTheory.measure_add_measure_compl, add_zero
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' 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]

Premises used: MeasureTheory.Measure.withDensity, Set.univ, MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.singularPart, Set.preimage, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
⊢ μ.singularPart ν = μ.restrict s

Tactic:
singularPart_eq_restrict hμs hνs

Premises used: MeasureTheory.Measure.singularPart_eq_restrict
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
⊢ μ.singularPart ν = μ.restrict s

Tactic:
exact singularPart_eq_restrict hμs hνs

Premises used: MeasureTheory.Measure.singularPart_eq_restrict
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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_eq : map f (ν.withDensity (μ.rnDeriv ν)) = ν.withDensity (μ.rnDeriv ν)
⊢ MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν))

Tactic:
use hfμ.measurable

Premises used: MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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_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)
⊢ map f (ν.withDensity (μ.rnDeriv ν)) = ν.withDensity (μ.rnDeriv ν)

Tactic:
ext s hs
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
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)
map_eq₆ : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
map_eq₇ map_eq₈ : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) 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)

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]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.rnDeriv_add_singularPart, MeasureTheory.measure_ne_top, ENNReal.add_left_inj, MeasureTheory.Measure.add_apply, MeasureTheory.Measure.singularPart, MeasureTheory.MeasurePreserving.singularPart, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
inr :
  ∀
    (this :
      ∀ {μ : Measure X} [IsFiniteMeasure μ] (hfμ : MeasurePreserving f μ μ) (hμν : μ ≪ ν),
        μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν)
    (hμν : ¬μ ≪ ν), μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
wlog :
  ∀ {μ : Measure X} [IsFiniteMeasure μ] (hfμ : MeasurePreserving f μ μ) (hμν : μ ≪ ν),
    μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
wlog hμν : μ ≪ ν generalizing μ
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this :
  ∀ {μ : Measure X} [IsFiniteMeasure μ] (hfμ : MeasurePreserving f μ μ) (hμν : μ ≪ ν),
    μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
hμν : ¬μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
specialize this (hfμ.withDensity_rnDeriv hfν) (withDensity_absolutelyContinuous _ _)

Premises used: MeasureTheory.MeasurePreserving.withDensity_rnDeriv, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
hμν : ¬μ ≪ ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
.trans (.trans ?_ this) (rnDeriv_withDensity ν (measurable_rnDeriv μ ν))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
hμν : ¬μ ≪ ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
inr : μ.rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
refine .trans (.trans ?_ this) (rnDeriv_withDensity ν (measurable_rnDeriv μ ν))
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
hμν : ¬μ ≪ ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
inr : μ.rnDeriv ν =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f

Tactic:
apply hfν.quasiMeasurePreserving.ae_eq_comp

Premises used: MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
hμν : ¬μ ≪ ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
(rnDeriv_withDensity ν (measurable_rnDeriv μ ν)).symm

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
hμν : ¬μ ≪ ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
exact (rnDeriv_withDensity ν (measurable_rnDeriv μ ν)).symm

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.Measure.measurable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
.of_forall_eventually_lt_iff fun c ↦ ?_

Premises used: Filter.EventuallyEq.of_forall_eventually_lt_iff
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
refine : ∀ (c : ENNReal), ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
refine .of_forall_eventually_lt_iff fun c ↦ ?_
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
⊢ MeasurableSet s

Tactic:
have hsm : MeasurableSet s := measurable_rnDeriv _ _ measurableSet_Iio