-- 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 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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Tactic:
have n1 := ((minpoly.monic hx).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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Proof state:
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 ≠ 0

Tactic:
simp

Result:
no goals

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
⊢ ¬IsIntegral A (-x)

Tactic:
exact IsIntegral.neg_iff.not.mpr hx

Result:
no goals

Proof state:
case pos
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:
refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
    ?_ fun q qmo hq => ?_).symm

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

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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

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).natDegree ≤ ↑(((-1) ^ q.natDegree).natDegree + q.natDegree * (-X).natDegree)
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

Tactic:
simpa using H

Result:
no goals

Proof state:
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).natDegree ≤ ↑((-1) ^ q.natDegree * q.comp (-X)).natDegree
n1 : (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X) ≠ 0
n2 : (-1) ^ q.natDegree * q.comp (-X) ≠ 0
⊢ (-1) ^ q.natDegree ≠ 0

Tactic:
simp

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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Tactic:
have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X this

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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Proof state:
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
⊢ (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0

Tactic:
simpa [aeval_comp] using hq

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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Tactic:
have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (- X)) = 0 := by
  simpa [aeval_comp] using hq

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
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

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).natDegree + (minpoly A x).natDegree * (-X).natDegree) ≤ ↑q.natDegree

Tactic:
rw [degree_eq_natDegree (minpoly.ne_zero hx),
  degree_eq_natDegree qmo.neg_one_pow_natDegree_mul_comp_neg_X.ne_zero,
  natDegree_mul (by simp) (right_ne_zero_of_mul n2), natDegree_comp] at H

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).natDegree ≤ ↑(((-1) ^ q.natDegree).natDegree + q.natDegree * (-X).natDegree)
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

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

Tactic:
by_cases hx : IsIntegral A x

Result:
case pos
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)

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)

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
⊢ 0 = (-1) ^ natDegree 0 * 0

Tactic:
simp only [natDegree_zero, pow_zero, mul_zero]

Result:
no goals