awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : UniqueFactorizationMonoid A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
p : A[X]
r : K
hr_1 : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : num A r ∣ p.coeff 0 * (↑(den A r) : A) ^ (p.natDegree - 0)
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) : A) ^ (p.natDegree - 0)
hq : Prime q
neg : IsUnit q
⊢ False

Tactic:
apply hq.not_unit

Premises used: Prime.not_unit
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : UniqueFactorizationMonoid A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
p : A[X]
r : K
hr_1 : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : num A r ∣ p.coeff 0 * (↑(den A r) : A) ^ (p.natDegree - 0)
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) : A) ^ (p.natDegree - 0)
hq : Prime q
⊢ IsUnit q

Tactic:
num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)

Premises used: Prime.dvd_of_dvd_pow, IsFractionRing.num_den_reduced
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : UniqueFactorizationMonoid A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
p : A[X]
r : K
hr_1 : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : num A r ∣ p.coeff 0 * (↑(den A r) : A) ^ (p.natDegree - 0)
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) : A) ^ (p.natDegree - 0)
hq : Prime q
⊢ IsUnit q

Tactic:
exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)

Premises used: Prime.dvd_of_dvd_pow, IsFractionRing.num_den_reduced
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
suffices : num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff 0
⊢ num A r ∣ p.coeff 0

Tactic:
suffices num A r ∣ (scaleRoots p (den A r)).coeff 0 by
    simp only [coeff_scaleRoots] at this
    haveI inst := Classical.propDecidable
    by_cases hr : num A r = 0
    · simp_all [nonZeroDivisors.coe_ne_zero]
    · 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)
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
⊢ num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff 0 * HPow.hPow (β := ℕ) (num A r) 0

Tactic:
dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _

Premises used: num_isRoot_scaleRoots_of_aeval_eq_zero, Polynomial.dvd_term_of_isRoot_of_dvd_terms, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
h : (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * HPow.hPow (β := ℕ) (num A r) 0
convert_2 : ∀ (j : ℕ), j ≠ 0 → num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
⊢ num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff 0

Tactic:
convert! dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _

Premises used: num_isRoot_scaleRoots_of_aeval_eq_zero, Polynomial.dvd_term_of_isRoot_of_dvd_terms, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
h : (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * 1
h₁ h₂ : (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0
⊢ (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * HPow.hPow (β := ℕ) (num A r) 0

Tactic:
rw [pow_zero, mul_one]

Premises used: pow_zero, mul_one
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ 0
convert_2 : num A r ∣ num A r ^ j
⊢ num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ 0
⊢ num A r ^ Nat.succ ⊥ ∣ num A r ^ j

Tactic:
pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))

Premises used: Iff.mpr, Nat.succ_le_of_lt, pow_dvd_pow, bot_lt_iff_ne_bot, IsFractionRing.num
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ 0
h : num A r = num A r ^ Nat.succ ⊥
⊢ num A r ∣ num A r ^ j

Tactic:
convert! pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))

Premises used: Iff.mpr, Nat.succ_le_of_lt, pow_dvd_pow, bot_lt_iff_ne_bot, IsFractionRing.num
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ 0
⊢ num A r = num A r ^ Nat.succ ⊥

Tactic:
(pow_one _).symm

Premises used: pow_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ 0
⊢ num A r = num A r ^ Nat.succ ⊥

Tactic:
exact (pow_one _).symm

Premises used: pow_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
⊢ (↑(den A r) : A) ∣ p.leadingCoeff

Tactic:
dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) ?_
        this

Premises used: IsFractionRing.den, UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors, Iff.mp, mem_nonZeroDivisors_iff_ne_zero, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
dvd_of_dvd_mul_left_of_no_prime_factors : ∀ ⦃d : A⦄, d ∣ (↑(den A r) : A) → d ∣ num A r ^ p.natDegree → ¬Prime d
⊢ (↑(den A r) : A) ∣ p.leadingCoeff

Tactic:
refine
      dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) ?_
        this

Premises used: IsFractionRing.den, UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors, Iff.mp, mem_nonZeroDivisors_iff_ne_zero, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ (↑(den A r) : A)
dvd_num_pow : q ∣ num A r ^ p.natDegree
hq : Prime q
apply : IsUnit q
⊢ False

Tactic:
apply hq.not_unit

Premises used: Prime.not_unit
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ (↑(den A r) : A)
dvd_num_pow : q ∣ num A r ^ p.natDegree
hq : Prime q
⊢ IsUnit q

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

Premises used: Prime.dvd_of_dvd_pow, IsFractionRing.num_den_reduced
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
this : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ (↑(den A r) : A)
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

Premises used: Prime.dvd_of_dvd_pow, IsFractionRing.num_den_reduced
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
suffices : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
⊢ (↑(den A r) : A) ∣ p.leadingCoeff

