ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ¬∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
⊢ False
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
⊢ ∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
by_contra H
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ∃ a, ∀ (b : ℕ), b ≥ a → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ¬∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
⊢ False
simp only [not_frequently, eventually_atTop, Ne.def, Classical.not_not] at H
case intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ∃ a, ∀ (b : ℕ), b ≥ a → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
rcases H with ⟨N, hN⟩
case intro.zero
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False

case intro.succ
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : (∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0) → False
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
case intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
induction' N with N ihN
case intro.succ
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : ¬∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
case intro.succ
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : (∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0) → False
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
rw [imp_false] at ihN
case intro.succ
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
ihN : ∃ b, b ≥ N ∧ ↑↑μ (s ∩ f^[b] ⁻¹' s) ≠ 0
⊢ False
case intro.succ
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : ¬∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
push_neg  at ihN
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
⊢ False
case intro.succ
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
ihN : ∃ b, b ≥ N ∧ ↑↑μ (s ∩ f^[b] ⁻¹' s) ≠ 0
⊢ False
rcases ihN with ⟨n, hn, hμn⟩
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
⊢ False
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
⊢ False
set T := s ∩ ⋃ n ≥ N + 1, f^[n] ⁻¹' s
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ False
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
⊢ False
have hT : MeasurableSet T :=
  hs.inter (MeasurableSet.biUnion (to_countable _) fun _ _ => hf.measurable.iterate _ hs)
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ False
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ False
have hμT : μ T = 0 := by
  convert(measure_biUnion_null_iff <| to_countable _).2 hN
  rw [← inter_iUnion₂]
  rfl
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
⊢ False
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ False
have : μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0 := by rwa [measure_diff_null hμT]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬(f^[m]) x ∈ T
left✝ : (f^[m]) x ∈ s
hxm : (f^[m]) x ∈ f^[n] ⁻¹' s
⊢ False
case intro.succ.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
⊢ False
rcases hf.exists_mem_image_mem ((hs.inter (hf.measurable.iterate n hs)).diff hT) this with
  ⟨x, ⟨⟨hxs, _⟩, hxT⟩, m, hm0, ⟨_, hxm⟩, _⟩
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬(f^[m]) x ∈ T
left✝ : (f^[m]) x ∈ s
hxm : (f^[m]) x ∈ f^[n] ⁻¹' s
⊢ n + m ≥ N + 1

case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬(f^[m]) x ∈ T
left✝ : (f^[m]) x ∈ s
hxm : (f^[m]) x ∈ f^[n] ⁻¹' s
⊢ x ∈ f^[n + m] ⁻¹' s
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬(f^[m]) x ∈ T
left✝ : (f^[m]) x ∈ s
hxm : (f^[m]) x ∈ f^[n] ⁻¹' s
⊢ False
refine' hxT ⟨hxs, mem_iUnion₂.2 ⟨n + m, _, _⟩⟩
case intro.zero
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ ↑↑μ s = 0
case intro.zero
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
apply h0
no goals
case intro.zero
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ ↑↑μ s = 0
simpa using hN 0 le_rfl
case h.e'_2.h.e'_3
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), s ∩ f^[i] ⁻¹' s
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ ↑↑μ T = 0
convert(measure_biUnion_null_iff <| to_countable _).2 hN
case h.e'_2.h.e'_3
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = s ∩ ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), f^[i] ⁻¹' s
case h.e'_2.h.e'_3
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), s ∩ f^[i] ⁻¹' s
rw [← inter_iUnion₂]
no goals
case h.e'_2.h.e'_3
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = s ∩ ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), f^[i] ⁻¹' s
rfl
no goals
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
rwa [measure_diff_null hμT]
no goals
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬(f^[m]) x ∈ T
left✝ : (f^[m]) x ∈ s
hxm : (f^[m]) x ∈ f^[n] ⁻¹' s
⊢ n + m ≥ N + 1
exact add_le_add hn (Nat.one_le_of_lt <| pos_iff_ne_zero.2 hm0)
no goals
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type ?u.54331
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬(f^[m]) x ∈ T
left✝ : (f^[m]) x ∈ s
hxm : (f^[m]) x ∈ f^[n] ⁻¹' s
⊢ x ∈ f^[n + m] ⁻¹' s
rwa [Set.mem_preimage, ← iterate_add_apply] at hxm