Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective (IMOSLLean4/IMO2020/A6/A6.lean)

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
Tactic:
suffices ∃ N : ℕ, 0 < f.minimalPeriod (f^[N] 0) by
  rcases this with ⟨N, h1⟩
  let k := f.minimalPeriod (f^[N] 0)
  let F := λ n ↦ |f^[n] 0|
  refine ⟨Extra.seqMax F (N + k) + 1, λ n ↦ Int.lt_add_one_of_le <|
    (n.le_total (N + k)).elim (Extra.le_seqMax_of_le F) (λ h2 ↦ ?_)⟩
  rw [le_iff_exists_add] at h2; rcases h2 with ⟨c, rfl⟩
  rw [add_rotate, iterate_add_apply, ← iterate_mod_minimalPeriod_eq,
    Nat.add_mod_left, ← iterate_add_apply, add_comm]
  exact Extra.le_seqMax_of_le F (add_le_add_left (c.mod_lt h1).le N)
State after:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)
Tactic:
obtain ⟨a, k, h1, h2⟩ : ∃ (a : ℤ) (k : ℕ), 0 < k ∧ f (a + k) = f a := by
  suffices ∃ a b, a < b ∧ f a = f b by
    rcases this with ⟨a, b, h1, h2⟩
    apply sub_pos_of_lt at h1
    refine ⟨a, (b - a).natAbs, Int.natAbs_pos.mpr h1.ne.symm, ?_⟩
    rw [Int.natCast_natAbs, abs_of_pos h1, add_sub_cancel, h2]
  simp_rw [Injective, not_forall] at h0
  rcases h0 with ⟨a, b, h0, h1⟩
  rcases ne_iff_lt_or_gt.mp h1 with h2 | h2
  exacts [⟨a, b, h2, h0⟩, ⟨b, a, h2, h0.symm⟩]
State after:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)

State before:
case intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)
Tactic:
rcases exists_iter_add_large_eq h a k with ⟨N, h4⟩
State after:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)

State before:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)
Tactic:
refine ⟨N + 1 + M, IsPeriodicPt.minimalPeriod_pos h1 ?_⟩
State after:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ IsPeriodicPt f k (f^[N + 1 + M] 0)

State before:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ IsPeriodicPt f k (f^[N + 1 + M] 0)
Tactic:
rw [iterate_add_apply, ← h3, Commute.iterate_iterate_self]
State after:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ IsPeriodicPt f k (f^[K] (f^[N + 1] a))

State before:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ IsPeriodicPt f k (f^[K] (f^[N + 1] a))
Tactic:
refine IsPeriodicPt.apply_iterate ?_ _
State after:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ IsPeriodicPt f k (f^[N + 1] a)

