awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
this : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a) : R ⧸ I) (0 : R ⧸ I)
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (0 : MvPolynomial.{u_2, u_1} σ (R ⧸ I))

Tactic:
simp only [this, C_0]

Premises used: MvPolynomial.C_0
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
suffices : coeff n a ∈ I
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (0 : MvPolynomial.{u_2, u_1} σ (R ⧸ I))

Tactic:
suffices coeff n a ∈ I by
    rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
    simp only [this, C_0]
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
⊢ coeff n a ∈ I

Tactic:
mem_map_C_iff.1 ha n

Premises used: MvPolynomial.mem_map_C_iff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
⊢ coeff n a ∈ I

Tactic:
exact mem_map_C_iff.1 ha n

Premises used: MvPolynomial.mem_map_C_iff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
h : a ≠ 0
⊢ (radical a).degree ≤ a.degree

Tactic:
degree_le_of_dvd radical_dvd_self h

Premises used: Polynomial.degree_le_of_dvd, UniqueFactorizationMonoid.radical_dvd_self
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
pos : ∀ (ha : a = 0), (radical a).natDegree ≤ a.natDegree
neg : ∀ (ha : ¬a = 0), (radical a).natDegree ≤ a.natDegree
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
ha : a = 0
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
ha : ¬a = 0
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
natDegree_le_of_dvd radical_dvd_self ha

Premises used: Polynomial.natDegree_le_of_dvd, UniqueFactorizationMonoid.radical_dvd_self
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
ha : ¬a = 0
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
exact natDegree_le_of_dvd radical_dvd_self ha

Premises used: Polynomial.natDegree_le_of_dvd
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
induction : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)
h1 : ∀ {x : k[X]}, IsUnit x → divRadical x ∣ (derivative : (a : k[X]) → k[X]) x
hpr : ∀ {p : k[X]} (i : ℕ), Prime p → divRadical (p ^ i) ∣ (derivative : (a : k[X]) → k[X]) (p ^ i)
hcp :
  ∀ {x y : k[X]},
    IsRelPrime x y →
      divRadical x ∣ (derivative : (a : k[X]) → k[X]) x →
        divRadical y ∣ (derivative : (a : k[X]) → k[X]) y →
          divRadical (x * y) ∣ (derivative : (a : k[X]) → k[X]) (x * y)
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a

Tactic:
induction a using induction_on_coprime
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
⊢ Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
case case₁ case₂ : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) 0
⊢ Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)

Tactic:
case h0 =>
    rw [derivative_zero]
    apply dvd_zero

Premises used: dvd_zero, Polynomial.derivative_zero
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
ha : IsUnit a
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a

Tactic:
(divRadical_isUnit ha).dvd

Premises used: IsUnit.dvd, EuclideanDomain.divRadical_isUnit
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
ha : IsUnit a
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a

Tactic:
exact (divRadical_isUnit ha).dvd

Premises used: IsUnit.dvd, EuclideanDomain.divRadical_isUnit
-- Module: Mathlib.RingTheory.Polynomial.Radical
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)
succ : ∀ (n : ℕ), divRadical (p ^ (n + 1)) ∣ (derivative : (a : k[X]) → k[X]) (p ^ (n + 1))
⊢ divRadical (p ^ i) ∣ (derivative : (a : k[X]) → k[X]) (p ^ i)

Tactic:
cases i
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
zero : Dvd.dvd.{u_1} (α := k[X]) (divRadical 1) 0
⊢ divRadical (HPow.hPow (β := ℕ) p 0) ∣ (derivative : (a : k[X]) → k[X]) (HPow.hPow (β := ℕ) p 0)

Tactic:
rw [pow_zero, derivative_one]

Premises used: pow_zero, Polynomial.derivative_one
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
⊢ Dvd.dvd.{u_1} (α := k[X]) (divRadical 1) 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
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])
⊢ divRadical (p ^ (i + 1)) ∣ (derivative : (a : k[X]) → k[X]) (p ^ (i + 1))

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]

Premises used: Polynomial.derivative_pow_succ, UniqueFactorizationMonoid.radical_ne_zero, EuclideanDomain.radical_mul_divRadical, mul_assoc, mul_dvd_mul_iff_left, Nat.succ_ne_zero, UniqueFactorizationMonoid.radical_pow_of_prime
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
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))
⊢ 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:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
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]))
⊢ 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:
rw [mul_comm, mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
h : p ^ (i + 1) ∣ HMul.hMul (β := k[X]) (p ^ i) ((normalize : (a : k[X]) → k[X]) p : k[X])
⊢ 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:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.RingTheory.Polynomial.Radical
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
h₂ h₃ : p ∣ p
⊢ p ^ (i + 1) ∣ 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]

Premises used: pow_succ, pow_ne_zero, mul_dvd_mul_iff_left, Prime.ne_zero, dvd_normalize_iff
-- Module: Mathlib.RingTheory.Polynomial.Radical
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
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Radical
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
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])
⊢ divRadical (x * y) ∣ (derivative : (a : k[X]) → k[X]) (x * y)

Tactic:
rw [divRadical_mul hc, derivative_mul]

Premises used: Polynomial.derivative_mul, EuclideanDomain.divRadical_mul
-- Module: Mathlib.RingTheory.Polynomial.Radical
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 * 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:
dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)

