awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
⊢ (n + 1) * m = l - k

Tactic:
have : (n + 1) * m = l - k := by
    apply Nat.mul_div_cancel'
    exact (Nat.modEq_iff_dvd' hkl.le).1 hn
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s

Tactic:
⟨f^[k] x, hk, m, ?_, ?_⟩

Premises used: Nat.iterate, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
succ : m ≠ 0
succ₁ : f^[n + 1]^[m] (f^[k] x) ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s

Tactic:
refine ⟨f^[k] x, hk, m, ?_, ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
⊢ l ≤ k

Tactic:
rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this

Premises used: tsub_eq_zero_iff_le, eq_comm, MulZeroClass.mul_zero
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
this₁ : l ≤ k
⊢ m = 0

Tactic:
rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this

Premises used: tsub_eq_zero_iff_le, eq_comm, MulZeroClass.mul_zero
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False

Tactic:
this.not_gt hkl

Premises used: LE.le.not_gt
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False

Tactic:
exact this.not_gt hkl

Premises used: LE.le.not_gt
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
succ : k ≤ l
⊢ f^[n + 1]^[m] (f^[k] x) ∈ s

Tactic:
rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]

Premises used: Function.iterate_add_apply, tsub_add_cancel_of_le, Function.iterate_mul
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l

Tactic:
hkl.le

Premises used: LT.lt.le
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
left : x ∈ s
hx : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
k : ℕ
hk : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} k
l : ℕ
hl : Membership.mem (γ := Set ℕ) {n : ℕ | f^[n] x ∈ s} l
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l

Tactic:
exact hkl.le

Premises used: LT.lt.le
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hs : MeasurableSet s
hfs : f ⁻¹' s = s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
simpa only [eventuallyConst_set'] using hf.aeconst_set hs hfs

Premises used: Filter.eventuallyConst_set', PreErgodic.aeconst_set
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa using hf.ae_empty_or_univ hs hs'

Premises used: PreErgodic.ae_empty_or_univ
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hsm : MeasurableSet s
hs : f ⁻¹' s = s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s

Tactic:
eventuallyConst_set.1 <| hf.aeconst_set hsm hs

Premises used: Filter.eventuallyConst_set, Iff.mp, PreErgodic.aeconst_set
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst : IsProbabilityMeasure μ
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'

Premises used: PreErgodic.measure_self_or_compl_eq_zero
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
n : ℕ
hf : PreErgodic f^[n] μ
⊢ PreErgodic f μ

Tactic:
⟨fun _ hs hs' => hf.aeconst_set hs <| IsFixedPt.preimage_iterate hs' n⟩

Premises used: Function.IsFixedPt.preimage_iterate, PreErgodic.mk, PreErgodic.aeconst_set
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
x : Set α
h : MeasurableSet x
h_1 : f ⁻¹' x = x
⊢ EventuallyConst x (ae (F := autoParam (Measure α) _auto_1) 0)

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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 : EventuallyConst (g ⁻¹' s) (ae μ)
⊢ EventuallyConst s (ae μ')

Tactic:
rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.MeasurePreserving.aeconst_preimage
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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
apply : f ⁻¹' g ⁻¹' s = g ⁻¹' s
⊢ EventuallyConst (g ⁻¹' s) (ae μ)

Tactic:
apply hf.aeconst_set (hg.measurable hs₀)

Premises used: MeasureTheory.MeasurePreserving.measurable, PreErgodic.aeconst_set
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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
rw₃ rw₄ : g ⁻¹' s = g ⁻¹' s
⊢ f ⁻¹' g ⁻¹' s = g ⁻¹' s

Tactic:
rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]

Premises used: Function.Semiconj.comp_eq, Set.preimage_comp
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : Ergodic f μ
f' : β → β
hf' : Measurable f'
h_comm : Semiconj g f f'
⊢ Ergodic f' μ'

Tactic:
⟨hg.of_semiconj hf.toMeasurePreserving h_comm hf',
   hg.preErgodic_of_preErgodic_semiconj hf.toPreErgodic h_comm⟩

Premises used: MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_semiconj, Ergodic.mk, Ergodic.toMeasurePreserving, MeasureTheory.MeasurePreserving.of_semiconj, Ergodic.toPreErgodic
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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 μ

Tactic:
⟨fun hf => preErgodic_of_preErgodic_semiconj (h.symm e) hf ?_,
      fun hf => preErgodic_of_preErgodic_semiconj h hf ?_⟩

Premises used: MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_semiconj, MeasureTheory.MeasurePreserving.symm, Iff.intro
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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
refine_2 :
  ∀ (hf : PreErgodic f μ),
    Semiconj.{u_1, u_2} (β := β) (⇑e : (a : α) → β) f ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α))
⊢ PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ

Tactic:
refine ⟨fun hf => preErgodic_of_preErgodic_semiconj (h.symm e) hf ?_,
      fun hf => preErgodic_of_preErgodic_semiconj h hf ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
hf : PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ'
⊢ Semiconj.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) f

Tactic:
simp [Semiconj]

Premises used: Function.Semiconj
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e : (a : α) → β) μ μ'
hf : PreErgodic f μ
⊢ Semiconj.{u_1, u_2} (β := β) (⇑e : (a : α) → β) f ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α))

Tactic:
simp [Semiconj]

Premises used: Function.Semiconj
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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 μ μ
rw₁ rw₂ : MeasurePreserving f μ μ ↔ MeasurePreserving f μ μ
⊢ MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ

Tactic:
rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.comp_right_iff, MeasureTheory.MeasurePreserving.comp_left_iff
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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 μ μ

Tactic:
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
    rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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 μ μ
⊢ PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ

Tactic:
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
this : MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ
h : PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ
⊢ Ergodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ Ergodic f μ

Tactic:
⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
    fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩

Premises used: Iff.mpr, Ergodic.mk, Ergodic.toMeasurePreserving, Iff.intro, Iff.mp, Ergodic.toPreErgodic
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
this : MeasurePreserving ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' μ' ↔ MeasurePreserving f μ μ
h : PreErgodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ PreErgodic f μ
⊢ Ergodic ((⇑e : (a : α) → β) ∘ f ∘ (⇑e.symm : (a : β) → α)) μ' ↔ Ergodic f μ

Tactic:
exact ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
    fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : QuasiErgodic f μ
hsm : NullMeasurableSet s μ
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
let ⟨_t, h₀, h₁, h₂⟩ := hf.toQuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae hsm hs
  (hf.aeconst_set h₀ h₂).congr h₁

Premises used: MeasureTheory.ae, _private.0.QuasiErgodic.aeconst_set₀.match_1, QuasiErgodic.toQuasiMeasurePreserving, Filter.EventuallyConst, QuasiErgodic.toPreErgodic, Filter.EventuallyConst.congr, MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae, PreErgodic.aeconst_set
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : QuasiErgodic f μ
hsm : NullMeasurableSet s μ
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
eventuallyConst_set'.mp <| hf.aeconst_set₀ hsm hs

Premises used: Filter.eventuallyConst_set', QuasiErgodic.aeconst_set₀, Iff.mp
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : QuasiErgodic f μ
hsm : NullMeasurableSet s μ
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s

Tactic:
eventuallyConst_set.mp <| hf.aeconst_set₀ hsm hs

Premises used: Filter.eventuallyConst_set, QuasiErgodic.aeconst_set₀, Iff.mp
-- 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 : QuasiErgodic f μ
c : R
⊢ QuasiErgodic f (c • μ)

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

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

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
hf : Ergodic f μ
⊢ QuasiErgodic f μ

Tactic:
{ hf.toPreErgodic, hf.toMeasurePreserving.quasiMeasurePreserving with }

Premises used: Ergodic.toMeasurePreserving, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, QuasiErgodic.mk, Ergodic.toPreErgodic
-- 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 μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
hf.quasiErgodic.ae_empty_or_univ₀ hs ?_

Premises used: Ergodic.quasiErgodic, QuasiErgodic.ae_empty_or_univ₀
-- 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∞)
refine : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_

Premises used: Ergodic.quasiErgodic, QuasiErgodic.ae_empty_or_univ₀
-- 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∞)
⊢ f ⁻¹' s =ᶠ[ae μ] s

Tactic:
ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).ge ?_ h_fin

Premises used: Eq.ge, Ergodic.toMeasurePreserving, MeasureTheory.ae_eq_of_ae_subset_of_measure_ge, MeasureTheory.MeasurePreserving.measure_preimage
-- 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∞)
refine : NullMeasurableSet (f ⁻¹' s) μ
⊢ f ⁻¹' s =ᶠ[ae μ] s

Tactic:
refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).ge ?_ h_fin

Premises used: Eq.ge, Ergodic.toMeasurePreserving, MeasureTheory.ae_eq_of_ae_subset_of_measure_ge, MeasureTheory.MeasurePreserving.measure_preimage
-- 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∞)
⊢ NullMeasurableSet (f ⁻¹' s) μ

Tactic:
hs.preimage hf.quasiMeasurePreserving

Premises used: Ergodic.toMeasurePreserving, MeasureTheory.NullMeasurableSet.preimage, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- 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∞)
⊢ NullMeasurableSet (f ⁻¹' s) μ

Tactic:
exact hs.preimage hf.quasiMeasurePreserving

Premises used: Ergodic.toMeasurePreserving, MeasureTheory.NullMeasurableSet.preimage, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [hf.measure_preimage hs]

Premises used: Ergodic.toMeasurePreserving, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
replace h_fin : μ (f ⁻¹' s) ≠ ∞ := by rwa [hf.measure_preimage hs]
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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

Tactic:
hf.quasiErgodic.ae_empty_or_univ₀ hs ?_

Premises used: Ergodic.quasiErgodic, QuasiErgodic.ae_empty_or_univ₀
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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∞)
refine : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_

Premises used: Ergodic.quasiErgodic, QuasiErgodic.ae_empty_or_univ₀
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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∞)
⊢ f ⁻¹' s =ᶠ[ae μ] s

Tactic:
(ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm

Premises used: Ergodic.toMeasurePreserving, Eq.le, MeasureTheory.ae_eq_of_ae_subset_of_measure_ge, Filter.EventuallyEq.symm, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.Ergodic
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∞)
⊢ f ⁻¹' s =ᶠ[ae μ] s

Tactic:
exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm

Premises used: Ergodic.toMeasurePreserving, Eq.le, MeasureTheory.ae_eq_of_ae_subset_of_measure_ge, Filter.EventuallyEq.symm, MeasureTheory.MeasurePreserving.measure_preimage