awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
hb : b ≤ q.natDegree
inr :
  p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b))) =
    p.coeff a * (q.coeff b * r ^ (p.natDegree - a + (q.natDegree - b)))
inr₁ inr₂ :
  p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b))) =
    p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b)))
⊢ p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b))) =
    p.coeff a * (q.coeff b * r ^ (q.natDegree - b + (p.natDegree - a)))

Tactic:
rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Premises used: HSub.hSub, tsub_add_tsub_comm, add_comm
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
⊢ q.natDegree < b ∨ b ≤ q.natDegree

Tactic:
cases lt_or_ge (natDegree q) b with
      | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
      | inr hb =>
        simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
        rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Premises used: MulZeroClass.zero_mul, mul_assoc, HSub.hSub, pow_add, add_comm, MulZeroClass.mul_zero, HPow.hPow, mul_comm, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
⊢ p.natDegree < a ∨ a ≤ p.natDegree

Tactic:
cases lt_or_ge (natDegree p) a with
    | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
    | inr ha =>
      cases lt_or_ge (natDegree q) b with
      | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
      | inr hb =>
        simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
        rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Premises used: MulZeroClass.zero_mul, mul_assoc, HSub.hSub, pow_add, add_comm, MulZeroClass.mul_zero, HPow.hPow, mul_comm, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
rw : (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r
rw₁ : (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p.natDegree + q.natDegree)) • (p * q).scaleRoots r
rw₂ : (p * q).scaleRoots r = HPow.hPow (β := ℕ) r 0 • (p * q).scaleRoots r
rw₃ : (p * q).scaleRoots r = HSMul.hSMul (α := R) 1 ((p * q).scaleRoots r)
rw₄ rw₅ : (p * q).scaleRoots r = (p * q).scaleRoots r
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]

