case h.e'_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ coeff (scaleRoots p ↑(den A r)) 0 = coeff (scaleRoots p ↑(den A r)) 0 * num A r ^ 0

case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ 0 → num A r ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ num A r ∣ coeff (scaleRoots p ↑(den A r)) 0
convert dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ 0 → num A r ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
intro j hj
case convert_2.h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ num A r ^ j
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
apply dvd_mul_of_dvd_right
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r = num A r ^ Nat.succ ⊥
case convert_2.h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ num A r ^ j
convert pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))
no goals
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r = num A r ^ Nat.succ ⊥
exact (pow_one _).symm
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff (scaleRoots p ↑(den A r)) 0
⊢ num A r ∣ coeff p 0
simp only [coeff_scaleRoots, tsub_zero] at this
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
⊢ num A r ∣ coeff p 0
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
haveI inst := Classical.propDecidable
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : num A r = 0
⊢ num A r ∣ coeff p 0

case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ num A r ∣ coeff p 0
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
⊢ num A r ∣ coeff p 0
by_cases hr : num A r = 0
case pos.intro
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : num A r = 0
u : Aˣ
hu : ↑u = ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : num A r = 0
⊢ num A r ∣ coeff p 0
obtain ⟨u, hu⟩ := (isUnit_den_of_num_eq_zero hr).pow p.natDegree
case pos.intro
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
inst : (a : Prop) → Decidable a
hr : num A r = 0
u : Aˣ
this : num A r ∣ coeff p 0 * ↑u
hu : ↑u = ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
case pos.intro
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : num A r = 0
u : Aˣ
hu : ↑u = ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
rw [← hu] at this
no goals
case pos.intro
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
inst : (a : Prop) → Decidable a
hr : num A r = 0
u : Aˣ
this : num A r ∣ coeff p 0 * ↑u
hu : ↑u = ↑(den A r) ^ natDegree p
⊢ num A r ∣ coeff p 0
exact Units.dvd_mul_right.mp this
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ ∀ {d : A}, d ∣ num A r → d ∣ ↑(den A r) ^ natDegree p → ¬Prime d
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ num A r ∣ coeff p 0
refine' dvd_of_dvd_mul_left_of_no_prime_factors hr _ this
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ natDegree p
hq : Prime q
⊢ False
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
⊢ ∀ {d : A}, d ∣ num A r → d ∣ ↑(den A r) ^ natDegree p → ¬Prime d
intro q dvd_num dvd_denom_pow hq
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ natDegree p
hq : Prime q
⊢ IsUnit q
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ natDegree p
hq : Prime q
⊢ False
apply hq.not_unit
no goals
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : ↑(aeval r) p = 0
this : num A r ∣ coeff p 0 * ↑(den A r) ^ natDegree p
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ natDegree p
hq : Prime q
⊢ IsUnit q
exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)
no goals
case h.e'_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ coeff (scaleRoots p ↑(den A r)) 0 = coeff (scaleRoots p ↑(den A r)) 0 * num A r ^ 0
rw [pow_zero, mul_one]