awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ c • μ[|s] = μ

Tactic:
have hcond : c • μ[|s] = μ := by
      apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')
      refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
      · rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
      · simp [ProbabilityTheory.cond, smul_smul, ← mul_assoc, ENNReal.div_mul_cancel,
          ENNReal.mul_inv_cancel, *]
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hcond : c • μ[|s] = μ
⊢ Ne (α := ℝ≥0∞) ((c • μ[|s] : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← hcond] at hs'
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hcond : c • μ[|s] = μ
hs'₁ : Ne (α := ℝ≥0∞) ((c • μ[|s] : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ c • μ[|s] = μ

Tactic:
rw [← hcond] at hs'
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((c • μ[|s] : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hcond : c • μ[|s] = μ
⊢ False

Tactic:
simp [ProbabilityTheory.cond_apply, hsm] at hs'

Premises used: ProbabilityTheory.cond_apply
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}) μ
⊢ Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞
      {ν : Measure X | MeasurePreserving f ν ν ∧ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)})
    μ

Tactic:
simpa only [isProbabilityMeasure_iff] using h

Premises used: MeasureTheory.isProbabilityMeasure_iff
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ

Tactic:
have := hfν.rnDeriv_comp_aeEq hμ.toMeasurePreserving
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
obtain : ∀ (c : ℝ≥0∞) (hc : ν.rnDeriv μ =ᶠ[ae μ] const X c), ∃ (c : ℝ≥0∞), ν = c • μ
⊢ ∃ (c : ℝ≥0∞), ν = c • μ

Tactic:
obtain ⟨c, hc⟩ := hμ.ae_eq_const_of_ae_eq_comp₀ (measurable_rnDeriv _ _).nullMeasurable this

Premises used: Measurable.nullMeasurable, Ergodic.ae_eq_const_of_ae_eq_comp₀, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
h : ν = c • μ
⊢ ∃ (c : ℝ≥0∞), ν = c • μ

Tactic:
use c
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
h :
  ∀ (s : Set X) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ν = c • μ

Tactic:
ext s hs
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
s : Set X
hs : MeasurableSet s
⊢ (ν : (a : Set X) → ℝ≥0∞) s = ∫⁻ (a : X) in s, ν.rnDeriv μ a ∂μ

Tactic:
.symm <| setLIntegral_rnDeriv hνμ _

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, Eq.symm
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
s : Set X
hs : MeasurableSet s
⊢ ∫⁻ (a : X) in s, ν.rnDeriv μ a ∂μ = ∫⁻ (x : X) in s, c ∂μ

Tactic:
lintegral_congr_ae <| hc.filter_mono <| ae_mono restrict_le_self

