[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) (scaleRoots p ↑s) = 0
[PROOFSTEP]
convert scaleRoots_eval₂_eq_zero (algebraMap A S) hr
[GOAL]
case h.e'_2.h.e
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s)
[PROOFSTEP]
funext
[GOAL]
case h.e'_2.h.e.h
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ ↑(aeval (↑(algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s) x✝
[PROOFSTEP]
rw [aeval_def, mk'_spec' _ r s]
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ IsRoot (scaleRoots p ↑(den A x)) (num A x)
[PROOFSTEP]
apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap A K) (↑(algebraMap A K) (num A x)) (scaleRoots p ↑(den A x)) = 0
[PROOFSTEP]
refine' scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero _
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval (mk' K (num A x) (den A x))) p = 0
[PROOFSTEP]
rw [mk'_num_den]
[GOAL]
A : Type u_1
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid A
inst✝⁵ : Algebra A S
inst✝⁴ : IsLocalization M S
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval x) p = 0
[PROOFSTEP]
exact hr
[GOAL]
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 p 0
[PROOFSTEP]
suffices num A r ∣ (scaleRoots p (den A r)).coeff 0
  by
  simp only [coeff_scaleRoots, tsub_zero] at this 
  haveI inst := Classical.propDecidable
  by_cases hr : num A r = 0
  · obtain ⟨u, hu⟩ := (isUnit_den_of_num_eq_zero hr).pow p.natDegree
    rw [← hu] at this 
    exact Units.dvd_mul_right.mp this
  · refine' dvd_of_dvd_mul_left_of_no_prime_factors hr _ this
    intro q dvd_num dvd_denom_pow hq
    apply hq.not_unit
    exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)
[GOAL]
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
[PROOFSTEP]
simp only [coeff_scaleRoots, tsub_zero] at this 
[GOAL]
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
[PROOFSTEP]
haveI inst := Classical.propDecidable
[GOAL]
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
[PROOFSTEP]
by_cases hr : num A r = 0
[GOAL]
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
[PROOFSTEP]
obtain ⟨u, hu⟩ := (isUnit_den_of_num_eq_zero hr).pow p.natDegree
[GOAL]
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
[PROOFSTEP]
rw [← hu] at this 
[GOAL]
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
[PROOFSTEP]
exact Units.dvd_mul_right.mp this
[GOAL]
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
[PROOFSTEP]
refine' dvd_of_dvd_mul_left_of_no_prime_factors hr _ this
[GOAL]
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
[PROOFSTEP]
intro q dvd_num dvd_denom_pow hq
[GOAL]
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
[PROOFSTEP]
apply hq.not_unit
[GOAL]
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
[PROOFSTEP]
exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)
[GOAL]
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
[PROOFSTEP]
convert dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _
[GOAL]
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
[PROOFSTEP]
rw [pow_zero, mul_one]
[GOAL]
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
[PROOFSTEP]
intro j hj
[GOAL]
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
[PROOFSTEP]
apply dvd_mul_of_dvd_right
[GOAL]
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
[PROOFSTEP]
convert pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))
[GOAL]
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 ⊥
[PROOFSTEP]
exact (pow_one _).symm
[GOAL]
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
⊢ ↑(den A r) ∣ leadingCoeff p
[PROOFSTEP]
suffices (den A r : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
  by
  refine' dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) _ this
  intro q dvd_den dvd_num_pow hq
  apply hq.not_unit
  exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
[GOAL]
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 : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ↑(den A r) ∣ leadingCoeff p
[PROOFSTEP]
refine' dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) _ this
[GOAL]
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 : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ∀ {d : A}, d ∣ ↑(den A r) → d ∣ num A r ^ natDegree p → ¬Prime d
[PROOFSTEP]
intro q dvd_den dvd_num_pow hq
[GOAL]
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 : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ False
[PROOFSTEP]
apply hq.not_unit
[GOAL]
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 : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ IsUnit q
[PROOFSTEP]
exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
[GOAL]
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
⊢ ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
[PROOFSTEP]
rw [← coeff_scaleRoots_natDegree]
[GOAL]
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
⊢ ↑(den A r) ∣ coeff (scaleRoots p ?s) (natDegree p) * num A r ^ natDegree p
case s
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
⊢ A
[PROOFSTEP]
apply dvd_term_of_isRoot_of_dvd_terms _ (num_isRoot_scaleRoots_of_aeval_eq_zero hr)
[GOAL]
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 ≠ natDegree p → ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
intro j hj
[GOAL]
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 ≠ natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
by_cases h : j < p.natDegree
[GOAL]
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
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
rw [coeff_scaleRoots]
[GOAL]
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
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff p j * ↑(den A r) ^ (natDegree p - j) * num A r ^ j
[PROOFSTEP]
refine' (dvd_mul_of_dvd_right _ _).mul_right _
[GOAL]
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
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ ↑(den A r) ^ (natDegree p - j)
[PROOFSTEP]
convert pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
[GOAL]
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 ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) = ↑(den A r) ^ Nat.succ ?pos.convert_1✝
[PROOFSTEP]
exact (pow_one _).symm
[GOAL]
case pos.convert_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
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ j + 0 < natDegree p
[PROOFSTEP]
simpa using h
[GOAL]
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
j : ℕ
hj : j ≠ natDegree p
h : ¬j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
rw [← natDegree_scaleRoots p (den A r)] at *
[GOAL]
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
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne (le_of_not_gt h) hj.symm), zero_mul]
[GOAL]
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
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ 0
[PROOFSTEP]
exact dvd_zero _
