awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
rw : g ∘ f ⁻¹' s = g ⁻¹' s
rw₁ : f' ∘ g ⁻¹' s = g ⁻¹' s
rw₂ : g ⁻¹' f' ⁻¹' s = g ⁻¹' s
⊢ f ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw₃ : g ⁻¹' s = g ⁻¹' s
Tactic: rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
⊢ PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ
have refine_1 : ∀ (hf : PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ'),
  Semiconj.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) f
Tactic: refine ⟨fun hf => preErgodic_of_preErgodic_semiconj (h.symm e) hf ?_,
      fun hf => preErgodic_of_preErgodic_semiconj h hf ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
refine_1 :
  ∀ (hf : PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ'),
    Semiconj.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) f
⊢ PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ
have refine_2 : ∀ (hf : PreErgodic f μ),
  Semiconj.{u_1, u_2} (β := β) (⇑e : (a : α) → β) f ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α))
Tactic: refine ⟨fun hf => preErgodic_of_preErgodic_semiconj (h.symm e) hf ?_,
      fun hf => preErgodic_of_preErgodic_semiconj h hf ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
⊢ MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ
have rw : MeasurePreserving (f ∘ (⇑e.symm : (a : β) → α)) μ' μ ↔ MeasurePreserving f μ μ
Tactic: rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
rw : MeasurePreserving (f ∘ (⇑e.symm : (a : β) → α)) μ' μ ↔ MeasurePreserving f μ μ
⊢ MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ
have rw₁ : MeasurePreserving f μ μ ↔ MeasurePreserving f μ μ
Tactic: rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
⊢ Ergodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ Ergodic f μ
have this : MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ
Tactic: have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
    rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
this : MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ
⊢ Ergodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ Ergodic f μ
have h₁ : PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ
Tactic: replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
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 μ] ∅ ∨ s =ᶠ[ae μ] univ
have refine : f ⁻¹' s =ᶠ[ae μ] s
Tactic: refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
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∞)
⊢ f ⁻¹' s =ᶠ[ae μ] s
have refine : NullMeasurableSet (f ⁻¹' s) μ
Tactic: refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).ge ?_ h_fin
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
have h_fin₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: replace h_fin : μ (f ⁻¹' s) ≠ ∞ := by rwa [hf.measure_preimage hs]
Cleared hypotheses: h_fin
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
have refine : f ⁻¹' s =ᶠ[ae μ] s
Tactic: refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (hypothesis)
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 μ] ∅ ∨ s =ᶠ[ae μ] univ
have hs'₁ : 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')
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
he : Ergodic (⇑e : (a : α) → α) μ
s : Set α
hsm : MeasurableSet s
hs : (⇑e.symm : (a : α) → α) ⁻¹' s = s
| (⇑e : (a : α) → α) ⁻¹' s
have rw : s
Tactic: rw [← hs, ← e.image_eq_preimage_symm, e.preimage_image]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
he : Ergodic (⇑e : (a : α) → α) μ
s : Set α
hsm : MeasurableSet s
hs : (⇑e.symm : (a : α) → α) ⁻¹' s = s
⊢ (⇑e : (a : α) → α) ⁻¹' s = s
have conv_lhs : (⇑e : (a : α) → α) ⁻¹' s = s
Tactic: conv_lhs => rw [← hs, ← e.image_eq_preimage_symm, e.preimage_image]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Ergodic (goal)
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
⊢ (⇑e : (a : α) → α) ⁻¹' s = s
have conv_lhs₁ : s = s
Tactic: conv_lhs => rw [← hs, ← e.image_eq_preimage_symm, e.preimage_image]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
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}) μ
⊢ Ergodic f μ
have hf : MeasurePreserving f μ μ
Tactic: have hf : MeasurePreserving f μ μ := h.1.1
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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 μ μ
⊢ Ergodic f μ
have 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 μ
Tactic: rcases eq_or_ne c 0 with rfl | hc₀
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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 μ
⊢ Ergodic f μ
have inr : ∀ (hc₀ : c ≠ 0), Ergodic f μ
Tactic: rcases eq_or_ne c 0 with rfl | hc₀
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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 f μ
have h₁ : μ = 0
Tactic: convert! zero_measure hf.measurable
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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∞)})
    μ
⊢ μ = 0
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_univ_eq_zero, h.1.2]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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∞)
⊢ μ = 0
have h₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← measure_univ_eq_zero, h.1.2]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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 μ
have inr : ∀ ⦃s : Set X⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)
Tactic: refine ⟨hf, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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 μ
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have measure_univ_lt_top : c < ∞
Tactic: rwa [h.1.2, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
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
⊢ ∀ ⦃s : Set X⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)
have this : IsFiniteMeasure μ
Tactic: have : IsFiniteMeasure μ := by
      constructor
      rwa [h.1.2, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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
have refine_1 : MeasurePreserving f (μ.restrict s) (μ.restrict s)
Tactic: refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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)
⊢ c • μ[|s] ∈ S
have refine_2 : (c • μ[|s] : (a : Set X) → ℝ≥0∞) univ = c
Tactic: refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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 s) (μ.restrict s)
have h₁ : s = f ⁻¹' s
Tactic: convert! hf.restrict_preimage hsm
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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] : (a : Set X) → ℝ≥0∞) univ = c
have refine_2 : HSMul.hSMul (β := ℝ≥0∞) c (μ[univ | s] : ℝ≥0∞) = c
Tactic: rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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
⊢ (c • μ[|s] : (a : Set X) → ℝ≥0∞) univ = c
have refine_2₁ : HSMul.hSMul (β := ℝ≥0∞) c 1 = c
Tactic: rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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
⊢ (c • μ[|s] : (a : Set X) → ℝ≥0∞) univ = c
have refine_2₂ : c * 1 = c
Tactic: rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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
⊢ (c • μ[|s] : (a : Set X) → ℝ≥0∞) univ = c
have refine_2₃ : c = c
Tactic: rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
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⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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
⊢ EventuallyConst s (ae μ)
have inr : ∀ (H : ¬EventuallyConst s (ae μ)), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
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 μ)
⊢ False
have hs : 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
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
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∞)
⊢ False
have hs' : 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
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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∞)
⊢ f ⁻¹' sᶜ = sᶜ
have rw : (f ⁻¹' s)ᶜ = sᶜ
Tactic: rw [preimage_compl, hfs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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ᶜ
⊢ f ⁻¹' sᶜ = sᶜ
have rw₁ : sᶜ = sᶜ
Tactic: rw [preimage_compl, hfs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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] = μ
have apply : μ ∈ openSegment ℝ≥0∞ (c • μ[|s]) (c • μ[|sᶜ])
Tactic: apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
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ᶜ])
have refine_1 : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
  1
Tactic: refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