awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
⊢ x ∈ f^[N + m] ⁻¹' s

Tactic:
simpa only [iterate_add] using hmt.1.2

Premises used: Function.iterate_add, And.right, And.left
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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)
N : ℕ
⊢ ∃ m > N, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)

Tactic:
let ⟨m, hm, hmN⟩ :=
    ((hf.frequently_measure_inter_ne_zero hs h0).and_eventually (eventually_gt_atTop N)).exists
  ⟨m, hmN, hm⟩

Premises used: MeasureTheory.Conservative.frequently_measure_inter_ne_zero, Exists, Ne, Nat.iterate, Inter.inter, Filter.Frequently.and_eventually, GT.gt, And, Set.preimage, Filter.Frequently.exists, And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe, _private.0.MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero.match_1, Filter.eventually_gt_atTop
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
by_contra :
  ∀
    (H :
      ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)),
    False
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x : α | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} : ENNReal) (0 : ENNReal)

Tactic:
by_contra H
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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)
simp : NullMeasurableSet (s ∩ ⋂ (i : ℕ), ⋂ (_ : i ≥ n), {a : α | f^[i] a ∈ s}ᶜ) μ
⊢ NullMeasurableSet (s ∩ {x : α | ∀ m ≥ n, f^[m] x ∉ s}) μ

Tactic:
simp only [setOf_forall, ← compl_setOf]

Premises used: Set.setOf_forall, Set.compl_setOf
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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 ∩ ⋂ (i : ℕ), ⋂ (_ : i ≥ n), {a : α | f^[i] a ∈ s}ᶜ) μ

Tactic:
hs.inter <| .biInter (to_countable _) fun m _ ↦
      (hs.preimage <| hf.toQuasiMeasurePreserving.iterate m).compl

Premises used: MeasureTheory.NullMeasurableSet.compl, MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.Measure.QuasiMeasurePreserving.iterate, MeasureTheory.NullMeasurableSet.preimage, MeasureTheory.NullMeasurableSet.inter, Set.to_countable, MeasureTheory.NullMeasurableSet.biInter
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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 ∩ ⋂ (i : ℕ), ⋂ (_ : i ≥ n), {a : α | f^[i] a ∈ s}ᶜ) μ

Tactic:
exact hs.inter <| .biInter (to_countable _) fun m _ ↦
      (hs.preimage <| hf.toQuasiMeasurePreserving.iterate m).compl

Premises used: MeasureTheory.NullMeasurableSet.inter
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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}) μ

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
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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}) μ
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
⊢ False

Tactic:
rcases (hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩

Premises used: MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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)
rcases : ∀ x ∈ s, ∀ (hxn : Membership.mem (γ := Set α) {x : α | ∀ m ≥ n, f^[m] x ∉ s} x) (hxm : f^[m] x ∈ s), False
⊢ False

Tactic:
rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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)
x : α
left : x ∈ s
hxn : Membership.mem (γ := Set α) {x : α | ∀ m ≥ n, f^[m] x ∉ s} x
hxm : f^[m] x ∈ s
⊢ False

Tactic:
hxn m hmn.lt.le hxm

Premises used: GT.gt.lt, LT.lt.le
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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)
x : α
left : x ∈ s
hxn : Membership.mem (γ := Set α) {x : α | ∀ m ≥ n, f^[m] x ∉ s} x
hxm : f^[m] x ∈ s
⊢ False

Tactic:
exact hxn m hmn.lt.le hxm

Premises used: GT.gt.lt, LT.lt.le
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
simp : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, ∀ (a_1 : a ∈ s), ∃ b ≥ i, f^[b] a ∈ s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
simp only [frequently_atTop, @forall_comm (_ ∈ s), ae_all_iff]

Premises used: Filter.frequently_atTop, forall_comm, MeasureTheory.ae_all_iff
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
h : ∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → ∀ (a_2 : a ∈ s), ∃ b ≥ n, f^[b] a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ (a_1 : 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)]

Premises used: Iff.mp, MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero, MeasureTheory.measure_eq_zero_iff_ae_notMem
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → ∀ (a_2 : a ∈ s), ∃ b ≥ n, f^[b] a ∈ s

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ s ∩ {x : α | ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s} =ᶠ[ae μ] s

Tactic:
inter_eventuallyEq_left.2 <| hf.ae_mem_imp_frequently_image_mem hs

Premises used: Iff.mpr, Filter.inter_eventuallyEq_left, MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ {x : α | ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s}) : ENNReal)
    ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
measure_congr (hf.inter_frequently_image_mem_ae_eq hs)

Premises used: MeasureTheory.measure_congr, MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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