State before:
case intro.intro.intro.intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
K M : ℕ
h3 : f^[K] a = f^[M] 0
N : ℕ
h4 : f^[N + k] a = f^[N] (a + ↑k)
⊢ IsPeriodicPt f k (f^[N + 1] a)
Tactic:
rw [IsPeriodicPt, IsFixedPt, ← iterate_add_apply,
  iterate_succ_apply, ← h2, Commute.iterate_self, ← h4,
  add_left_comm, ← add_assoc, iterate_succ_apply']
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
this : ∃ N, 0 < minimalPeriod f (f^[N] 0)
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
Tactic:
rcases this with ⟨N, h1⟩
State after:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M

State before:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
Tactic:
let k := f.minimalPeriod (f^[N] 0)
State after:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M

State before:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
Tactic:
let F := λ n ↦ |f^[n] 0|
State after:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M

State before:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
⊢ ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
Tactic:
refine ⟨Extra.seqMax F (N + k) + 1, λ n ↦ Int.lt_add_one_of_le <|
  (n.le_total (N + k)).elim (Extra.le_seqMax_of_le F) (λ h2 ↦ ?_)⟩
State after:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
n : ℕ
h2 : N + k ≤ n
⊢ |f^[n] 0| ≤ Extra.seqMax F (N + k)

State before:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
n : ℕ
h2 : N + k ≤ n
⊢ |f^[n] 0| ≤ Extra.seqMax F (N + k)
Tactic:
rw [le_iff_exists_add] at h2
State after:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
n : ℕ
h2 : ∃ c, n = N + k + c
⊢ |f^[n] 0| ≤ Extra.seqMax F (N + k)

State before:
case intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
n : ℕ
h2 : ∃ c, n = N + k + c
⊢ |f^[n] 0| ≤ Extra.seqMax F (N + k)
Tactic:
rcases h2 with ⟨c, rfl⟩
State after:
case intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
c : ℕ
⊢ |f^[N + k + c] 0| ≤ Extra.seqMax F (N + k)

State before:
case intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
c : ℕ
⊢ |f^[N + k + c] 0| ≤ Extra.seqMax F (N + k)
Tactic:
rw [add_rotate, iterate_add_apply, ← iterate_mod_minimalPeriod_eq,
  Nat.add_mod_left, ← iterate_add_apply, add_comm]
State after:
case intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
c : ℕ
⊢ |f^[N + c % k] 0| ≤ Extra.seqMax F (N + k)

State before:
case intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
N : ℕ
h1 : 0 < minimalPeriod f (f^[N] 0)
k : ℕ := minimalPeriod f (f^[N] 0)
F : ℕ → ℤ := fun n => |f^[n] 0|
c : ℕ
⊢ |f^[N + c % k] 0| ≤ Extra.seqMax F (N + k)
Tactic:
exact Extra.le_seqMax_of_le F (add_le_add_left (c.mod_lt h1).le N)
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ a k, 0 < k ∧ f (a + ↑k) = f a
Tactic:
suffices ∃ a b, a < b ∧ f a = f b by
  rcases this with ⟨a, b, h1, h2⟩
  apply sub_pos_of_lt at h1
  refine ⟨a, (b - a).natAbs, Int.natAbs_pos.mpr h1.ne.symm, ?_⟩
  rw [Int.natCast_natAbs, abs_of_pos h1, add_sub_cancel, h2]
State after:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ a b, a < b ∧ f a = f b

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ a b, a < b ∧ f a = f b
Tactic:
simp_rw [Injective, not_forall] at h0
State after:
f : ℤ → ℤ
h : good f
h0 : ∃ x x_1, ∃ (_ : f x = f x_1), ¬x = x_1
⊢ ∃ a b, a < b ∧ f a = f b

State before:
f : ℤ → ℤ
h : good f
h0 : ∃ x x_1, ∃ (_ : f x = f x_1), ¬x = x_1
⊢ ∃ a b, a < b ∧ f a = f b
Tactic:
rcases h0 with ⟨a, b, h0, h1⟩
State after:
case intro.intro.intro
f : ℤ → ℤ
h : good f
a b : ℤ
h0 : f a = f b
h1 : ¬a = b
⊢ ∃ a b, a < b ∧ f a = f b

State before:
case intro.intro.intro
f : ℤ → ℤ
h : good f
a b : ℤ
h0 : f a = f b
h1 : ¬a = b
⊢ ∃ a b, a < b ∧ f a = f b
Tactic:
rcases ne_iff_lt_or_gt.mp h1 with h2 | h2
State after:
case intro.intro.intro.inl
f : ℤ → ℤ
h : good f
a b : ℤ
h0 : f a = f b
h1 : ¬a = b
h2 : a < b
⊢ ∃ a b, a < b ∧ f a = f b

case intro.intro.intro.inr
f : ℤ → ℤ
h : good f
a b : ℤ
h0 : f a = f b
h1 : ¬a = b
h2 : a > b
⊢ ∃ a b, a < b ∧ f a = f b

State before:
case intro.intro.intro.inl
f : ℤ → ℤ
h : good f
a b : ℤ
h0 : f a = f b
h1 : ¬a = b
h2 : a < b
⊢ ∃ a b, a < b ∧ f a = f b

case intro.intro.intro.inr
f : ℤ → ℤ
h : good f
a b : ℤ
h0 : f a = f b
h1 : ¬a = b
h2 : a > b
⊢ ∃ a b, a < b ∧ f a = f b
Tactic:
exacts [⟨a, b, h2, h0⟩, ⟨b, a, h2, h0.symm⟩]
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
this : ∃ a b, a < b ∧ f a = f b
⊢ ∃ a k, 0 < k ∧ f (a + ↑k) = f a
Tactic:
rcases this with ⟨a, b, h1, h2⟩
State after:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a b : ℤ
h1 : a < b
h2 : f a = f b
⊢ ∃ a k, 0 < k ∧ f (a + ↑k) = f a

State before:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a b : ℤ
h1 : a < b
h2 : f a = f b
⊢ ∃ a k, 0 < k ∧ f (a + ↑k) = f a
Tactic:
apply sub_pos_of_lt at h1
State after:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a b : ℤ
h2 : f a = f b
h1 : 0 < b - a
⊢ ∃ a k, 0 < k ∧ f (a + ↑k) = f a

State before:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a b : ℤ
h2 : f a = f b
h1 : 0 < b - a
⊢ ∃ a k, 0 < k ∧ f (a + ↑k) = f a
Tactic:
refine ⟨a, (b - a).natAbs, Int.natAbs_pos.mpr h1.ne.symm, ?_⟩
State after:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a b : ℤ
h2 : f a = f b
h1 : 0 < b - a
⊢ f (a + ↑(b - a).natAbs) = f a

State before:
case intro.intro.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a b : ℤ
h2 : f a = f b
h1 : 0 < b - a
⊢ f (a + ↑(b - a).natAbs) = f a
Tactic:
rw [Int.natCast_natAbs, abs_of_pos h1, add_sub_cancel, h2]
State after:
no goals

State before:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
rcases le_total a 0 with h3 | h3
State after:
case inl
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : a ≤ 0
⊢ ∃ K M, f^[K] a = f^[M] 0

case inr
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : 0 ≤ a
⊢ ∃ K M, f^[K] a = f^[M] 0

State before:
case inl
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : a ≤ 0
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
rcases exists_iter_add_large_eq h a a.natAbs with ⟨N, h4⟩
State after:
case inl.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : a ≤ 0
N : ℕ
h4 : f^[N + a.natAbs] a = f^[N] (a + ↑a.natAbs)
⊢ ∃ K M, f^[K] a = f^[M] 0

State before:
case inl.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : a ≤ 0
N : ℕ
h4 : f^[N + a.natAbs] a = f^[N] (a + ↑a.natAbs)
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
rw [Int.natCast_natAbs, abs_of_nonpos h3, add_neg_self] at h4
State after:
case inl.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : a ≤ 0
N : ℕ
h4 : f^[N + a.natAbs] a = f^[N] 0
⊢ ∃ K M, f^[K] a = f^[M] 0

State before:
case inl.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : a ≤ 0
N : ℕ
h4 : f^[N + a.natAbs] a = f^[N] 0
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
exact ⟨_, _, h4⟩
State after:
no goals

State before:
case inr
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : 0 ≤ a
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
rcases exists_iter_add_large_eq h 0 a.natAbs with ⟨N, h4⟩
State after:
case inr.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : 0 ≤ a
N : ℕ
h4 : f^[N + a.natAbs] 0 = f^[N] (0 + ↑a.natAbs)
⊢ ∃ K M, f^[K] a = f^[M] 0

State before:
case inr.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : 0 ≤ a
N : ℕ
h4 : f^[N + a.natAbs] 0 = f^[N] (0 + ↑a.natAbs)
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
rw [Int.natCast_natAbs, abs_of_nonneg h3, zero_add] at h4
State after:
case inr.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : 0 ≤ a
N : ℕ
h4 : f^[N + a.natAbs] 0 = f^[N] a
⊢ ∃ K M, f^[K] a = f^[M] 0

State before:
case inr.intro
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
a : ℤ
k : ℕ
h1 : 0 < k
h2 : f (a + ↑k) = f a
h3 : 0 ≤ a
N : ℕ
h4 : f^[N + a.natAbs] 0 = f^[N] a
⊢ ∃ K M, f^[K] a = f^[M] 0
Tactic:
exact ⟨_, _, h4.symm⟩
State after:
no goals