Theorem: Imo2006P5.imo2006_p5' (Compfiles/Imo2006P5.lean)

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
State after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree

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
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

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
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

State before:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ (P - X).natDegree = P.natDegree
Tactic:
rw [natDegree_sub_eq_left_of_natDegree_lt]
State after:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ X.natDegree < P.natDegree

State before:
P : ℤ[X]
hP : 1 < P.natDegree
⊢ X.natDegree < P.natDegree
Tactic:
simpa using hP
State after:
no goals

State before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
⊢ P - X ≠ 0
Tactic:
intro h
State after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
h : P - X = 0
⊢ False

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
State after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False

State before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False
Tactic:
rw [← hPX] at hP
State after:
P : ℤ[X]
hP : 1 < 0
hPX : 0 = P.natDegree
h : P - X = 0
⊢ False

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
State after:
no goals

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))
State after:
no goals

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⟩
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

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)
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

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
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

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
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

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
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

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
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

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
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

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)
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

State before:
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 + X - ↑a - ↑b).natDegree = P.natDegree
Tactic:
rw [sub_sub, ← Int.cast_add]
State after:
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 + X - ↑(a + b)).natDegree = P.natDegree

State before:
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 + X - ↑(a + b)).natDegree = P.natDegree
Tactic:
have h₁ : (P + X).natDegree = P.natDegree := by
  rw [natDegree_add_eq_left_of_natDegree_lt]
  simpa using hP
State after:
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
h₁ : (P + X).natDegree = P.natDegree
⊢ (P + X - ↑(a + b)).natDegree = P.natDegree

State before:
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
h₁ : (P + X).natDegree = P.natDegree
⊢ (P + X - ↑(a + b)).natDegree = P.natDegree
Tactic:
rwa [natDegree_sub_eq_left_of_natDegree_lt]
State after:
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
h₁ : (P + X).natDegree = P.natDegree
⊢ (↑(a + b)).natDegree < (P + X).natDegree

State before:
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
h₁ : (P + X).natDegree = P.natDegree
⊢ (↑(a + b)).natDegree < (P + X).natDegree
Tactic:
rw [h₁, natDegree_intCast]
State after:
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
h₁ : (P + X).natDegree = P.natDegree
⊢ 0 < P.natDegree

State before:
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
h₁ : (P + X).natDegree = P.natDegree
⊢ 0 < P.natDegree
Tactic:
exact zero_lt_one.trans hP
State after:
no goals

State before:
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 + X).natDegree = P.natDegree
Tactic:
rw [natDegree_add_eq_left_of_natDegree_lt]
State after:
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
⊢ X.natDegree < P.natDegree

State before:
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
⊢ X.natDegree < P.natDegree
Tactic:
simpa using hP
State after:
no goals

State before:
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 + X - ↑a - ↑b ≠ 0
Tactic:
intro h
State after:
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
h : P + X - ↑a - ↑b = 0
⊢ False

State before:
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
h : P + X - ↑a - ↑b = 0
⊢ False
Tactic:
rw [h, natDegree_zero] at hPab
State after:
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 : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False

State before:
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 : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Tactic:
rw [← hPab] at hP
State after:
P : ℤ[X]
hP : 1 < 0
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 : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False

State before:
P : ℤ[X]
hP : 1 < 0
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 : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Tactic:
exact (zero_le_one.not_lt hP).elim
State after:
no goals

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 ⊆ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
intro t ht
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
t : ℤ
ht : t ∈ (P.comp P - X).roots.toFinset
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset

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
t : ℤ
ht : t ∈ (P.comp P - X).roots.toFinset
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
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
t : ℤ
ht : (P.comp P - X).IsRoot t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset

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
t : ℤ
ht : (P.comp P - X).IsRoot t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
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
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset

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
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def, eval_sub,
  eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
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
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ Polynomial.eval t P + t = b + a

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
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ Polynomial.eval t P + t = b + a
Tactic:
apply (Int.add_eq_add_of_natAbs_eq_of_natAbs_eq hab _ _).symm <;>
    apply Int.natAbs_eq_of_dvd_dvd <;> set u := P.eval t
State after:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ t - a

case hnm
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - a ∣ u - b

case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ t - b

case hnm
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - a

State before:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ t - a
Tactic:
rw [← ha, ← ht]
State after:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ Polynomial.eval u P - Polynomial.eval b P

State before:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ Polynomial.eval u P - Polynomial.eval b P
Tactic:
apply sub_dvd_eval_sub
State after:
no goals

State before:
case hnm
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - a ∣ u - b
Tactic:
apply sub_dvd_eval_sub
State after:
no goals

State before:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ t - b
Tactic:
rw [← ht]
State after:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ Polynomial.eval u P - b

State before:
case hmn
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ Polynomial.eval u P - b
Tactic:
apply sub_dvd_eval_sub
State after:
no goals

State before:
case hnm
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - a
Tactic:
rw [← ha]
State after:
case hnm
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - Polynomial.eval b P

State before:
case hnm
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
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - Polynomial.eval b P
Tactic:
apply sub_dvd_eval_sub
State after:
no goals