awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
i : ℕ
hp : Prime p
zero : divRadical (HPow.hPow (β := ℕ) p 0) ∣ (derivative : (a : k[X]) → k[X]) (HPow.hPow (β := ℕ) p 0)
⊢ divRadical (p ^ i) ∣ (derivative : (a : k[X]) → k[X]) (p ^ i)
have succ : ∀ (n : ℕ), divRadical (p ^ (n + 1)) ∣ (derivative : (a : k[X]) → k[X]) (p ^ (n + 1))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical (HPow.hPow (β := ℕ) p 0) ∣ (derivative : (a : k[X]) → k[X]) (HPow.hPow (β := ℕ) p 0)
have zero : Dvd.dvd.{u_1} (α := k[X]) (divRadical 1) 0
Tactic: rw [pow_zero, derivative_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ divRadical (p ^ (i + 1)) ∣ (derivative : (a : k[X]) → k[X]) (p ^ (i + 1))
have rw : p ^ (i + 1) ∣
  HMul.hMul (β := k[X])
    (HMul.hMul (α := k[X]) ((normalize : (a : k[X]) → k[X]) p : k[X])
      (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (HAdd.hAdd (α := k) (↑i : k) 1) : k[X]) (p ^ i)))
    ((derivative : (a : k[X]) → k[X]) p : k[X])
Tactic: rw [← mul_dvd_mul_iff_left radical_ne_zero, radical_mul_divRadical,
        radical_pow_of_prime hp i.succ_ne_zero, derivative_pow_succ, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣
    HMul.hMul (β := k[X])
      (HMul.hMul (α := k[X]) ((normalize : (a : k[X]) → k[X]) p : k[X])
        (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (HAdd.hAdd (α := k) (↑i : k) 1) : k[X]) (p ^ i)))
      ((derivative : (a : k[X]) → k[X]) p : k[X])
have h : p ^ (i + 1) ∣
  HMul.hMul (α := k[X]) ((normalize : (a : k[X]) → k[X]) p : k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (HAdd.hAdd (α := k) (↑i : k) 1) : k[X]) (p ^ i))
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣
    HMul.hMul (α := k[X]) ((normalize : (a : k[X]) → k[X]) p : k[X])
      (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (HAdd.hAdd (α := k) (↑i : k) 1) : k[X]) (p ^ i))
have h : p ^ (i + 1) ∣
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (HAdd.hAdd (α := k) (↑i : k) 1) : k[X])
    (HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X]))
Tactic: rw [mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (HAdd.hAdd (α := k) (↑i : k) 1) : k[X])
      (HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X]))
have h : p ^ (i + 1) ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
have h : p ^ i * p ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
Tactic: rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
h : p ^ i * p ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
⊢ p ^ (i + 1) ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
have h₁ : p ∣ (normalize : (a : k[X]) → k[X]) p
Tactic: rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
h : p ^ i * p ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
h₁ : p ∣ (normalize : (a : k[X]) → k[X]) p
⊢ p ^ (i + 1) ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
have h₂ : p ∣ p
Tactic: rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ (derivative : (a : k[X]) → k[X]) x
hy : divRadical y ∣ (derivative : (a : k[X]) → k[X]) y
⊢ divRadical (x * y) ∣ (derivative : (a : k[X]) → k[X]) (x * y)
have hc : IsCoprime x y
Tactic: have hc : IsCoprime x y :=
      EuclideanDomain.isCoprime_of_dvd
        (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
        fun p hp _ hpx hpy => hp (hpxy hpx hpy)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ (derivative : (a : k[X]) → k[X]) x
hy : divRadical y ∣ (derivative : (a : k[X]) → k[X]) y
hc : IsCoprime x y
⊢ divRadical (x * y) ∣ (derivative : (a : k[X]) → k[X]) (x * y)
have rw : divRadical x * divRadical y ∣
  HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) x : k[X]) y +
    HMul.hMul (β := k[X]) x ((derivative : (a : k[X]) → k[X]) y : k[X])
Tactic: rw [divRadical_mul hc, derivative_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣
    HMul.hMul (β := k[X]) a ((derivative : (a : k[X]) → k[X]) b : k[X]) -
      HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) b
