awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
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
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))
have x : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))
have x : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have rw : (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r
Tactic: rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have rw₁ : (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p.natDegree + q.natDegree)) • (p * q).scaleRoots r
Tactic: rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have rw₂ : (p * q).scaleRoots r = HPow.hPow (β := ℕ) r 0 • (p * q).scaleRoots r
Tactic: rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have rw₃ : (p * q).scaleRoots r = HSMul.hSMul (α := R) 1 ((p * q).scaleRoots r)
Tactic: rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have rw₄ : (p * q).scaleRoots r = (p * q).scaleRoots r
Tactic: rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have pos : ∀ (hp : p = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have neg : ∀ (hp : ¬p = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have pos : ∀ (hq : q = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
have neg : ∀ (hq : ¬q = 0), (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have neg : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: apply mul_scaleRoots'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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 ^ (n + 1)).scaleRoots r = p.scaleRoots r ^ (n + 1)
have succ : p.leadingCoeff ^ n ≠ 0
Tactic: rw [pow_succ, mul_scaleRoots', IH, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p ^ (n + 1)).scaleRoots r = p.scaleRoots r ^ (n + 1)
have succ₁ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Tactic: rw [pow_succ, mul_scaleRoots', IH, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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 ^ n).leadingCoeff * p.leadingCoeff ≠ 0
have succ : p.leadingCoeff ^ n * p.leadingCoeff ≠ 0
Tactic: rwa [leadingCoeff_pow' (mt (by simp +contextual [pow_succ]) hp), ← pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
n : ℕ
hp : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
have zero : ∀ (hp : HPow.hPow (β := ℕ) p.leadingCoeff 0 ≠ 0),
  (HPow.hPow (β := ℕ) p 0).scaleRoots r = HPow.hPow (β := ℕ) (p.scaleRoots r) 0
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]
Cleared hypotheses: n, hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
have 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)
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]
Cleared hypotheses: n, hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsReduced R
p : R[X]
r : R
n : ℕ
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
have pos : ∀ (hp : p = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
have neg : ∀ (hp : ¬p = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have pos : ∀ (hn : n = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
have neg : ∀ (hn : ¬n = 0), (p ^ n).scaleRoots r = p.scaleRoots r ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
⊢ r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r
have a : ∀ (n : ℕ),
  (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n
have 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)
Tactic: simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul,
    mul_comm (r ^ _), ← h, ← add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.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)
have 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)
Tactic: rw [mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (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)
have 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)
Tactic: rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ (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)
have a₁ : (p.coeff n + q.coeff n) * r ^ (p.natDegree - n) = (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = 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)
have x : (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r
have obtain : ∀ (a : R[X]), p.scaleRoots r ∣ (p * a).scaleRoots r
Tactic: obtain ⟨a, rfl⟩ := hpq
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r
have rw : p.scaleRoots r ∣ p.scaleRoots r * 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
inst_1 : NoZeroDivisors R
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r
have obtain : ∀ (a : R[X]), p.scaleRoots r ∣ (p * a).scaleRoots r
Tactic: obtain ⟨a, rfl⟩ := hpq
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
inst_1 : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r
have rw : p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
Tactic: rw [mul_scaleRoots_of_noZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have refine : (p.scaleRoots r).scaleRoots (↑hr.unit⁻¹ : R) ∣ (q.scaleRoots r).scaleRoots (↑hr.unit⁻¹ : R) → p ∣ q
Tactic: refine ⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
h : IsCoprime p q
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)
have obtain : ∀ (a b : R[X]) (e : a * p + b * q = 1), IsCoprime (p.scaleRoots r) (q.scaleRoots r)
Tactic: obtain ⟨a, b, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have H : (a * p + b * q).natDegree = 0
Tactic: apply natDegree_eq_of_natDegree_add_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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 + b * q).natDegree = 0
have H : natDegree.{u_1} (R := R) 1 = 0
Tactic: rw [e, natDegree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (a * p + b * q).natDegree = 0
have H₁ : Eq (α := ℕ) 0 0
Tactic: rw [e, natDegree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
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)
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)
have this : (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)
have 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
Tactic: use s ^ natDegree (a * p) • s ^ (natDegree a + natDegree p - natDegree (a * p)) • a.scaleRoots r
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ ∃ (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
have 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
Tactic: use s ^ natDegree (a * p) • s ^ (natDegree b + natDegree q - natDegree (b * q)) • b.scaleRoots r
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
⊢ (p.scaleRoots r).Splits
have inl : Subsingleton R → (p.scaleRoots r).Splits
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
inl : Subsingleton R → (p.scaleRoots r).Splits
⊢ (p.scaleRoots r).Splits
have inr : Nontrivial R → (p.scaleRoots r).Splits
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
⊢ (p.scaleRoots r).Splits
have inr : ∀ (hp : Splits.{u_1} (R := R) 0), Splits (Polynomial.scaleRoots 0 r)
Tactic: obtain rfl | hp0 := eq_or_ne p 0
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ (p.scaleRoots r).Splits
have inr₁ : ∀ (hp0 : p ≠ 0), (p.scaleRoots r).Splits
Tactic: obtain rfl | hp0 := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
⊢ (p.scaleRoots r).Splits
have 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
Tactic: obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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])
⊢ (p.scaleRoots r).Splits
have 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
Tactic: rw [hm, mul_scaleRoots', scaleRoots_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (p.scaleRoots r).Splits
have 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
Tactic: rw [hm, mul_scaleRoots', scaleRoots_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
have 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)
Tactic: refine .mul (.C _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH :
  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])) s))
      r)
⊢ 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])) (a ::ₘ s)))
      r)
have inr : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (a * r) : 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])) s))
      r).Splits
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, mul_scaleRoots', X_add_C_scaleRoots]