Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two (Compfiles/Imo2006P5.lean)

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
let C : Cycle ℤ := (periodicOrbit (fun x => P.eval x) t).map fun x => P.eval x - x
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have HC : ∀ {n : ℕ}, (fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t ∈ C := by
  intro n
  rw [Cycle.mem_map, Function.iterate_succ_apply']
  exact ⟨_, iterate_mem_periodicOrbit ht n, rfl⟩
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have Habs :
  ∀ m n : ℕ,
    ((fun x => P.eval x)^[m + 1] t - (fun x => P.eval x)^[m] t).natAbs =
      ((fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t).natAbs :=
  fun m n => Int.natAbs_eq_of_chain_dvd Hdvd HC HC
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
⊢ ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Tactic:
intro n
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Tactic:
rw [Cycle.mem_map, Function.iterate_succ_apply']
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ ∃ a ∈ periodicOrbit (fun x => Polynomial.eval x P) t,
    Polynomial.eval a P - a =
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ ∃ a ∈ periodicOrbit (fun x => Polynomial.eval x P) t,
    Polynomial.eval a P - a =
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t
Tactic:
exact ⟨_, iterate_mem_periodicOrbit ht n, rfl⟩
State after:
no goals

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ Cycle.Chain (fun x x_1 => x ∣ x_1) C
Tactic:
rw [Cycle.chain_map, periodicOrbit_chain' _ ht]
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ ∀ (n : ℕ),
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ ∀ (n : ℕ),
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Tactic:
intro n
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
n : ℕ
⊢ Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
n : ℕ
⊢ Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Tactic:
convert sub_dvd_eval_sub ((fun x => P.eval x)^[n + 1] t) ((fun x => P.eval x)^[n] t) P <;>
  rw [Function.iterate_succ_apply']
State after:
no goals

State before:
case pos
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have Heq :
  ∀ m n : ℕ,
    (fun x => P.eval x)^[m + 1] t - (fun x => P.eval x)^[m] t =
      (fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t :=
  fun m n => Cycle.chain_iff_pairwise.1 HC' _ HC _ HC
State after:
case pos
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case pos
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
rcases ht with ⟨_ | k, hk, hk'⟩
State after:
case pos.intro.zero.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
hk : 0 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) 0 t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
⊢ ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
Tactic:
intro n
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
⊢ ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
⊢ ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
Tactic:
induction' n with n IH
State after:
case zero
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
⊢ ((fun x => Polynomial.eval x P)^[0 + 1] t - t).sign = (Polynomial.eval t P - t).sign

case succ
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ ((fun x => Polynomial.eval x P)^[n + 1 + 1] t - t).sign = (Polynomial.eval t P - t).sign

State before:
case zero
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
⊢ ((fun x => Polynomial.eval x P)^[0 + 1] t - t).sign = (Polynomial.eval t P - t).sign
Tactic:
rfl
State after:
no goals

State before:
case succ
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ ((fun x => Polynomial.eval x P)^[n + 1 + 1] t - t).sign = (Polynomial.eval t P - t).sign
Tactic:
apply Eq.trans _ (Int.sign_add_eq_of_sign_eq IH)
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ ((fun x => Polynomial.eval x P)^[n + 1 + 1] t - t).sign =
    ((fun x => Polynomial.eval x P)^[n + 1] t - t + (Polynomial.eval t P - t)).sign

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ ((fun x => Polynomial.eval x P)^[n + 1 + 1] t - t).sign =
    ((fun x => Polynomial.eval x P)^[n + 1] t - t + (Polynomial.eval t P - t)).sign
Tactic:
have H := Heq n.succ 0
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
H :
  (fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t =
    (fun x => Polynomial.eval x P)^[0 + 1] t - (fun x => Polynomial.eval x P)^[0] t
⊢ ((fun x => Polynomial.eval x P)^[n + 1 + 1] t - t).sign =
    ((fun x => Polynomial.eval x P)^[n + 1] t - t + (Polynomial.eval t P - t)).sign

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
H :
  (fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t =
    (fun x => Polynomial.eval x P)^[0 + 1] t - (fun x => Polynomial.eval x P)^[0] t
⊢ ((fun x => Polynomial.eval x P)^[n + 1 + 1] t - t).sign =
    ((fun x => Polynomial.eval x P)^[n + 1] t - t + (Polynomial.eval t P - t)).sign
Tactic:
dsimp at H ⊢
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
H :
  (fun x => Polynomial.eval x P)^[n] (Polynomial.eval (Polynomial.eval t P) P) -
      (fun x => Polynomial.eval x P)^[n] (Polynomial.eval t P) =
    Polynomial.eval t P - t
⊢ ((fun x => Polynomial.eval x P)^[n] (Polynomial.eval (Polynomial.eval t P) P) - t).sign =
    ((fun x => Polynomial.eval x P)^[n] (Polynomial.eval t P) - t + (Polynomial.eval t P - t)).sign

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
H :
  (fun x => Polynomial.eval x P)^[n] (Polynomial.eval (Polynomial.eval t P) P) -
      (fun x => Polynomial.eval x P)^[n] (Polynomial.eval t P) =
    Polynomial.eval t P - t
⊢ ((fun x => Polynomial.eval x P)^[n] (Polynomial.eval (Polynomial.eval t P) P) - t).sign =
    ((fun x => Polynomial.eval x P)^[n] (Polynomial.eval t P) - t + (Polynomial.eval t P - t)).sign
Tactic:
rw [← H, sub_add_sub_cancel']
State after:
no goals

State before:
case pos.intro.zero.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
hk : 0 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) 0 t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
exact (irrefl 0 hk).elim
State after:
no goals

State before:
case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have H := IH k
State after:
case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
H : ((fun x => Polynomial.eval x P)^[k + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
H : ((fun x => Polynomial.eval x P)^[k + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
rw [hk'.isFixedPt.eq, sub_self, Int.sign_zero, eq_comm, Int.sign_eq_zero_iff_zero,
  sub_eq_zero] at H
State after:
case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
H : Polynomial.eval t P = t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
H : Polynomial.eval t P = t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
simp [IsPeriodicPt, IsFixedPt, H]
State after:
no goals

State before:
case neg
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : ¬Cycle.Chain (fun x x_1 => x = x_1) C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
rw [Cycle.chain_map, periodicOrbit_chain' _ ht] at HC'
State after:
case neg
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' :
  ¬∀ (n : ℕ),
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t =
        Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case neg
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' :
  ¬∀ (n : ℕ),
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t =
        Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
push_neg at HC'
State after:
case neg
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' :
  ∃ n,
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case neg
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' :
  ∃ n,
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
cases' HC' with n hn
State after:
case neg.intro
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case neg.intro
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
cases' Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' hn'
State after:
case neg.intro.inl
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t =
    (fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

case neg.intro.inr
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t =
    -((fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case neg.intro.inl
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t =
    (fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
apply (hn _).elim
State after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t =
    (fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t
⊢ Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t =
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t

State before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t =
    (fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t
⊢ Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t =
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Tactic:
convert hn' <;> simp only [Function.iterate_succ_apply']
State after:
no goals

State before:
case neg.intro.inr
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t =
    -((fun x => Polynomial.eval x P)^[n.succ + 1] t - (fun x => Polynomial.eval x P)^[n.succ] t)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
rw [neg_sub, sub_right_inj] at hn'
State after:
case neg.intro.inr
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' : (fun x => Polynomial.eval x P)^[n] t = (fun x => Polynomial.eval x P)^[n.succ + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case neg.intro.inr
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' : (fun x => Polynomial.eval x P)^[n] t = (fun x => Polynomial.eval x P)^[n.succ + 1] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
simp only [Function.iterate_succ_apply'] at hn'
State after:
case neg.intro.inr
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n] t = Polynomial.eval (Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P) P
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

State before:
case neg.intro.inr
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
n : ℕ
hn :
  Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ≠
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
hn' :
  (fun x => Polynomial.eval x P)^[n] t = Polynomial.eval (Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P) P
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
exact isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate ht hn'.symm
State after:
no goals