internlm/Lean-Github huggingface dataset:
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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
Proof 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
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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'
Proof 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
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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
Proof 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
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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']
Proof state after:
no goals
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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'
Proof 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
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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'
Proof 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
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof 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
Proof state after:
no goals
Theorem: Imo2006P5.Polynomial.iterate_comp_sub_X_ne
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ P.comp^[k] X - X ≠ 0
Tactic:
rw [sub_ne_zero]
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ P.comp^[k] X ≠ X
Theorem: Imo2006P5.Polynomial.iterate_comp_sub_X_ne
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ P.comp^[k] X ≠ X
Tactic:
apply_fun natDegree
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ (P.comp^[k] X).natDegree ≠ X.natDegree
Theorem: Imo2006P5.Polynomial.iterate_comp_sub_X_ne
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ (P.comp^[k] X).natDegree ≠ X.natDegree
Tactic:
simpa using (one_lt_pow hP hk.ne').ne'
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
have hPX : (P - X).natDegree = P.natDegree := by
  rw [natDegree_sub_eq_left_of_natDegree_lt]
  simpa using hP
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
have hPX' : P - X ≠ 0 := by
  intro h
  rw [h, natDegree_zero] at hPX
  rw [← hPX] at hP
  exact (zero_le_one.not_lt hP).elim
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
by_cases H : (P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
Proof state after:
case pos
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : (P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree

case neg
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ (P - X).natDegree = P.natDegree
Tactic:
rw [natDegree_sub_eq_left_of_natDegree_lt]
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ X.natDegree < P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ X.natDegree < P.natDegree
Tactic:
simpa using hP
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
⊢ P - X ≠ 0
Tactic:
intro h
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
h : P - X = 0
⊢ False
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
h : P - X = 0
⊢ False
Tactic:
rw [h, natDegree_zero] at hPX
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False
Tactic:
rw [← hPX] at hP
Proof state after:
P : ℤ[X]
hP : 1 < 0
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < 0
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False
Tactic:
exact (zero_le_one.not_lt hP).elim
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case pos
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : (P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
exact (Finset.card_le_card H).trans
  ((Multiset.toFinset_card_le _).trans ((card_roots' _).trans_eq hPX))
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
rcases Finset.not_subset.1 H with ⟨a, ha, hab⟩
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
ha : a ∈ (P.comp P - X).roots.toFinset
hab : a ∉ (P - X).roots.toFinset
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
ha : a ∈ (P.comp P - X).roots.toFinset
hab : a ∉ (P - X).roots.toFinset
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
replace ha := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ha)
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
hab : a ∉ (P - X).roots.toFinset
ha : (P.comp P - X).IsRoot a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
hab : a ∉ (P - X).roots.toFinset
ha : (P.comp P - X).IsRoot a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ha
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
hab : a ∉ (P - X).roots.toFinset
ha : Polynomial.eval (Polynomial.eval a P) P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
hab : a ∉ (P - X).roots.toFinset
ha : Polynomial.eval (Polynomial.eval a P) P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
rw [Multiset.mem_toFinset, mem_roots hPX', IsRoot.def, eval_sub, eval_X, sub_eq_zero] at hab
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
hab : ¬Polynomial.eval a P = a
ha : Polynomial.eval (Polynomial.eval a P) P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
hab : ¬Polynomial.eval a P = a
ha : Polynomial.eval (Polynomial.eval a P) P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
set b := P.eval a
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
have hPab : (P + (X : ℤ[X]) - a - b).natDegree = P.natDegree := by
  rw [sub_sub, ← Int.cast_add]
  have h₁ : (P + X).natDegree = P.natDegree := by
    rw [natDegree_add_eq_left_of_natDegree_lt]
    simpa using hP
  rwa [natDegree_sub_eq_left_of_natDegree_lt]
  rw [h₁, natDegree_intCast]
  exact zero_lt_one.trans hP
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
have hPab' : P + (X : ℤ[X]) - a - b ≠ 0 := by
  intro h
  rw [h, natDegree_zero] at hPab
  rw [← hPab] at hP
  exact (zero_le_one.not_lt hP).elim
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
Tactic:
suffices H' : (P.comp P - X).roots.toFinset ⊆ (P + (X : ℤ[X]) - a - b).roots.toFinset from
  (Finset.card_le_card H').trans
    ((Multiset.toFinset_card_le _).trans <| (card_roots' _).trans_eq hPab)
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
⊢ (P.comp P - X).roots.toFinset ⊆ (P + X - ↑a - ↑b).roots.toFinset