-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem neg {B : Type*} [CommRing B] [Algebra A B] (x : B) :
    minpoly A (- x) = (-1) ^ (natDegree (minpoly A x)) * (minpoly A x).comp (- X)

Proof state:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)

Tactic:
rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]

Result:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ 0 = (-1) ^ natDegree 0 * 0

case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (-x)

Proof state:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
this : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0
H : (minpoly A x).degree ≤ ((-1) ^ q.natDegree * q.comp (-X)).degree
n1 : (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X) ≠ 0
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Tactic:
have n2 := qmo.neg_one_pow_natDegree_mul_comp_neg_X.ne_zero

Result:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
this : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0
H : (minpoly A x).degree ≤ ((-1) ^ q.natDegree * q.comp (-X)).degree
n1 : (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X) ≠ 0
n2 : (-1) ^ q.natDegree * q.comp (-X) ≠ 0
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Proof state:
case pos.refine_1
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval (-x)) ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)) = 0

Tactic:
simp [aeval_comp]

Result:
no goals

Proof state:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
this : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0
H : (minpoly A x).degree ≤ ((-1) ^ q.natDegree * q.comp (-X)).degree
n1 : (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X) ≠ 0
n2 : (-1) ^ q.natDegree * q.comp (-X) ≠ 0
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree qmo.ne_zero,
  degree_eq_natDegree n1, natDegree_mul (by simp) (right_ne_zero_of_mul n1), natDegree_comp]

Result:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
this : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0
H : (minpoly A x).degree ≤ ((-1) ^ q.natDegree * q.comp (-X)).degree
n1 : (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X) ≠ 0
n2 : (-1) ^ q.natDegree * q.comp (-X) ≠ 0
⊢ ↑(((-1) ^ (minpoly A x).natDegree).natDegree + (minpoly A x).natDegree * (-X).natDegree) ≤ ↑q.natDegree