awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f '' s ≤ᶠ[ae μ] s
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s ≤ᶠ[ae μ] f ⁻¹' s

Tactic:
replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
    (HasSubset.Subset.eventuallyLE (subset_preimage_image f s)).trans
      (hf.quasiMeasurePreserving.preimage_mono_ae hs')
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin

Premises used: Ergodic.ae_empty_or_univ_of_ae_le_preimage'
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin

Premises used: Ergodic.ae_empty_or_univ_of_ae_le_preimage'
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
he : Ergodic (⇑e : (a : α) → α) μ
s : Set α
hsm : MeasurableSet s
hs : (⇑e.symm : (a : α) → α) ⁻¹' s = s
rw : s
| (⇑e : (a : α) → α) ⁻¹' s

Tactic:
rw [← hs, ← e.image_eq_preimage_symm, e.preimage_image]

Premises used: MeasurableEquiv.preimage_image, MeasurableEquiv.image_eq_preimage_symm
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
he : Ergodic (⇑e : (a : α) → α) μ
s : Set α
hsm : MeasurableSet s
hs : (⇑e.symm : (a : α) → α) ⁻¹' s = s
conv_lhs : (⇑e : (a : α) → α) ⁻¹' s = s
conv_lhs₁ : s = s
⊢ (⇑e : (a : α) → α) ⁻¹' s = s

Tactic:
conv_lhs => rw [← hs, ← e.image_eq_preimage_symm, e.preimage_image]

Premises used: MeasurableEquiv.preimage_image, MeasurableEquiv.image_eq_preimage_symm
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
⊢ Ergodic (⇑e.symm : (a : α) → α) μ ↔ Ergodic (⇑e : (a : α) → α) μ

Tactic:
⟨.symm, .symm⟩

Premises used: Iff.intro, Ergodic.symm
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
R : Type u_2
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : Ergodic f μ
c : R
⊢ Ergodic f (c • μ)

Tactic:
⟨hf.1.smul_measure _, hf.2.smul_measure _⟩

Premises used: Ergodic.mk, MeasureTheory.MeasurePreserving.smul_measure, PreErgodic.smul_measure, Ergodic.toMeasurePreserving, Ergodic.toPreErgodic
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Eq (α := Measure α) (Measure.map f 0) 0

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst : IsFiniteMeasure μ
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
ae_empty_or_univ_of_preimage_ae_le' hf hs hs' <| measure_ne_top μ s

Premises used: MeasureTheory.measure_ne_top, Ergodic.ae_empty_or_univ_of_preimage_ae_le'
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst : IsFiniteMeasure μ
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
ae_empty_or_univ_of_ae_le_preimage' hf hs hs' <| measure_ne_top μ s

Premises used: MeasureTheory.measure_ne_top, Ergodic.ae_empty_or_univ_of_ae_le_preimage'
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst : IsFiniteMeasure μ
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f '' s ≤ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
ae_empty_or_univ_of_image_ae_le' hf hs hs' <| measure_ne_top μ s

Premises used: MeasureTheory.measure_ne_top, Ergodic.ae_empty_or_univ_of_image_ae_le'
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
⊢ MeasurePreserving f μ μ

Tactic:
have hf : MeasurePreserving f μ μ := h.1.1
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
inl :
  ∀ (hc : Ne (α := ℝ≥0∞) 0 ∞)
    (h :
      Membership.mem (γ := Set (Measure X))
        (extremePoints ℝ≥0∞
          {ν : Measure X | MeasurePreserving f ν ν ∧ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)})
        μ),
    Ergodic f μ
inr : ∀ (hc₀ : c ≠ 0), Ergodic f μ
⊢ Ergodic f μ

Tactic:
rcases eq_or_ne c 0 with rfl | hc₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : Ne (α := ℝ≥0∞) 0 ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞
      {ν : Measure X | MeasurePreserving f ν ν ∧ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)})
    μ
⊢ Ergodic (m := m) f 0

Tactic:
zero_measure hf.measurable

Premises used: Ergodic.zero_measure, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : Ne (α := ℝ≥0∞) 0 ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞
      {ν : Measure X | MeasurePreserving f ν ν ∧ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)})
    μ
h₁ : μ = 0
⊢ Ergodic f μ

Tactic:
convert! zero_measure hf.measurable

Premises used: Ergodic.zero_measure, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : Ne (α := ℝ≥0∞) 0 ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞
      {ν : Measure X | MeasurePreserving f ν ν ∧ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)})
    μ
h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ h₃ : Eq (α := ℝ≥0∞) 0 0
⊢ μ = 0

Tactic:
rw [← measure_univ_eq_zero, h.1.2]

Premises used: And.right, And.left, MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ

Tactic:
⟨hf, ⟨?_⟩⟩

Premises used: Ergodic.mk, PreErgodic.mk
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
inr : ∀ ⦃s : Set X⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)
⊢ Ergodic f μ

Tactic:
refine ⟨hf, ⟨?_⟩⟩
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure μ

