awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
have rwa : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋃ (n : ℕ), ⋃ (_ : n > N), t n) : ENNReal) (0 : ENNReal)
Tactic: rwa [hT, measure_diff_null]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
⊢ False
have hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
Tactic: have hμT : μ T ≠ 0 := by
    rwa [hT, measure_diff_null]
    exact (measure_biUnion_null_iff {n | N < n}.to_countable).2 hmax
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
⊢ False
have hTm : NullMeasurableSet T μ
Tactic: have hTm : NullMeasurableSet T μ := htm.diff <| .biUnion {n | N < n}.to_countable fun _ _ ↦ htm
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
⊢ False
have rcases : ∀ (x : α) (hxt : x ∈ T) (m : ℕ) (hm₀ : m ≠ 0) (hmt : f^[m] x ∈ T), False
Tactic: rcases hf.exists_mem_iterate_mem hTm hμT with ⟨x, hxt, m, hm₀, hmt⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ False
have refine_1 : N + m > N
Tactic: refine hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
refine_1 : N + m > N
⊢ False
have refine_2 : x ∈ f^[N + m] ⁻¹' s
Tactic: refine hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)
have by_contra : ∀ (H : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)),
  False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)
⊢ NullMeasurableSet (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s}) μ
have simp : NullMeasurableSet (s ∩ ⋂ (i : ℕ), ⋂ (_ : i ≥ n), {a : α | f^[i] a ∈ s}ᶜ) μ
Tactic: simp only [setOf_forall, ← compl_setOf]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)
⊢ False
have this : NullMeasurableSet (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s}) μ
Tactic: have : NullMeasurableSet (s ∩ { x | ∀ m ≥ n, f^[m] x ∉ s }) μ := by
    simp only [setOf_forall, ← compl_setOf]
    exact hs.inter <| .biInter (to_countable _) fun m _ ↦
      (hs.preimage <| hf.toQuasiMeasurePreserving.iterate m).compl
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)
this : NullMeasurableSet (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s}) μ
⊢ False
have rcases : ∀ (m : ℕ) (hmn : m > n)
  (hm :
    Ne (α := ENNReal)
      ((μ : (a : Set α) → ENNReal)
          (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s} ∩ f^[m] ⁻¹' (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s})) :
        ENNReal)
      (0 : ENNReal)),
  False
Tactic: rcases (hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)
this : NullMeasurableSet (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s}) μ
m : ℕ
hmn : m > n
hm :
  Ne (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s} ∩ f^[m] ⁻¹' (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s})) :
      ENNReal)
    (0 : ENNReal)
⊢ False
have rcases : ∀ x ∈ s, ∀ (hxn : Membership.mem (γ := Set α) {x : α | ∀ m ≥ n, f^[m] x ∉ s} x) (hxm : f^[m] x ∈ s), False
Tactic: rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
have simp : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, ∀ (a_1 : a ∈ s), ∃ b ≥ i, f^[b] a ∈ s
Tactic: simp only [frequently_atTop, @forall_comm (_ ∈ s), ae_all_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, ∀ (a_1 : a ∈ s), ∃ b ≥ n, f^[b] a ∈ s
have h : ∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → ∀ (a_2 : a ∈ s), ∃ b ≥ n, f^[b] a ∈ s
Tactic: filter_upwards
    [measure_eq_zero_iff_ae_notMem.1 (hf.measure_mem_forall_ge_image_notMem_eq_zero hs n)]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
have refine : ∀ (k : ℕ), ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s
Tactic: refine ae_all_iff.2 fun k => ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s
have refine : ∀ (x : α) (hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s) (hk : f^[k] x ∈ s),
  ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
Tactic: refine (hf.ae_mem_imp_frequently_image_mem
    (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
have rw : ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s
Tactic: rw [← map_add_atTop_eq_nat k, frequently_map]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s
have refine : ∀ (n : ℕ) (hn : f^[n] x ∈ f^[k] ⁻¹' s), f^[n + k] x ∈ s
Tactic: refine (hx hk).mono fun n hn => ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[n + k] x ∈ s
have rwa : f^[k + n] x ∈ s
Tactic: rwa [add_comm, iterate_add_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
rwa : f^[k + n] x ∈ s
⊢ f^[n + k] x ∈ s
have rwa₁ : f^[k] (f^[n] x) ∈ s
Tactic: rwa [add_comm, iterate_add_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
have this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
Tactic: have : ∀ s ∈ countableBasis α, ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s := fun s hs =>
    h.ae_mem_imp_frequently_image_mem (isOpen_of_mem_countableBasis hs).nullMeasurableSet
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
have refine : ∀ (x : α) (hx : ∀ (i : Set α) (hi : i ∈ countableBasis α), x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i) (s : Set α)
  (hs : s ∈ 𝓝 x), ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
Tactic: refine ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ (i : Set α) (hi : i ∈ countableBasis α), x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
have rcases : ∀ (o : Set α) (hoS : o ∈ countableBasis α) (hxo : x ∈ o) (hos : o ⊆ s), ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
Tactic: rcases (isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n] μ
have zero : Conservative f^[0] μ
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
zero : Conservative f^[0] μ
⊢ Conservative f^[n] μ
have succ : ∀ (n : ℕ), Conservative f^[n + 1] μ
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n + 1] μ
have succ : ∀ (s : Set α) (hs : MeasurableSet s) (hs0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)),
  ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
Tactic: refine ⟨hf.1.iterate _, fun s hs hs0 => ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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 ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
have succ : ∀ x ∈ s, ∀ (hx : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s), ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
Tactic: rcases (hf.frequently_ae_mem_and_frequently_image_mem hs.nullMeasurableSet hs0).exists
    with ⟨x, _, hx⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
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 : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
have hx₁ : Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}
Tactic: rw [Nat.frequently_atTop_iff_infinite] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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}
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
have succ : ∀ (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]),
  ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
Tactic: rcases Nat.exists_lt_modEq_of_infinite hx n.succ_pos with ⟨k, hk, l, hl, hkl, hn⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
have H : n + 1 ∣ l - k
Tactic: apply Nat.mul_div_cancel'
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
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)
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
have this : (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
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
have succ : m ≠ 0
Tactic: refine ⟨f^[k] x, hk, m, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
have succ₁ : f^[n + 1]^[m] (f^[k] x) ∈ s
Tactic: refine ⟨f^[k] x, hk, m, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
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
⊢ False
have this₁ : l ≤ k
Tactic: rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this
Cleared hypotheses: this, hm
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
⊢ f^[n + 1]^[m] (f^[k] x) ∈ s
have succ : k ≤ l
Tactic: rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]
-- 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
⊢ EventuallyConst s (ae μ')
have rw : EventuallyConst (g ⁻¹' s) (ae μ)
Tactic: rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]
-- 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
⊢ EventuallyConst (g ⁻¹' s) (ae μ)
have apply : f ⁻¹' g ⁻¹' s = g ⁻¹' s
Tactic: apply hf.aeconst_set (hg.measurable 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 β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw : g ∘ f ⁻¹' 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 β
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
⊢ f ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw₁ : f' ∘ 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 β
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
⊢ f ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw₂ : g ⁻¹' f' ⁻¹' s = g ⁻¹' s
Tactic: rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]