Premises used: tsub_self, Polynomial.natDegree_mul', pow_zero, one_smul, Polynomial.mul_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
pos : ∀ (hp : p = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
neg : ∀ (hp : ¬p = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hp : p = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
simp [hp]
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hp : ¬p = 0
pos : ∀ (hq : q = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
neg : ∀ (hq : ¬q = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
simp [hq]
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
neg : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
apply mul_scaleRoots'

Premises used: Polynomial.mul_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero, hp, hq, or_self, not_false_eq_true]

Premises used: mul_eq_zero, ne_eq, or_self, not_false_eq_true, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
hp : HPow.hPow (β := ℕ) p.leadingCoeff 0 ≠ 0
⊢ (HPow.hPow (β := ℕ) p 0).scaleRoots r = HPow.hPow (β := ℕ) (p.scaleRoots r) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : ∀ (hp : p.leadingCoeff ^ n ≠ 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
succ : p.leadingCoeff ^ n ≠ 0
succ₁ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ (n + 1)).scaleRoots r = p.scaleRoots r ^ (n + 1)

Tactic:
rw [pow_succ, mul_scaleRoots', IH, pow_succ]

Premises used: pow_succ, Polynomial.mul_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : ∀ (hp : p.leadingCoeff ^ n ≠ 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n = 0 → p.leadingCoeff ^ (n + 1) = 0

Tactic:
simp +contextual [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : ∀ (hp : p.leadingCoeff ^ n ≠ 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
refine mt (by simp +contextual [pow_succ]) hp

Premises used: mt
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : ∀ (hp : p.leadingCoeff ^ n ≠ 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
succ : p.leadingCoeff ^ n * p.leadingCoeff ≠ 0
succ₁ succ₂ succ₃ succ₄ : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
rwa [leadingCoeff_pow' (mt (by simp +contextual [pow_succ]) hp), ← pow_succ]

Premises used: pow_succ, mt, Polynomial.leadingCoeff_pow'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
n : ℕ
hp : p.leadingCoeff ^ n ≠ 0
zero :
  ∀ (hp : HPow.hPow (β := ℕ) p.leadingCoeff 0 ≠ 0),
    (HPow.hPow (β := ℕ) p 0).scaleRoots r = HPow.hPow (β := ℕ) (p.scaleRoots r) 0
succ :
  ∀ (n : ℕ) (IH : ∀ (hp : p.leadingCoeff ^ n ≠ 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n)
    (hp : p.leadingCoeff ^ (n + 1) ≠ 0), (p ^ (n + 1)).scaleRoots r = p.scaleRoots r ^ (n + 1)
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
induction n with
  | zero => simp
  | succ n IH =>
    rw [pow_succ, mul_scaleRoots', IH, pow_succ]
    · refine mt (by simp +contextual [pow_succ]) hp
    · rwa [leadingCoeff_pow' (mt (by simp +contextual [pow_succ]) hp), ← pow_succ]

Premises used: pow_succ, mt, Polynomial.leadingCoeff_pow', Polynomial.mul_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
pos : ∀ (hp : p = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
neg : ∀ (hp : ¬p = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
hp : p = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
simp [hp, zero_pow_eq, apply_ite (scaleRoots · r)]

Premises used: apply_ite, zero_pow_eq, Polynomial.scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
pos : ∀ (hn : n = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
neg : ∀ (hn : ¬n = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : n = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
exact pow_scaleRoots' _ _ _ (by simp_all)

Premises used: Polynomial.pow_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
a :
  ∀ (n : ℕ),
    (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n
⊢ r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r

Tactic:
ext n
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
a :
  (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
⊢ (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n

Tactic:
simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul,
    mul_comm (r ^ _), ← h, ← add_mul]

Premises used: add_mul, Polynomial.coeff_scaleRoots, Polynomial.coeff_add, Polynomial.coeff_smul, HPow.hPow, mul_comm, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
a :
  (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
rw [mul_assoc, ← pow_add]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : (p + q).natDegree < n
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_add, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : n ≤ (p + q).natDegree
a :
  (p.coeff n + q.coeff n) * r ^ (p.natDegree - (p + q).natDegree + ((p + q).natDegree - n)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
a₁ a₂ : (p.coeff n + q.coeff n) * r ^ (p.natDegree - n) = (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]

Premises used: Eq.ge, le_rfl, HSub.hSub, Polynomial.natDegree_add_le_of_degree_le, add_comm, tsub_add_tsub_cancel
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p + q).natDegree < n ∨ n ≤ (p + q).natDegree

Tactic:
cases lt_or_ge (natDegree (p + q)) n with
  | inl hn => simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]
  | inr hn =>
      rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]

Premises used: MulZeroClass.zero_mul, HSub.hSub, Polynomial.coeff_add, add_comm, HAdd.hAdd, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
hpq : p ∣ q
obtain : ∀ (a : R[X]), p.scaleRoots r ∣ (p * a).scaleRoots r
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
obtain ⟨a, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
rw : p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Tactic:
rw [← ((hr.pow (natDegree p + natDegree a - natDegree (p * a))).map
    (algebraMap R R[X])).dvd_mul_left, ← Algebra.smul_def, mul_scaleRoots]

Premises used: IsUnit.dvd_mul_left, HMul.hMul, Algebra.algebraMap, HSub.hSub, IsUnit.pow, Polynomial, Polynomial.mul_scaleRoots, HAdd.hAdd, IsUnit.map, Algebra.smul_def, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Tactic:
dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Premises used: Polynomial.scaleRoots, dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Tactic:
exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Premises used: Polynomial.scaleRoots, dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hpq : p ∣ q
obtain : ∀ (a : R[X]), p.scaleRoots r ∣ (p * a).scaleRoots r
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
obtain ⟨a, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
inst_1 : NoZeroDivisors R
a : R[X]
rw : p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Tactic:
rw [mul_scaleRoots_of_noZeroDivisors]

Premises used: Polynomial.mul_scaleRoots_of_noZeroDivisors
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
inst_1 : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Tactic:
dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Premises used: Polynomial.scaleRoots, dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
inst_1 : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Tactic:
exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Premises used: Polynomial.scaleRoots, dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Tactic:
⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩

Premises used: Polynomial.scaleRoots_dvd', Function.comp, Inv.inv, Iff.intro, IsUnit.unit, Units.isUnit
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
refine : (p.scaleRoots r).scaleRoots (↑hr.unit⁻¹ : R) ∣ (q.scaleRoots r).scaleRoots (↑hr.unit⁻¹ : R) → p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Tactic:
refine ⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).scaleRoots (↑hr.unit⁻¹ : R) ∣ (q.scaleRoots r).scaleRoots (↑hr.unit⁻¹ : R) → p ∣ q

Tactic:
simp [← scaleRoots_mul, scaleRoots_one]

Premises used: Polynomial.scaleRoots_mul, Polynomial.scaleRoots_one
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
h : IsCoprime p q
obtain : ∀ (a b : R[X]) (e : a * p + b * q = 1), IsCoprime (p.scaleRoots r) (q.scaleRoots r)
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
obtain ⟨a, b, e⟩ := h
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := (↑hr.unit⁻¹ : R)
H : (a * p + b * q).natDegree = 0
⊢ (a * p).natDegree = (b * q).natDegree

Tactic:
apply natDegree_eq_of_natDegree_add_eq_zero

Premises used: Polynomial.natDegree_eq_of_natDegree_add_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := (↑hr.unit⁻¹ : R)
H : natDegree.{u_1} (R := R) 1 = 0
H₁ H₂ : Eq (α := ℕ) 0 0
⊢ (a * p + b * q).natDegree = 0

Tactic:
rw [e, natDegree_one]

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := (↑hr.unit⁻¹ : R)
⊢ (a * p).natDegree = (b * q).natDegree

Tactic:
have : natDegree (a * p) = natDegree (b * q) := by
    apply natDegree_eq_of_natDegree_add_eq_zero
    rw [e, natDegree_one]
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := (↑hr.unit⁻¹ : R)
this : (a * p).natDegree = (b * q).natDegree
h :
  ∃ (b : R[X]),
    s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
        b * q.scaleRoots r =
      1
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
use s ^ natDegree (a * p) • s ^ (natDegree a + natDegree p - natDegree (a * p)) • a.scaleRoots r

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd, Polynomial.scaleRoots, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := (↑hr.unit⁻¹ : R)
this : (a * p).natDegree = (b * q).natDegree
h :
  s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
      s ^ (a * p).natDegree • s ^ (b.natDegree + q.natDegree - (b * q).natDegree) • b.scaleRoots r * q.scaleRoots r =
    1
⊢ ∃ (b : R[X]),
    s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
        b * q.scaleRoots r =
      1

Tactic:
use s ^ natDegree (a * p) • s ^ (natDegree b + natDegree q - natDegree (b * q)) • b.scaleRoots r

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd, Polynomial.scaleRoots, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := (↑hr.unit⁻¹ : R)
this : (a * p).natDegree = (b * q).natDegree
⊢ s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
      s ^ (a * p).natDegree • s ^ (b.natDegree + q.natDegree - (b * q).natDegree) • b.scaleRoots r * q.scaleRoots r =
    1

Tactic:
simp only [smul_smul, smul_mul_assoc, ← mul_scaleRoots, mul_assoc, ← mul_pow, IsUnit.val_inv_mul,
    one_pow, mul_one, ← smul_add, ← add_scaleRoots_of_natDegree_eq _ _ _ this, e, natDegree_one,
    Nat.sub_zero, one_scaleRoots, one_smul, s]

Premises used: one_pow, Polynomial.one_scaleRoots, mul_assoc, smul_smul, smul_mul_assoc, one_smul, Polynomial.mul_scaleRoots, Polynomial.natDegree_one, Nat.sub_zero, mul_one, IsUnit.val_inv_mul, mul_pow, smul_add, Polynomial.add_scaleRoots_of_natDegree_eq
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
inl : Subsingleton R → (p.scaleRoots r).Splits
inr : Nontrivial R → (p.scaleRoots r).Splits
⊢ (p.scaleRoots r).Splits

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Subsingleton R
inl inl₁ inl₂ inl₃ : p.Splits
⊢ (p.scaleRoots r).Splits

Tactic:
rwa [Subsingleton.elim (p.scaleRoots r) p]

Premises used: Polynomial.scaleRoots, Subsingleton.elim
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
inr : ∀ (hp : Splits.{u_1} (R := R) 0), Splits (Polynomial.scaleRoots 0 r)
inr₁ : ∀ (hp0 : p ≠ 0), (p.scaleRoots r).Splits
⊢ (p.scaleRoots r).Splits

Tactic:
obtain rfl | hp0 := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
r : R
h : Nontrivial R
hp : Splits.{u_1} (R := R) 0
⊢ Splits (Polynomial.scaleRoots 0 r)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
inr :
  ∀ (m : Multiset R)
    (hm :
      p =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])),
    (p.scaleRoots r).Splits
⊢ (p.scaleRoots r).Splits

Tactic:
obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hp

Premises used: Iff.mp, Polynomial.splits_iff_exists_multiset'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm :
  p =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
inr :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
        r)).Splits
inr₁ :
  HMul.hMul (α := R) (leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff))
      (leadingCoeff
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))) ≠
    0
⊢ (p.scaleRoots r).Splits

Tactic:
rw [hm, mul_scaleRoots', scaleRoots_C]

Premises used: Polynomial.scaleRoots_C, Polynomial.mul_scaleRoots'
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
        r)).Splits

Tactic:
.mul (.C _) ?_

Premises used: Polynomial.Splits.C, Polynomial.Splits.mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
inr :
  Splits
    (Polynomial.scaleRoots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
      r)
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (Polynomial.scaleRoots
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
        r)).Splits

Tactic:
refine .mul (.C _) ?_