case zero
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
⊢ Conservative (f^[Nat.zero]) μ

case succ
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative (f^[Nat.succ n]) μ
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative (f^[n]) μ
cases' n with n
case succ
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
case succ
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative (f^[Nat.succ n]) μ
refine' ⟨hf.1.iterate _, fun s hs hs0 => _⟩
case succ.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
case succ
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
rcases(hf.frequently_ae_mem_and_frequently_image_mem hs hs0).exists with ⟨x, _, hx⟩
case succ.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
case succ.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
rw [Nat.frequently_atTop_iff_infinite] at hx
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
case succ.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
rcases Nat.exists_lt_modEq_of_infinite hx n.succ_pos with ⟨k, hk, l, hl, hkl, hn⟩
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
set m := (l - k) / (n + 1)
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
have : (n + 1) * m = l - k := by
  apply Nat.mul_div_cancel'
  exact (Nat.modEq_iff_dvd' hkl.le).1 hn
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0

case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ (f^[Nat.succ n]^[m]) ((f^[k]) x) ∈ s
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[Nat.succ n]^[m]) x ∈ s
refine' ⟨(f^[k]) x, hk, m, _, _⟩
no goals
case zero
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
⊢ Conservative (f^[Nat.zero]) μ
exact Conservative.id μ
case H
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ n + 1 ∣ l - k
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ (n + 1) * m = l - k
apply Nat.mul_div_cancel'
no goals
case H
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ n + 1 ∣ l - k
exact (Nat.modEq_iff_dvd' hkl.le).1 hn
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
⊢ False
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0
intro hm
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
⊢ False
rw [hm, MulZeroClass.mul_zero, eq_comm, tsub_eq_zero_iff_le] at this
no goals
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False
exact this.not_lt hkl
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ (f^[Nat.succ n]^[m]) ((f^[k]) x) ∈ s
rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]
no goals
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type ?u.77532
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | (f^[n]) x ∈ s}
k : ℕ
hk : k ∈ {n | (f^[n]) x ∈ s}
l : ℕ
hl : l ∈ {n | (f^[n]) x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l
exact hkl.le