Premises used: Filter.EventuallyEq.filter_mono, MeasureTheory.ae_mono, MeasureTheory.lintegral_congr_ae, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
s : Set X
hs : MeasurableSet s
⊢ ∫⁻ (x : X) in s, c ∂μ = (c • μ : (a : Set X) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
s : Set X
hs : MeasurableSet s
ν₁ : ∫⁻ (x : X) in s, c ∂μ = (c • μ : (a : Set X) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    ν s = ∫⁻ a in s, ν.rnDeriv μ a ∂μ := .symm <| setLIntegral_rnDeriv hνμ _
    _ = ∫⁻ _ in s, c ∂μ := lintegral_congr_ae <| hc.filter_mono <| ae_mono restrict_le_self
    _ = (c • μ) s := by simp

Premises used: Filter.EventuallyEq.filter_mono, MeasureTheory.Measure.setLIntegral_rnDeriv, MeasureTheory.ae_mono, MeasureTheory.lintegral_congr_ae, MeasureTheory.Measure.restrict_le_self, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
huniv : Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
rcases :
  ∀ (c : ℝ≥0∞) [IsFiniteMeasure (c • μ)] (hfν : MeasurePreserving f (c • μ) (c • μ)) (hνμ : c • μ ≪ μ)
    (huniv : Eq (α := ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)),
    c • μ = μ
⊢ ν = μ

Tactic:
rcases hμ.eq_smul_of_absolutelyContinuous hfν hνμ with ⟨c, rfl⟩

Premises used: Ergodic.eq_smul_of_absolutelyContinuous, rfl
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst_1 : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : Eq (α := ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
inl :
  ∀ [IsFiniteMeasure.{u_1} (α := X) (m0 := m) 0] (hμ : Ergodic (m := m) f 0)
    [IsFiniteMeasure (HSMul.hSMul (β := Measure X) c 0)]
    (hfν : MeasurePreserving f (HSMul.hSMul (β := Measure X) c 0) (HSMul.hSMul (β := Measure X) c 0))
    (hνμ : HSMul.hSMul (β := Measure X) c 0 ≪ 0)
    (huniv :
      Eq (α := ℝ≥0∞) ((HSMul.hSMul (β := Measure X) c 0 : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
        (((0 : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)),
    HSMul.hSMul (β := Measure X) c 0 = 0
inr : ∀ (hμ₀ : μ ≠ 0), c • μ = μ
⊢ c • μ = μ

Tactic:
rcases eq_or_ne μ 0 with rfl | hμ₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
c : ℝ≥0∞
inst : IsFiniteMeasure.{u_1} (α := X) (m0 := m) 0
hμ : Ergodic (m := m) f 0
inst_1 : IsFiniteMeasure (HSMul.hSMul (β := Measure X) c 0)
hfν : MeasurePreserving f (HSMul.hSMul (β := Measure X) c 0) (HSMul.hSMul (β := Measure X) c 0)
hνμ : HSMul.hSMul (β := Measure X) c 0 ≪ 0
huniv :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (β := Measure X) c 0 : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
    (((0 : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HSMul.hSMul (β := Measure X) c 0 = 0

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst_1 : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : Eq (α := ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hμ₀ : μ ≠ 0
⊢ c • μ = μ

Tactic:
simp_all [ENNReal.mul_eq_right]

Premises used: ENNReal.mul_eq_right
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
⊢ Membership.mem (γ := Set (Measure X))
      {ν : Measure X |
        MeasurePreserving f ν ν ∧
          Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
      μ ∧
    ∀ (x₁ : Measure X),
      Membership.mem (γ := Set (Measure X))
          {ν : Measure X |
            MeasurePreserving f ν ν ∧
              Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
          x₁ →
        ∀ (x₂ : Measure X),
          Membership.mem (γ := Set (Measure X))
              {ν : Measure X |
                MeasurePreserving f ν ν ∧
                  Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
              x₂ →
            μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ

Tactic:
⟨⟨hμ.toMeasurePreserving, rfl⟩, ?_⟩

Premises used: Ergodic.toMeasurePreserving, And.intro, rfl
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
refine :
  ∀ (x₁ : Measure X),
    Membership.mem (γ := Set (Measure X))
        {ν : Measure X |
          MeasurePreserving f ν ν ∧
            Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
        x₁ →
      ∀ (x₂ : Measure X),
        Membership.mem (γ := Set (Measure X))
            {ν : Measure X |
              MeasurePreserving f ν ν ∧
                Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
            x₂ →
          μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ
⊢ Membership.mem (γ := Set (Measure X))
      {ν : Measure X |
        MeasurePreserving f ν ν ∧
          Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
      μ ∧
    ∀ (x₁ : Measure X),
      Membership.mem (γ := Set (Measure X))
          {ν : Measure X |
            MeasurePreserving f ν ν ∧
              Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
          x₁ →
        ∀ (x₂ : Measure X),
          Membership.mem (γ := Set (Measure X))
              {ν : Measure X |
                MeasurePreserving f ν ν ∧
                  Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
              x₂ →
            μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ

Tactic:
refine ⟨⟨hμ.toMeasurePreserving, rfl⟩, ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
rw : LT.lt (α := ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [hν₁μ]
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply measure_lt_top

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ IsFiniteMeasure ν₁

Tactic:
have : IsFiniteMeasure ν₁ := ⟨by rw [hν₁μ]; apply measure_lt_top⟩
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν₁
apply : ν₁ ≪ a • ν₁
⊢ ν₁ = a • ν₁ + b • ν₂

Tactic:
apply hμ.eq_of_absolutelyContinuous_measure_univ_eq hfν₁ (.add_right _ _) hν₁μ

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.add_right, Ergodic.eq_of_absolutelyContinuous_measure_univ_eq
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν₁
⊢ ν₁ ≪ a • ν₁

Tactic:
apply absolutelyContinuous_smul ha.ne'

Premises used: MeasureTheory.Measure.absolutelyContinuous_smul, LT.lt.ne'
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsProbabilityMeasure μ
hμ : Ergodic f μ
⊢ Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}) μ

Tactic:
simpa only [isProbabilityMeasure_iff, measure_univ] using hμ.mem_extremePoints_measure_univ_eq

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.isProbabilityMeasure_iff, Ergodic.mem_extremePoints_measure_univ_eq
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
⊢ Ergodic f μ ↔
    Membership.mem (γ := Set (Measure X))
      (extremePoints ℝ≥0∞
        {ν : Measure X |
          MeasurePreserving f ν ν ∧
            Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)})
      μ

Tactic:
⟨mem_extremePoints_measure_univ_eq, of_mem_extremePoints_measure_univ_eq (measure_ne_top _ _)⟩

Premises used: MeasureTheory.measure_ne_top, Ergodic.of_mem_extremePoints_measure_univ_eq, Iff.intro, Ergodic.mem_extremePoints_measure_univ_eq
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsProbabilityMeasure μ
⊢ Ergodic f μ ↔
    Membership.mem (γ := Set (Measure X))
      (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}) μ

Tactic:
⟨mem_extremePoints, of_mem_extremePoints⟩

Premises used: Iff.intro, Ergodic.mem_extremePoints, Ergodic.of_mem_extremePoints
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_

Premises used: MeasurableSet, Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
refine : ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
refine exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_

Premises used: MeasurableSet, Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U

Tactic:
fun U hU ↦ h.ae_mem_or_ae_notMem₀ (s := g ⁻¹' U) (hgm hU) ?_b

Premises used: Set.Mem, QuasiErgodic.ae_mem_or_ae_notMem₀, setOf, Set.preimage
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
_b : ∀ (U : Set X) (hU : MeasurableSet U), f ⁻¹' g ⁻¹' U =ᶠ[ae μ] g ⁻¹' U
⊢ ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U

Tactic:
refine fun U hU ↦ h.ae_mem_or_ae_notMem₀ (s := g ⁻¹' U) (hgm hU) ?_b
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' g ⁻¹' U =ᶠ[ae μ] g ⁻¹' U

Tactic:
(hg_eq.mono fun x hx ↦ ?_).set_eq

Premises used: Filter.Eventually.set_eq, Filter.Eventually.mono
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
_b : ∀ (x : α) (hx : (g ∘ f) x = g x), x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U
⊢ f ⁻¹' g ⁻¹' U =ᶠ[ae μ] g ⁻¹' U

Tactic:
refine (hg_eq.mono fun x hx ↦ ?_).set_eq

Premises used: Filter.Eventually.set_eq, Filter.Eventually.mono
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
_b : x ∈ g ∘ f ⁻¹' U ↔ x ∈ g ⁻¹' U
_b₁ : (g ∘ f) x ∈ U ↔ x ∈ g ⁻¹' U
_b₂ : (g ∘ f) x ∈ U ↔ g x ∈ U
_b₃ _b₄ : g x ∈ U ↔ g x ∈ U
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U

Tactic:
rw [← preimage_comp, mem_preimage, mem_preimage, hx]

Premises used: Set.preimage_comp, Set.mem_preimage
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
inst_3 : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
rw : g ∘ f ⁻¹' U = g ⁻¹' U
rw₁ rw₂ : g ⁻¹' U = g ⁻¹' U
⊢ f ⁻¹' g ⁻¹' U = g ⁻¹' U

Tactic:
rw [← preimage_comp, hg_eq]

Premises used: Set.preimage_comp