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
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)
⊢ 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) 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 : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
have inr : ∀
  (this :
    ∀ {μ : Measure X} [IsFiniteMeasure μ] (hfμ : MeasurePreserving f μ μ) (hμν : μ ≪ ν),
      μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν)
  (hμν : ¬μ ≪ ν), μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
Tactic: wlog hμν : μ ≪ ν generalizing μ
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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 ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
have wlog : ∀ {μ : Measure X} [IsFiniteMeasure μ] (hfμ : MeasurePreserving f μ μ) (hμν : μ ≪ ν),
  μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
Tactic: wlog hμν : μ ≪ ν generalizing μ
Cleared hypotheses: inst, hfμ
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (hypothesis)
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μν : ¬μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᶠ[ae ν] μ.rnDeriv ν
have this₁ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Tactic: specialize this (hfμ.withDensity_rnDeriv hfν) (withDensity_absolutelyContinuous _ _)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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 ν
have inr : μ.rnDeriv ν ∘ f =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f
Tactic: refine .trans (.trans ?_ this) (rnDeriv_withDensity ν (measurable_rnDeriv μ ν))
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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 ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f
have inr : μ.rnDeriv ν =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Tactic: apply hfν.quasiMeasurePreserving.ae_eq_comp
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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 ν
have refine : ∀ (c : ENNReal), ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
Tactic: refine .of_forall_eventually_lt_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (hypothesis)
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}
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
have hsm : MeasurableSet s
Tactic: have hsm : MeasurableSet s := measurable_rnDeriv _ _ measurableSet_Iio
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (hypothesis)
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}
hsm : MeasurableSet s
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
have hμ_diff : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
  ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
Tactic: have hμ_diff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s) :=
    measure_diff_symm (hfμ.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
      (hfμ.measure_preimage hsm.nullMeasurableSet) (by finiteness)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (hypothesis)
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}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
have hν_diff : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
  ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
