A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x) (minpoly A x) = 0
delta minpoly
case inl
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (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) =
    0

case inr
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
split_ifs with hx
case inl
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
case inl
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
rw [dif_pos hx]
no goals
case inl
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
exact (degree_lt_wf.min_mem _ hx).2
case inr
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x) 0 = 0
case inr
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (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) =
    0
rw [dif_neg hx]
no goals
case inr
A : Type u_2
B : Type u_1
B' : Type ?u.17400
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x) 0 = 0
exact aeval_zero _