A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
⊢ p = minpoly A x
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
⊢ p = minpoly A x
nontriviality A
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
⊢ p = minpoly A x
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
⊢ p = minpoly A x
have hx : IsIntegral A x := ⟨p, hm, hp⟩
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x

case inr
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
⊢ p = minpoly A x
obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
case inr
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x

case inl
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x

case inr
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
swap
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = minpoly A x
case inl
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
obtain ⟨r, hr⟩ := (dvd_iff_modByMonic_eq_zero hm).1 h
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = p * r
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = minpoly A x
rw [hr]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : leadingCoeff (minpoly A x) = leadingCoeff (p * r)
⊢ p = p * r
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = p * r
have hlead := congr_arg leadingCoeff hr
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ p = p * r
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : leadingCoeff (minpoly A x) = leadingCoeff (p * r)
⊢ p = p * r
rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
this : natDegree r ≤ 0
⊢ p = p * r
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ p = p * r
have : natDegree r ≤ 0 := by
  have hr0 : r ≠ 0 := by
    rintro rfl
    exact ne_zero hx (MulZeroClass.mul_zero p ▸ hr)
  apply_fun natDegree  at hr
  rw [hm.natDegree_mul' hr0] at hr
  apply Nat.le_of_add_le_add_left
  rw [add_zero]
  exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
no goals
case inl.intro
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
this : natDegree r ≤ 0
⊢ p = p * r
rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
  mul_one]
no goals
case inr
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
exact (h <| (aeval_modByMonic_eq_self_of_root hm hp).trans <| aeval A x).elim
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
⊢ natDegree r ≤ 0
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ natDegree r ≤ 0
have hr0 : r ≠ 0 := by
  rintro rfl
  exact ne_zero hx (MulZeroClass.mul_zero p ▸ hr)
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree (p * r)
⊢ natDegree r ≤ 0
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
⊢ natDegree r ≤ 0
apply_fun natDegree  at hr
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ natDegree r ≤ 0
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree (p * r)
⊢ natDegree r ≤ 0
rw [hm.natDegree_mul' hr0] at hr
case h
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?a + natDegree r ≤ ?a + 0

case a
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ natDegree r ≤ 0
apply Nat.le_of_add_le_add_left
case h
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?h + natDegree r ≤ ?h

case h
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
case h
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?a + natDegree r ≤ ?a + 0

case a
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
rw [add_zero]
no goals
case h
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?h + natDegree r ≤ ?h

case h
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
hr : minpoly A x = p * 0
hlead : 1 = leadingCoeff 0
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ r ≠ 0
rintro rfl
no goals
A : Type u_1
B : Type u_2
B' : Type ?u.42573
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
hr : minpoly A x = p * 0
hlead : 1 = leadingCoeff 0
⊢ False
exact ne_zero hx (MulZeroClass.mul_zero p ▸ hr)