Tactic: have hν_diff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s) :=
    measure_diff_symm (hfν.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
      (hfν.measure_preimage hsm.nullMeasurableSet) (by finiteness)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
have suffices : f ⁻¹' s =ᶠ[ae ν] s
Tactic: suffices f ⁻¹' s =ᵐ[ν] s from this.mem_iff
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ f ⁻¹' s =ᶠ[ae ν] s
have suffices : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
Tactic: suffices ν (f ⁻¹' s \ s) = 0 from (ae_le_set.mpr this).antisymm (ae_le_set.mpr <| hν_diff ▸ this)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
have contrapose! : ∀ (h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)),
  Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
Tactic: contrapose! hμ_diff with h₀
Cleared hypotheses: hμ_diff
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
have h : LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
  ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν < ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν
have hfi : ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤
Tactic: apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
hfi : ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤
⊢ ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν < ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν
have h : ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c
Tactic: apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤
have hfi : Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal) (⊤ : ENNReal)
Tactic: rw [setLIntegral_rnDeriv hμν]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
have μ₁ : ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν < ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν
Tactic: calc
    μ (s \ f ⁻¹' s) = ∫⁻ a in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν := (setLIntegral_rnDeriv hμν _).symm
    _ < ∫⁻ _ in s \ f ⁻¹' s, c ∂ν := by
      apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const
      · rw [setLIntegral_rnDeriv hμν]
        finiteness
      · exact .of_forall fun x hx ↦ hx.1
    _ = ∫⁻ _ in f ⁻¹' s \ s, c ∂ν := by simp [hν_diff]
    _ ≤ ∫⁻ a in f ⁻¹' s \ s, μ.rnDeriv ν a ∂ν :=
      setLIntegral_mono (by fun_prop) (fun x hx ↦ not_lt.mp hx.2)
    _ = μ (f ⁻¹' s \ s) := setLIntegral_rnDeriv hμν _
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
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}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
μ₁ : ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν < ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν
⊢ LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
have μ₂ : ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν = ∫⁻ (x : X) in f ⁻¹' s \ s, c ∂ν
Tactic: calc
    μ (s \ f ⁻¹' s) = ∫⁻ a in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν := (setLIntegral_rnDeriv hμν _).symm
    _ < ∫⁻ _ in s \ f ⁻¹' s, c ∂ν := by
      apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const
      · rw [setLIntegral_rnDeriv hμν]
        finiteness
      · exact .of_forall fun x hx ↦ hx.1
    _ = ∫⁻ _ in f ⁻¹' s \ s, c ∂ν := by simp [hν_diff]
    _ ≤ ∫⁻ a in f ⁻¹' s \ s, μ.rnDeriv ν a ∂ν :=
      setLIntegral_mono (by fun_prop) (fun x hx ↦ not_lt.mp hx.2)
    _ = μ (f ⁻¹' s \ s) := setLIntegral_rnDeriv hμν _
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Basic (goal)
Goal:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s
have rw : IsFixedPt (Set.preimage f)^[n] s
Tactic: rw [Set.preimage_iterate_eq]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • s = s
have refine : s ≤ g • s
Tactic: refine le_antisymm (this hg) ?_
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
have rw : g • g⁻¹ • s
Tactic: rw [← smul_inv_smul g s]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ s ≤ g • s
have conv_lhs : g • g⁻¹ • s ≤ g • s
Tactic: conv_lhs => rw [← smul_inv_smul g s]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g⁻¹ ^ n ^ j = 1
have rw : (g ^ n ^ j)⁻¹ = 1
Tactic: rw [inv_zpow, hg, inv_one]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
rw : (g ^ n ^ j)⁻¹ = 1
⊢ g⁻¹ ^ n ^ j = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1⁻¹ 1
Tactic: rw [inv_zpow, hg, inv_one]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
rw : (g ^ n ^ j)⁻¹ = 1
rw₁ : Eq.{u_1 + 1} (α := G) 1⁻¹ 1
⊢ g⁻¹ ^ n ^ j = 1
have rw₂ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [inv_zpow, hg, inv_one]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • g⁻¹ • s ≤ g • s
have hg₁ : g⁻¹ ^ n ^ j = 1
Tactic: replace hg : g⁻¹ ^ n ^ j = 1 := by rw [inv_zpow, hg, inv_one]
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ g • s = s
have suffices : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
Tactic: suffices ∀ {g' : G} (_ : g' ^ n ^ j = 1), g' • s ⊆ s by
    refine le_antisymm (this hg) ?_
    conv_lhs => rw [← smul_inv_smul g s]
    replace hg : g⁻¹ ^ n ^ j = 1 := by rw [inv_zpow, hg, inv_one]
    simpa only [le_eq_subset, smul_set_subset_smul_set_iff] using this hg
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
have rw : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s ⊆ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
Tactic: rw [(IsFixedPt.preimage_iterate hs j : (zpowGroupHom n)^[j] ⁻¹' s = s).symm]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
⊢ (fun (x : G) ↦ g' • x) y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
have change : (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s
Tactic: change (zpowGroupHom n)^[j] (g' * y) ∈ s
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s
have hg'₁ : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1
Tactic: replace hg' : (zpowGroupHom n)^[j] g' = 1 := by simpa [zpowGroupHom]
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
hg' : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s
have rwa : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
Tactic: rwa [iterate_map_mul, hg', one_mul]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
hg' : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1
rwa : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s
have rwa₁ : 1 * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
Tactic: rwa [iterate_map_mul, hg', one_mul]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Prufer (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
hg' : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1
rwa : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
rwa₁ : 1 * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s
have rwa₂ : (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
Tactic: rwa [iterate_map_mul, hg', one_mul]
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Topology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ IsFixedPt f y
have refine : Tendsto (fun (n : ℕ) ↦ f^[n + 1] x) atTop (𝓝 (f y))
Tactic: refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 ?_) hy
-- Lean 4 proof step from Mathlib.Dynamics.FixedPoints.Topology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun (n : ℕ) ↦ f^[n + 1] x) atTop (𝓝 (f y))
have simp : Tendsto (fun (n : ℕ) ↦ (f ∘ f^[n]) x) atTop (𝓝 (f y))
Tactic: simp only [iterate_succ' f]