internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2020A6.exists_iter_add_large_eq
Proof state before:
f : ℤ → ℤ
h : good f
a : ℤ
k : ℕ
⊢ ∃ N, f^[N + (k + 1)] a = f^[N] (a + ↑(k + 1))
Tactic:
rcases exists_iter_add_large_eq a k with ⟨N, h0⟩
Proof state after:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ ∃ N, f^[N + (k + 1)] a = f^[N] (a + ↑(k + 1))
Theorem: IMOSL.IMO2020A6.exists_iter_add_large_eq
Proof state before:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ ∃ N, f^[N + (k + 1)] a = f^[N] (a + ↑(k + 1))
Tactic:
refine ⟨N + (a + k + 1).natAbs ^ 2, ?_⟩
Proof state after:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ f^[N + (a + ↑k + 1).natAbs ^ 2 + (k + 1)] a = f^[N + (a + ↑k + 1).natAbs ^ 2] (a + ↑(k + 1))
Theorem: IMOSL.IMO2020A6.exists_iter_add_large_eq
Proof state before:
case intro
f : ℤ → ℤ
h : good f
a : ℤ
k N : ℕ
h0 : f^[N + k] a = f^[N] (a + ↑k)
⊢ f^[N + (a + ↑k + 1).natAbs ^ 2 + (k + 1)] a = f^[N + (a + ↑k + 1).natAbs ^ 2] (a + ↑(k + 1))
Tactic:
rw [f.iterate_add_apply N, Nat.cast_succ, ← add_assoc a,
  ← map_iterate_sq_add_one h, Commute.iterate_iterate_self, ← h0,
  ← iterate_add_apply, add_comm _ (N + k), add_add_add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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)
Proof state after:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ N, 0 < minimalPeriod f (f^[N] 0)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩]
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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 ?_⟩
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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]
Proof 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))
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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 ?_ _
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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']
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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)
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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|
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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 ↦ ?_)⟩
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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]
Proof 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)
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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]
Proof state after:
f : ℤ → ℤ
h : good f
h0 : ¬Injective f
⊢ ∃ a b, a < b ∧ f a = f b
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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, ?_⟩
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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
Proof 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
Theorem: IMOSL.IMO2020A6.orbit_zero_bdd_of_not_injective
Proof 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⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
h0 : ∃ M, ∀ (n : ℕ), |f^[n] 0| < M
⊢ f = 0
Tactic:
rcases h0 with ⟨M, h0⟩
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
⊢ f = 0
Tactic:
have h1 (a : ℤ) : f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a)) := by
  have h := h a (-a); rwa [a.natAbs_neg, add_neg_self,
    ← two_mul, neg_mul, ← sub_eq_add_neg, ← mul_sub] at h
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f = 0
Tactic:
replace h0 (a : ℤ) (h2 : M ≤ a) : f.IsPeriodicPt (2 * a.natAbs ^ 2) 0 :=
  Int.eq_zero_of_abs_lt_dvd ⟨_, h1 a⟩ ((h0 _).trans_le h2)
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
⊢ f = 0
Tactic:
replace h0 : f.IsPeriodicPt 2 0 := by
  have h2 := (h0 _ M.le_refl).gcd (h0 _ M.lt_succ.le)
  have h3 : IsCoprime M (M + 1) :=
    ⟨-1, 1, by rw [one_mul, neg_one_mul, neg_add_cancel_left]⟩
  rwa [Nat.gcd_mul_left, ← Int.natAbs_pow, ← Int.natAbs_pow,
    ← Int.gcd_eq_natAbs, Int.gcd_eq_one_iff_coprime.mpr h3.pow, mul_one] at h2
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : IsPeriodicPt f 2 0
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : IsPeriodicPt f 2 0
⊢ f = 0
Tactic:
replace h1 (a : ℤ) (h3 : a ≠ 0) : f a = f (-a) := by
  specialize h1 a
  rw [h0.mul_const, zero_eq_mul] at h1
  exact eq_of_sub_eq_zero (h1.resolve_left h3)
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ f = 0
Tactic:
suffices h2 : ∀ a : ℤ, a ≠ 0 → f a = 0 by
  have h3 : f (f 2) = 1 * f 1 + 1 * f 1 := h 1 1
  rw [h2 1 one_ne_zero, h2 _ two_ne_zero] at h3
  exact funext λ a ↦ (ne_or_eq a 0).elim (h2 a) (λ h4 ↦ h4.symm ▸ h3)
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ ∀ (a : ℤ), a ≠ 0 → f a = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
⊢ ∀ (a : ℤ), a ≠ 0 → f a = 0
Tactic:
intro a h2
Proof state after:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
⊢ f a = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
⊢ f a = 0
Tactic:
obtain ⟨n, h3⟩ : ∃ n : ℕ, a.natAbs ^ 2 = n.succ :=
  Nat.exists_eq_succ_of_ne_zero (pow_ne_zero 2 <| Int.natAbs_ne_zero.mpr h2)
Proof state after:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
⊢ f a = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
⊢ f a = 0
Tactic:
have h4 := map_iterate_sq h (-a)
Proof state after:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : f^[(-a).natAbs ^ 2] (-a) = -a * f (-a)
⊢ f a = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : f^[(-a).natAbs ^ 2] (-a) = -a * f (-a)
⊢ f a = 0
Tactic:
rw [Int.natAbs_neg, h3, iterate_succ_apply, ← h1 a h2, ← iterate_succ_apply,
  ← h3, map_iterate_sq h, neg_mul, eq_neg_self_iff, mul_eq_zero] at h4
Proof state after:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : a = 0 ∨ f a = 0
⊢ f a = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
case intro.intro
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
a : ℤ
h2 : a ≠ 0
n : ℕ
h3 : a.natAbs ^ 2 = n.succ
h4 : a = 0 ∨ f a = 0
⊢ f a = 0
Tactic:
exact h4.resolve_left h2
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
a : ℤ
⊢ f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
Tactic:
have h := h a (-a)
Proof state after:
f : ℤ → ℤ
h✝ : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
a : ℤ
h : f^[a.natAbs ^ 2 + (-a).natAbs ^ 2] (a + -a) = a * f a + -a * f (-a)
⊢ f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h✝ : good f
M : ℤ
h0 : ∀ (n : ℕ), |f^[n] 0| < M
a : ℤ
h : f^[a.natAbs ^ 2 + (-a).natAbs ^ 2] (a + -a) = a * f a + -a * f (-a)
⊢ f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
Tactic:
rwa [a.natAbs_neg, add_neg_self,
← two_mul, neg_mul, ← sub_eq_add_neg, ← mul_sub] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
⊢ IsPeriodicPt f 2 0
Tactic:
have h2 := (h0 _ M.le_refl).gcd (h0 _ M.lt_succ.le)
Proof state after:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
⊢ IsPeriodicPt f 2 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
⊢ IsPeriodicPt f 2 0
Tactic:
have h3 : IsCoprime M (M + 1) :=
  ⟨-1, 1, by rw [one_mul, neg_one_mul, neg_add_cancel_left]⟩
Proof state after:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
h3 : IsCoprime M (M + 1)
⊢ IsPeriodicPt f 2 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
h3 : IsCoprime M (M + 1)
⊢ IsPeriodicPt f 2 0
Tactic:
rwa [Nat.gcd_mul_left, ← Int.natAbs_pow, ← Int.natAbs_pow,
  ← Int.gcd_eq_natAbs, Int.gcd_eq_one_iff_coprime.mpr h3.pow, mul_one] at h2
Proof state after:
no goals