have h₁ : divRadical a ∣ HMul.hMul (β := k[X]) a ((derivative : (a : k[X]) → k[X]) b : k[X])
Tactic: apply dvd_sub
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
h₁ : divRadical a ∣ HMul.hMul (β := k[X]) a ((derivative : (a : k[X]) → k[X]) b : k[X])
⊢ divRadical a ∣
    HMul.hMul (β := k[X]) a ((derivative : (a : k[X]) → k[X]) b : k[X]) -
      HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) b
have h₂ : divRadical a ∣ HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) b
Tactic: apply dvd_sub
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ HMul.hMul (β := k[X]) a ((derivative : (a : k[X]) → k[X]) b : k[X])
have h₁ : divRadical a ∣ a
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) b
have h₂ : divRadical a ∣ (derivative : (a : k[X]) → k[X]) a
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ a.wronskian b
have rw : divRadical b ∣ b.wronskian a
Tactic: rw [← wronskian_neg_eq, dvd_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
S : Type u_4
inst : CommRing A
inst_1 : CommRing S
M : Submonoid A
inst_2 : Algebra A S
inst_3 : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : Eq.{u_4 + 1} (α := S) ((aeval (mk' S r s) : (a : A[X]) → S) p : S) (0 : S)
⊢ Eq.{u_4 + 1} (α := S)
    (((aeval ((algebraMap A S : (a : A) → S) r) : A[X] →ₐ[A] S) : (a : A[X]) → S) (p.scaleRoots (↑s : A)) : S) (0 : S)
have h : Eq (α := (a : A[X]) → S) (⇑(aeval ((algebraMap A S : (a : A) → S) r) : A[X] →ₐ[A] S) : (a : A[X]) → S)
  (eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)))
Tactic: convert! scaleRoots_eval₂_eq_zero (algebraMap A S) hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
S : Type u_4
inst : CommRing A
inst_1 : CommRing S
M : Submonoid A
inst_2 : Algebra A S
inst_3 : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : Eq.{u_4 + 1} (α := S) ((aeval (mk' S r s) : (a : A[X]) → S) p : S) (0 : S)
⊢ Eq (α := (a : A[X]) → S) (⇑(aeval ((algebraMap A S : (a : A) → S) r) : A[X] →ₐ[A] S) : (a : A[X]) → S)
    (eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)))
have h : ∀ (x : A[X]),
  ((aeval ((algebraMap A S : (a : A) → S) r) : A[X] →ₐ[A] S) : (a : A[X]) → S) x =
    eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)) x
Tactic: funext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
S : Type u_4
inst : CommRing A
inst_1 : CommRing S
M : Submonoid A
inst_2 : Algebra A S
inst_3 : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : Eq.{u_4 + 1} (α := S) ((aeval (mk' S r s) : (a : A[X]) → S) p : S) (0 : S)
x : A[X]
⊢ ((aeval ((algebraMap A S : (a : A) → S) r) : A[X] →ₐ[A] S) : (a : A[X]) → S) x =
    eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)) x
have h : eval₂ (algebraMap A S) ((algebraMap A S : (a : A) → S) r) x =
  eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)) x
Tactic: rw [aeval_def, mk'_spec' _ r s]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
S : Type u_4
inst : CommRing A
inst_1 : CommRing S
M : Submonoid A
inst_2 : Algebra A S
inst_3 : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : Eq.{u_4 + 1} (α := S) ((aeval (mk' S r s) : (a : A[X]) → S) p : S) (0 : S)
x : A[X]
h :
  eval₂ (algebraMap A S) ((algebraMap A S : (a : A) → S) r) x =
    eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)) x
⊢ ((aeval ((algebraMap A S : (a : A) → S) r) : A[X] →ₐ[A] S) : (a : A[X]) → S) x =
    eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s)) x
have h₁ : eval₂ (algebraMap A S) ((algebraMap A S : (a : A) → S) r) x =
  eval₂ (algebraMap A S) ((algebraMap A S : (a : A) → S) r) x