Premises used: EuclideanDomain.divRadical_dvd_self, mul_dvd_mul, dvd_add
-- Module: Mathlib.RingTheory.Polynomial.Radical
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 * 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:
exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)

Premises used: EuclideanDomain.divRadical_dvd_self, mul_dvd_mul, dvd_add
-- Module: Mathlib.RingTheory.Polynomial.Radical
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])
h₂ : divRadical a ∣ HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) b
⊢ 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

Tactic:
apply dvd_sub

Premises used: dvd_sub
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
h₁ : divRadical a ∣ a
⊢ divRadical a ∣ HMul.hMul (β := k[X]) a ((derivative : (a : k[X]) → k[X]) b : k[X])

Tactic:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a

Tactic:
divRadical_dvd_self a

Premises used: EuclideanDomain.divRadical_dvd_self
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a

Tactic:
exact divRadical_dvd_self a

Premises used: EuclideanDomain.divRadical_dvd_self
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
h₂ : divRadical a ∣ (derivative : (a : k[X]) → k[X]) a
⊢ divRadical a ∣ HMul.hMul (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) b

Tactic:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a

Tactic:
divRadical_dvd_derivative a

Premises used: divRadical_dvd_derivative
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a

Tactic:
exact divRadical_dvd_derivative a

Premises used: divRadical_dvd_derivative
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
rw : divRadical b ∣ b.wronskian a
⊢ divRadical b ∣ a.wronskian b

Tactic:
rw [← wronskian_neg_eq, dvd_neg]

Premises used: Polynomial.wronskian_neg_eq, dvd_neg
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ b.wronskian a

Tactic:
divRadical_dvd_wronskian_left _ _

Premises used: divRadical_dvd_wronskian_left
-- Module: Mathlib.RingTheory.Polynomial.Radical
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ b.wronskian a

Tactic:
exact divRadical_dvd_wronskian_left _ _

Premises used: divRadical_dvd_wronskian_left
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
⊢ eval₂ (algebraMap A S) (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) (↑s : A) : S) (mk' S r s))
      (p.scaleRoots (↑s : A)) =
    0

Tactic:
scaleRoots_eval₂_eq_zero (algebraMap A S) hr

Premises used: Algebra.algebraMap, Polynomial.scaleRoots_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
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)))
⊢ 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)

Tactic:
convert! scaleRoots_eval₂_eq_zero (algebraMap A S) hr

Premises used: Algebra.algebraMap, Polynomial.scaleRoots_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
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
⊢ 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:
funext
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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
h₁ 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
⊢ ((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:
rw [aeval_def, mk'_spec' _ r s]

Premises used: IsLocalization.mk'_spec', Polynomial.aeval_def
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
apply : eval₂ (algebraMap A K) ((algebraMap A K : (a : A) → K) (num A x)) (p.scaleRoots (↑(den A x) : A)) = 0
⊢ (p.scaleRoots (↑(den A x) : A)).IsRoot (num A x)

Tactic:
apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)

Premises used: IsFractionRing.injective, Polynomial.isRoot_of_eval₂_map_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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

Tactic:
scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero ?_

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
refine : Eq.{u_2 + 1} (α := K) ((aeval (mk' K (num A x) (den A 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

Tactic:
refine scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero ?_

Premises used: scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
rw : Eq.{u_2 + 1} (α := K) ((aeval x : (a : A[X]) → K) p : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((aeval (mk' K (num A x) (den A x)) : (a : A[X]) → K) p : K) (0 : K)

Tactic:
rw [mk'_num_den]

Premises used: IsFractionRing.mk'_num_den
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : A[X]) → K) p : K) (0 : K)

Tactic:
hr
-- Module: Mathlib.RingTheory.Polynomial.RationalRoot
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)
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : A[X]) → K) p : K) (0 : K)

Tactic:
exact 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]
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 * (↑(den A r) : A) ^ (p.natDegree - 0)

Tactic:
simp only [coeff_scaleRoots] at this

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)
this : num A r ∣ p.coeff 0 * (↑(den A r) : A) ^ (p.natDegree - 0)
haveI : ∀ (inst_6 : (a : Prop) → Decidable a), num A r ∣ p.coeff 0
⊢ num A r ∣ p.coeff 0

Tactic:
haveI inst := Classical.propDecidable
-- 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 : 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
neg : ∀ (hr : ¬num A r = 0), num A r ∣ p.coeff 0
⊢ num A r ∣ p.coeff 0

Tactic:
by_cases hr : num A r = 0

Premises used: IsFractionRing.num
-- 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
⊢ num A r ∣ p.coeff 0

Tactic:
simp_all [nonZeroDivisors.coe_ne_zero]

Premises used: nonZeroDivisors.coe_ne_zero
-- 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
⊢ num A r ∣ p.coeff 0

Tactic:
dvd_of_dvd_mul_left_of_no_prime_factors hr ?_ this

Premises used: UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors
-- 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
neg : ∀ ⦃d : A⦄, d ∣ num A r → d ∣ (↑(den A r) : A) ^ (p.natDegree - 0) → ¬Prime d
⊢ num A r ∣ p.coeff 0

Tactic:
refine dvd_of_dvd_mul_left_of_no_prime_factors hr ?_ this

Premises used: UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors