ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
⊢ False
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
by_contra H
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
⊢ False
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
⊢ False
have : MeasurableSet (s ∩ { x | ∀ m ≥ n, (f^[m]) x ∉ s }) := by
  simp only [setOf_forall, ← compl_setOf]
  exact
    hs.inter (MeasurableSet.biInter (to_countable _) fun m _ => hf.measurable.iterate m hs.compl)
case intro.intro
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})) ≠ 0
⊢ False
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
⊢ False
rcases(hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩
case intro.intro.intro.intro.intro.intro
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})) ≠ 0
x : α
left✝ : x ∈ s
hxn : x ∈ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s}
hxm : (f^[m]) x ∈ s
⊢ False
case intro.intro
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})) ≠ 0
⊢ False
rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩
no goals
case intro.intro.intro.intro.intro.intro
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})) ≠ 0
x : α
left✝ : x ∈ s
hxn : x ∈ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s}
hxm : (f^[m]) x ∈ s
⊢ False
exact hxn m hmn.lt.le hxm
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
⊢ MeasurableSet (s ∩ ⋂ (i : ℕ) (_ : i ≥ n), {a | (f^[i]) a ∈ s}ᶜ)
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
⊢ MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s})
simp only [setOf_forall, ← compl_setOf]
no goals
ι : Type ?u.62235
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬(f^[m]) x ∈ s} = 0
⊢ MeasurableSet (s ∩ ⋂ (i : ℕ) (_ : i ≥ n), {a | (f^[i]) a ∈ s}ᶜ)
exact
  hs.inter (MeasurableSet.biInter (to_countable _) fun m _ => hf.measurable.iterate m hs.compl)