Tactic:
ae_all_iff.2 fun k => ?_

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
refine : ∀ (k : ℕ), ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ae_all_iff.2 fun k => ?_

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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

Tactic:
(hf.ae_mem_imp_frequently_image_mem
    (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_

Premises used: MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.Measure.QuasiMeasurePreserving.iterate, MeasureTheory.NullMeasurableSet.preimage, Filter.Eventually.mono, MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
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
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s

Tactic:
refine (hf.ae_mem_imp_frequently_image_mem
    (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_

Premises used: MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.Measure.QuasiMeasurePreserving.iterate, MeasureTheory.NullMeasurableSet.preimage, Filter.Eventually.mono, MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
rw : ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
rw [← map_add_atTop_eq_nat k, frequently_map]

Premises used: Filter.frequently_map, Filter.map_add_atTop_eq_nat
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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

Tactic:
(hx hk).mono fun n hn => ?_

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
refine : ∀ (n : ℕ) (hn : f^[n] x ∈ f^[k] ⁻¹' s), f^[n + k] x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s

Tactic:
refine (hx hk).mono fun n hn => ?_

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
rwa₁ rwa₂ rwa₃ rwa₄ : f^[k] (f^[n] x) ∈ s
⊢ f^[n + k] x ∈ s

Tactic:
rwa [add_comm, iterate_add_apply]

Premises used: Function.iterate_add_apply, add_comm
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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)
⊢ ∃ᵐ (x : α) ∂μ, x ∈ s ∧ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
((frequently_ae_mem_iff.2 h0).and_eventually (hf.ae_mem_imp_frequently_image_mem hs)).mono
    fun _ hx => ⟨hx.1, hx.2 hx.1⟩

Premises used: Iff.mpr, MeasureTheory.frequently_ae_mem_iff, Filter.Frequently.mono, Filter.Frequently.and_eventually, MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem, And.right, And.left, And.intro
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
⊢ ∀ 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
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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

Tactic:
((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_

Premises used: Iff.mpr, TopologicalSpace.countable_countableBasis, MeasureTheory.ae_ball_iff, Filter.Eventually.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
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
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_

Premises used: Iff.mpr, TopologicalSpace.countable_countableBasis, MeasureTheory.ae_ball_iff, Filter.Eventually.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
rcases : ∀ (o : Set α) (hoS : o ∈ countableBasis α) (hxo : x ∈ o) (hos : o ⊆ s), ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
rcases (isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩

Premises used: Iff.mp, TopologicalSpace.isBasis_countableBasis, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
(hx o hoS hxo).mono fun n hn => hos hn

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
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
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
exact (hx o hoS hxo).mono fun n hn => hos hn

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
zero : Conservative f^[0] μ
succ : ∀ (n : ℕ), Conservative f^[n + 1] μ
⊢ Conservative f^[n] μ

Tactic:
rcases n with - | n
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
⊢ Conservative f^[0] μ

Tactic:
Conservative.id μ

Premises used: Nat.iterate, MeasureTheory.Conservative.id
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
⊢ Conservative f^[0] μ

Tactic:
exact Conservative.id μ

Premises used: MeasureTheory.Conservative.id
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n + 1] μ

Tactic:
⟨hf.1.iterate _, fun s hs hs0 => ?_⟩

Premises used: MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.Measure.QuasiMeasurePreserving.iterate, MeasureTheory.Conservative.mk
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
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
⊢ Conservative f^[n + 1] μ

Tactic:
refine ⟨hf.1.iterate _, fun s hs hs0 => ?_⟩
-- 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)
succ : ∀ x ∈ s, ∀ (hx : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s), ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[n + 1]^[m] 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⟩

Premises used: MeasurableSet.nullMeasurableSet, Filter.Frequently.exists, MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem
-- 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 : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ Set.Infinite (α := ℕ) {n : ℕ | f^[n] x ∈ s}

Tactic:
rw [Nat.frequently_atTop_iff_infinite] at hx

Premises used: Nat.frequently_atTop_iff_infinite
-- 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}
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
⊢ ∃ 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⟩

Premises used: Nat.exists_lt_modEq_of_infinite, Nat.succ_pos
-- 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)
H : n + 1 ∣ l - k
⊢ (n + 1) * m = l - k

Tactic:
apply Nat.mul_div_cancel'

Premises used: Nat.mul_div_cancel'
-- 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 ∣ l - k

Tactic:
(Nat.modEq_iff_dvd' hkl.le).1 hn

Premises used: LT.lt.le, Nat.modEq_iff_dvd', Iff.mp
-- 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 ∣ l - k

Tactic:
exact (Nat.modEq_iff_dvd' hkl.le).1 hn

Premises used: LT.lt.le, Nat.modEq_iff_dvd', Iff.mp