Tactic:
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
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
rw : (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff p.natDegree * num A r ^ p.natDegree
s : A
⊢ (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree

Tactic:
rw [← coeff_scaleRoots_natDegree]

Premises used: Polynomial.coeff_scaleRoots_natDegree
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
pos : ∀ (h : j < p.natDegree), (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
neg : ∀ (h : p.natDegree ≤ j), (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j

Tactic:
by_cases! h : j < p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
pos : (↑(den A r) : A) ∣ p.coeff j * (↑(den A r) : A) ^ (p.natDegree - j) * num A r ^ j
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j

Tactic:
rw [coeff_scaleRoots]

Premises used: Polynomial.coeff_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) ∣ p.coeff j * (↑(den A r) : A) ^ (p.natDegree - j) * num A r ^ j

Tactic:
(dvd_mul_of_dvd_right ?_ _).mul_right _

Premises used: dvd_mul_of_dvd_right, Dvd.dvd.mul_right
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
pos : (↑(den A r) : A) ∣ (↑(den A r) : A) ^ (p.natDegree - j)
⊢ (↑(den A r) : A) ∣ p.coeff j * (↑(den A r) : A) ^ (p.natDegree - j) * num A r ^ j

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

Premises used: dvd_mul_of_dvd_right, Dvd.dvd.mul_right
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) ^ Nat.succ 0 ∣ (↑(den A r) : A) ^ (p.natDegree - j)

Tactic:
pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))

Premises used: Iff.mpr, pow_dvd_pow, IsFractionRing.den, Nat.succ_le_iff, Subtype.val, lt_tsub_iff_left
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
h₁ : (↑(den A r) : A) = (↑(den A r) : A) ^ Nat.succ 0
pos : ℕ
pos₁ : j + 0 < p.natDegree
⊢ (↑(den A r) : A) ∣ (↑(den A r) : A) ^ (p.natDegree - j)

Tactic:
convert! pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))

Premises used: Iff.mpr, pow_dvd_pow, IsFractionRing.den, Nat.succ_le_iff, Subtype.val, lt_tsub_iff_left
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) = (↑(den A r) : A) ^ Nat.succ 0

Tactic:
(pow_one _).symm

Premises used: pow_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) = (↑(den A r) : A) ^ Nat.succ 0

Tactic:
exact (pow_one _).symm

Premises used: pow_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ j + 0 < p.natDegree

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : p.natDegree ≤ j
⊢ j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree

Tactic:
rw [← natDegree_scaleRoots p (den A r)] at *

Premises used: IsFractionRing.den, Polynomial.natDegree_scaleRoots, Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : p.natDegree ≤ j
hj₁ : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
⊢ (p.scaleRoots (↑(den A r) : A)).natDegree ≤ j

Tactic:
rw [← natDegree_scaleRoots p (den A r)] at *

Premises used: IsFractionRing.den, Polynomial.natDegree_scaleRoots, Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
h : (p.scaleRoots (↑(den A r) : A)).natDegree ≤ j
neg : (↑(den A r) : A) ∣ 0
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h hj.symm),
    zero_mul]

Premises used: MulZeroClass.zero_mul, Ne.symm, Polynomial.coeff_eq_zero_of_natDegree_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
h : (p.scaleRoots (↑(den A r) : A)).natDegree ≤ j
⊢ (↑(den A r) : A) ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
h : (p.scaleRoots (↑(den A r) : A)).natDegree ≤ j
⊢ (↑(den A r) : A) ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
⊢ IsInteger A r

Tactic:
isInteger_of_isUnit_den (isUnit_of_dvd_one (hp ▸ den_dvd_of_is_root hr))

Premises used: isUnit_of_dvd_one, IsFractionRing.isInteger_of_isUnit_den
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
obtain :
  ∀ (inv : A) (h_inv : 1 = (↑(den A r) : A) * inv), ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0
⊢ ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0

Tactic:
obtain ⟨inv, h_inv⟩ := hp ▸ den_dvd_of_is_root hr
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
right : num A r * inv ∣ p.coeff 0
left : r = (algebraMap A K : (a : A) → K) (num A r * inv)
⊢ ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0

Tactic:
use num A r * inv, ?_

Premises used: IsFractionRing.num
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
⊢ 1 = inv * (↑(den A r) : A)

Tactic:
simpa [mul_comm] using h_inv

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
⊢ inv ∣ 1

Tactic:
have h : inv ∣ 1 := ⟨den A r, by simpa [mul_comm] using h_inv⟩
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
h : inv ∣ 1
⊢ num A r * inv ∣ p.coeff 0

Tactic:
simpa using mul_dvd_mul (num_dvd_of_is_root hr) h

Premises used: mul_dvd_mul, num_dvd_of_is_root
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)

Tactic:
have d_ne_zero : algebraMap A K (den A r) ≠ 0 :=
      IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (den A r).prop
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
⊢ r = (algebraMap A K : (a : A) → K) (num A r * inv)

Tactic:
nth_rw 1 [← mk'_num_den' A r]

Premises used: IsFractionRing.mk'_num_den'