Tactic:
constructor
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
measure_univ_lt_top : c < ∞
measure_univ_lt_top₁ measure_univ_lt_top₂ measure_univ_lt_top₃ measure_univ_lt_top₄ : c ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [h.1.2, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, And.right, And.left
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ IsFiniteMeasure μ

Tactic:
have : IsFiniteMeasure μ := by
      constructor
      rwa [h.1.2, lt_top_iff_ne_top]
-- Module: Mathlib.Dynamics.Ergodic.Extreme
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h :
  Membership.mem (γ := Set (Measure X))
    (extremePoints ℝ≥0∞ {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}) μ
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
⊢ let S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c};
  μ ∈ extremePoints ℝ≥0∞ S

Tactic:
set S := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
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

Tactic:
⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩

Premises used: Set.Mem, setOf, MeasureTheory.MeasurePreserving.smul_measure, And.intro
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : MeasurePreserving f (μ.restrict s) (μ.restrict s)
refine_2 : (c • μ[|s] : (a : Set X) → ℝ≥0∞) univ = c
⊢ c • μ[|s] ∈ S

Tactic:
refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurePreserving f (μ.restrict (f ⁻¹' s)) (μ.restrict s)

Tactic:
hf.restrict_preimage hsm

Premises used: MeasureTheory.MeasurePreserving.restrict_preimage
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : s = f ⁻¹' s
⊢ MeasurePreserving f (μ.restrict s) (μ.restrict s)

Tactic:
convert! hf.restrict_preimage hsm

Premises used: MeasureTheory.MeasurePreserving.restrict_preimage
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s = f ⁻¹' s

Tactic:
hfs.symm

Premises used: Eq.symm
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s = f ⁻¹' s

Tactic:
exact hfs.symm

Premises used: Eq.symm
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 : HSMul.hSMul (β := ℝ≥0∞) c (μ[univ | s] : ℝ≥0∞) = c
refine_2₁ : HSMul.hSMul (β := ℝ≥0∞) c 1 = c
refine_2₂ : c * 1 = c
refine_2₃ refine_2₄ : c = c
⊢ (c • μ[|s] : (a : Set X) → ℝ≥0∞) univ = c

Tactic:
rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.Measure.smul_apply, smul_eq_mul, mul_one
-- 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 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
⊢ ∀ {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

Tactic:
have {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s) (hμs : μ s ≠ 0) :
        c • μ[|s] ∈ S := by
      refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
      · convert! hf.restrict_preimage hsm
        exact hfs.symm
      · rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
-- 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
inr : ∀ (H : ¬EventuallyConst s (ae μ)), False
⊢ EventuallyConst s (ae μ)

Tactic:
by_contra H
-- 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 μ)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: Filter.eventuallyConst_set, and_comm, MeasureTheory.ae_iff
-- 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 μ)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨hs, hs'⟩ : μ s ≠ 0 ∧ μ sᶜ ≠ 0 := by
      simpa [eventuallyConst_set, ae_iff, and_comm] using H

Premises used: Compl.compl, DFunLike.coe
-- 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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨hs, hs'⟩ : μ s ≠ 0 ∧ μ sᶜ ≠ 0 := by
      simpa [eventuallyConst_set, ae_iff, and_comm] using H

Premises used: Compl.compl, DFunLike.coe
-- 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∞)
rw : (f ⁻¹' s)ᶜ = sᶜ
rw₁ rw₂ : sᶜ = sᶜ
⊢ f ⁻¹' sᶜ = sᶜ

Tactic:
rw [preimage_compl, hfs]

Premises used: Set.preimage_compl
-- 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∞)
apply : μ ∈ openSegment ℝ≥0∞ (c • μ[|s]) (c • μ[|sᶜ])
⊢ c • μ[|s] = μ

Tactic:
apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')

Premises used: MeasurableSet.compl, And.right
-- 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∞)
⊢ μ ∈ openSegment ℝ≥0∞ (c • μ[|s]) (c • μ[|sᶜ])

Tactic:
⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩

Premises used: Set.Mem, Compl.compl, setOf, HDiv.hDiv, And.intro, Exists.intro, ENNReal.div_pos, openSegment, DFunLike.coe
-- 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∞)
refine_1 :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1
refine_2 :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c • c • μ[|s] +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c • c • μ[|sᶜ] =
    μ
⊢ μ ∈ openSegment ℝ≥0∞ (c • μ[|s]) (c • μ[|sᶜ])

Tactic:
refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
-- 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∞)
refine_1 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) / c = 1
refine_1₁ : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) c = 1
refine_1₂ : c / c = 1
refine_1₃ refine_1₄ : Eq (α := ℝ≥0∞) 1 1
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1

Tactic:
rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]

Premises used: MeasureTheory.measure_add_measure_compl, ENNReal.add_div, ENNReal.div_self, And.right, And.left
-- 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∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c • c • μ[|s] +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c • c • μ[|sᶜ] =
    μ

Tactic:
simp [ProbabilityTheory.cond, smul_smul, ← mul_assoc, ENNReal.div_mul_cancel,
          ENNReal.mul_inv_cancel, *]

Premises used: mul_assoc, smul_smul, ENNReal.div_mul_cancel, ENNReal.mul_inv_cancel, ProbabilityTheory.cond