-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem aeval_ne_zero_of_dvdNotUnit_minpoly {a : A[X]} (hx : IsIntegral A x) (hamonic : a.Monic)
    (hdvd : DvdNotUnit a (minpoly A x)) : Polynomial.aeval x a ≠ 0

Proof state:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < a.natDegree + c.natDegree

Tactic:
apply lt_add_of_pos_right

Result:
case intro.intro.intro.h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ 0 < c.natDegree

Proof state:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ a.natDegree < (minpoly A x).natDegree

Tactic:
have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)

Result:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < (minpoly A x).natDegree

Proof state:
case intro.intro.intro.h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit c

Tactic:
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
  C_1]

Result:
case intro.intro.intro.h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit 1

Proof state:
case intro.intro.intro.h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ 0 < c.natDegree

Tactic:
refine (lt_of_not_le fun h => hu ?_)

Result:
case intro.intro.intro.h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit c

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
ha : (Polynomial.aeval x) a = 0
⊢ a.natDegree < (minpoly A x).natDegree

Tactic:
obtain ⟨_, c, hu, he⟩ := hdvd

Result:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ a.natDegree < (minpoly A x).natDegree

Proof state:
case intro.intro.intro.h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit 1

Tactic:
exact isUnit_one

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
⊢ (Polynomial.aeval x) a ≠ 0

Tactic:
refine fun ha => (min A x hamonic ha).not_lt (degree_lt_degree ?_)

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
ha : (Polynomial.aeval x) a = 0
⊢ a.natDegree < (minpoly A x).natDegree

Proof state:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < (minpoly A x).natDegree

Tactic:
rw [he, hamonic.natDegree_mul hcm]

Result:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < a.natDegree + c.natDegree