A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) ≤
    degree p
A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree (minpoly A x) ≤ degree p
delta minpoly
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ degree
      (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) ≤
    degree p

case inr
A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ degree p
A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) ≤
    degree p
split_ifs with hx
no goals
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ degree
      (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) ≤
    degree p
exact le_of_not_lt (degree_lt_wf.not_lt_min _ hx ⟨pmonic, hp⟩)
no goals
case inr
A : Type u_1
B : Type u_2
B' : Type ?u.37651
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ degree p
simp only [degree_zero, bot_le]