Tactic: rw [aeval_def, mk'_spec' _ r s]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
inst_5 : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : Eq.{u_2 + 1} (α := K) ((aeval x : (a : A[X]) → K) p : K) (0 : K)
⊢ (p.scaleRoots (↑(den A x) : A)).IsRoot (num A x)
have apply : eval₂ (algebraMap A K) ((algebraMap A K : (a : A) → K) (num A x)) (p.scaleRoots (↑(den A x) : A)) = 0
Tactic: apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
inst_5 : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : Eq.{u_2 + 1} (α := K) ((aeval x : (a : A[X]) → K) p : K) (0 : K)
⊢ eval₂ (algebraMap A K) ((algebraMap A K : (a : A) → K) (num A x)) (p.scaleRoots (↑(den A x) : A)) = 0
have refine : Eq.{u_2 + 1} (α := K) ((aeval (mk' K (num A x) (den A x)) : (a : A[X]) → K) p : K) (0 : K)
Tactic: refine scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (hypothesis)
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 : num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff 0
⊢ num A r ∣ p.coeff 0
have this₁ : num A r ∣ p.coeff 0 * (↑(den A r) : A) ^ (p.natDegree - 0)
Tactic: simp only [coeff_scaleRoots] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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 : num A r ∣ p.coeff 0 * (↑(den A r) : A) ^ (p.natDegree - 0)
⊢ num A r ∣ p.coeff 0
have haveI : ∀ (inst_6 : (a : Prop) → Decidable a), num A r ∣ p.coeff 0
Tactic: haveI inst := Classical.propDecidable
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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 : 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
⊢ num A r ∣ p.coeff 0
have pos : ∀ (hr : num A r = 0), num A r ∣ p.coeff 0
Tactic: by_cases hr : num A r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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 : 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
pos : ∀ (hr : num A r = 0), num A r ∣ p.coeff 0
⊢ num A r ∣ p.coeff 0
have neg : ∀ (hr : ¬num A r = 0), num A r ∣ p.coeff 0
Tactic: by_cases hr : num A r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ num A r ∣ p.coeff 0
have neg : ∀ ⦃d : A⦄, d ∣ num A r → d ∣ (↑(den A r) : A) ^ (p.natDegree - 0) → ¬Prime d
Tactic: refine dvd_of_dvd_mul_left_of_no_prime_factors hr ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ False
have neg : IsUnit q
Tactic: apply hq.not_unit
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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.coeff 0
have suffices : num A r ∣ (p.scaleRoots (↑(den A r) : A)).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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
have h : (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * HPow.hPow (β := ℕ) (num A r) 0
Tactic: convert! dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff 0
have convert_2 : ∀ (j : ℕ), j ≠ 0 → num A r ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
Tactic: convert! dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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)
⊢ (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * HPow.hPow (β := ℕ) (num A r) 0
have h : (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * 1
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0 * HPow.hPow (β := ℕ) (num A r) 0
have h₁ : (p.scaleRoots (↑(den A r) : A)).coeff 0 = (p.scaleRoots (↑(den A r) : A)).coeff 0
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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 ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have convert_2 : num A r ∣ num A r ^ j
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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 ^ j
have h : num A r = num A r ^ Nat.succ ⊥
Tactic: convert! pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
have dvd_of_dvd_mul_left_of_no_prime_factors : ∀ ⦃d : A⦄, d ∣ (↑(den A r) : A) → d ∣ num A r ^ p.natDegree → ¬Prime d
Tactic: refine
      dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) ?_
        this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ False
have apply : IsUnit q
Tactic: apply hq.not_unit
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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)
⊢ (↑(den A r) : A) ∣ p.leadingCoeff
have suffices : (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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)
⊢ (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
have rw : (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff p.natDegree * num A r ^ p.natDegree
Tactic: rw [← coeff_scaleRoots_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ (↑(den A r) : A) ∣ p.leadingCoeff * num A r ^ p.natDegree
have s : A
Tactic: rw [← coeff_scaleRoots_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have pos : ∀ (h : j < p.natDegree), (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
Tactic: by_cases! h : j < p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
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
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have neg : ∀ (h : p.natDegree ≤ j), (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
Tactic: by_cases! h : j < p.natDegree