rcases Finset.not_subset.1 H with ⟨a, ha, hab⟩
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
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