mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
⊢ ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y

Tactic:
·

Goal state after:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
⊢ ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_3.inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X), (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x ≠ y → x < y → False
hlt : ¬x < y
⊢ False

pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
⊢ False

Tactic:
·

Goal state after:
case refine_3.inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X), (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x ≠ y → x < y → False
hlt : ¬x < y
⊢ False
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)

pp: case e'_7
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict s

Tactic:
·

Goal state after:
case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : 0 ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 0}
⊢ Ergodic f μ

pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ

Tactic:
·

Goal state after:
case inl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : 0 ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 0}
⊢ Ergodic f μ
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case e'_7
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict s

Tactic:
·

Goal state after:
case e'_7
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict s
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ

Tactic:
·

Goal state after:
case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this : ∀ {μ : Measure X} [IsFiniteMeasure μ], MeasurePreserving f μ μ → μ ≪ ν → μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν
hμν : ¬μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

Tactic:
·

Goal state after:
case inr
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this : ∀ {μ : Measure X} [IsFiniteMeasure μ], MeasurePreserving f μ μ → μ ≪ ν → μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν
hμν : ¬μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ MeasurePreserving f (μ.restrict s) (μ.restrict s)

pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ (c • μ[|s]) univ = c

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ MeasurePreserving f (μ.restrict s) (μ.restrict s)
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ (c • μ[|s]) univ = c

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ (c • μ[|s]) univ = c
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case hfi
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤

pp: case h
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c

Tactic:
·

Goal state after:
case hfi
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x

Tactic:
refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_
  filter_upwards [Measure.rnDeriv_pos (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)),
    (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).ae_le
    (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ))] with x hx hx2
  rwa [← hx2]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case h
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c

Tactic:
·

Goal state after:
case h
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
⊢ μ s ≠ 0 ∧ μ sᶜ ≠ 0

Tactic:
by
      simpa [eventuallyConst_set, ae_iff, and_comm] using! H

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
hf : HasCompactFixedSupport f
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
x✝ : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ HasCompactFixedSupport f

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
hf : HasCompactFixedSupport f
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
x✝ : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ HasCompactFixedSupport f

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
x✝ : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ HasCompactFixedSupport f
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ s / c + μ sᶜ / c = 1

pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s / c) • c • μ[|s] + (μ sᶜ / c) • c • μ[|sᶜ] = μ

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ s / c + μ sᶜ / c = 1
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → X
inst✝ : R1Space X
⊢ HasCompactFixedSupport f ↔ ∃ K, IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

Tactic:
rw [HasCompactFixedSupport_iff']

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → X
inst✝ : R1Space X
⊢ (∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K) ↔ ∃ K, IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s / c) • c • μ[|s] + (μ sᶜ / c) • c • μ[|sᶜ] = μ

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s / c) • c • μ[|s] + (μ sᶜ / c) • c • μ[|sᶜ] = μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (fun x ↦ f x * μ.rnDeriv ν x) ν

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (fun x ↦ f x * μ.rnDeriv ν x) ν
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inl
X : Type u_1
m : MeasurableSpace X
f : X → X
c : ℝ≥0∞
inst✝¹ : IsFiniteMeasure 0
hμ : Ergodic f 0
inst✝ : IsFiniteMeasure (c • 0)
hfν : MeasurePreserving f (c • 0) (c • 0)
hνμ : c • 0 ≪ 0
huniv : (c • 0) univ = 0 univ
⊢ c • 0 = 0

pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst✝ : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : (c • μ) univ = μ univ
hμ₀ : μ ≠ 0
⊢ c • μ = μ

Tactic:
·

Goal state after:
case inl
X : Type u_1
m : MeasurableSpace X
f : X → X
c : ℝ≥0∞
inst✝¹ : IsFiniteMeasure 0
hμ : Ergodic f 0
inst✝ : IsFiniteMeasure (c • 0)
hfν : MeasurePreserving f (c • 0) (c • 0)
hνμ : c • 0 ≪ 0
huniv : (c • 0) univ = 0 univ
⊢ c • 0 = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst✝ : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : (c • μ) univ = μ univ
hμ₀ : μ ≠ 0
⊢ c • μ = μ

Tactic:
·

Goal state after:
case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst✝ : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : (c • μ) univ = μ univ
hμ₀ : μ ≠ 0
⊢ c • μ = μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ AEMeasurable (fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ AEMeasurable (fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f * fun a ↦ (f a)⁻¹ * μ.rnDeriv ν a) a ∂ν

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f * fun a ↦ (f a)⁻¹ * μ.rnDeriv ν a) a ∂ν