rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
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
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