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

State before:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ P.comp^[k] X - X ≠ 0
Tactic:
rw [sub_ne_zero]
State after:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ P.comp^[k] X ≠ X

State before:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ P.comp^[k] X ≠ X
Tactic:
apply_fun natDegree
State after:
P : ℤ[X]
hP : 1 < P.natDegree
k : ℕ
hk : 0 < k
⊢ (P.comp^[k] X).natDegree ≠ X.natDegree

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