-- Mathlib/RingTheory/Polynomial/RationalRoot.lean
theorem den_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) :
    (den A r : A) ∣ p.leadingCoeff

Proof state:
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) ∣ (p.scaleRoots ?s).coeff p.natDegree * num A r ^ p.natDegree

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

Tactic:
apply dvd_term_of_isRoot_of_dvd_terms _ (num_isRoot_scaleRoots_of_aeval_eq_zero hr)

Result:
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 ≠ p.natDegree → ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Proof state:
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) ∣ p.leadingCoeff * num A r ^ p.natDegree
⊢ ∀ ⦃d : A⦄, d ∣ ↑(den A r) → d ∣ num A r ^ p.natDegree → ¬Prime d

Tactic:
intro q dvd_den dvd_num_pow hq

Result:
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) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ p.natDegree
hq : Prime q
⊢ False

Proof state:
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 ≠ (p.scaleRoots ↑(den A r)).natDegree
h : ¬j < (p.scaleRoots ↑(den A r)).natDegree
⊢ ↑(den A r) ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
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 ≠ p.natDegree
h : j < p.natDegree
⊢ j + 0 < p.natDegree

Tactic:
simpa using h

Result:
no goals

Proof state:
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) ∣ p.leadingCoeff * num A r ^ p.natDegree

Tactic:
rw [← coeff_scaleRoots_natDegree]

Result:
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) ∣ (p.scaleRoots ?s).coeff p.natDegree * num A r ^ p.natDegree

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

Proof state:
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 ≠ p.natDegree
h : j < p.natDegree
⊢ ↑(den A r) = ↑(den A r) ^ Nat.succ ?pos.convert_1✝

Tactic:
exact (pow_one _).symm

Result:
no goals

Proof state:
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) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ p.natDegree
hq : Prime q
⊢ IsUnit q

Tactic:
exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den

Result:
no goals

Proof state:
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 ≠ p.natDegree
h : j < p.natDegree
⊢ ↑(den A r) ∣ p.coeff j * ↑(den A r) ^ (p.natDegree - j) * num A r ^ j

Tactic:
refine (dvd_mul_of_dvd_right ?_ _).mul_right _

Result:
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 ≠ p.natDegree
h : j < p.natDegree
⊢ ↑(den A r) ∣ ↑(den A r) ^ (p.natDegree - j)