awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
u : R[X]ˣ
rw : p.roots = (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) ((↑u : R[X]).coeff 0) : R[X])).roots
rw₁ : p.roots = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑u : R[X]).coeff 0) : R[X]) p).roots
⊢ p.roots = (p * (↑u : R[X])).roots
have rw₂ : p.roots = p.roots
Tactic: rw [eq_C_of_degree_eq_zero <| degree_coe_units u, mul_comm,
    roots_C_mul _ <| coeff_coe_units_zero_ne_zero u]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ (a • p).roots = p.roots
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots
Tactic: rw [smul_eq_C_mul, roots_C_mul _ ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ha : a ≠ 0
rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots
⊢ (a • p).roots = p.roots
have rw₁ : p.roots = p.roots
Tactic: rw [smul_eq_C_mul, roots_C_mul _ ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ (-p).roots = p.roots
have rw : (HSMul.hSMul (α := R) (-1) p).roots = p.roots
Tactic: rw [← neg_one_smul R p, roots_smul_nonzero p (neg_ne_zero.mpr one_ne_zero)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw : (HSMul.hSMul (α := R) (-1) p).roots = p.roots
⊢ (-p).roots = p.roots
have rw₁ : p.roots = p.roots
Tactic: rw [← neg_one_smul R p, roots_smul_nonzero p (neg_ne_zero.mpr one_ne_zero)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
⊢ (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {(↑a⁻¹ : R) * b}
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ((↑a⁻¹ : R) * b) : R[X])).roots = {(↑a⁻¹ : R) * b}
Tactic: rw [← roots_C_mul _ (Units.ne_zero a⁻¹), mul_sub, ← mul_assoc, ← C_mul, ← C_mul,
    Units.inv_mul, C_1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
have rw : (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
      (-(C : (a : R) → R[X]) b : R[X])).roots =
  {-((↑a⁻¹ : R) * b)}
Tactic: rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
rw :
  (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        (-(C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
have rw₁ : (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
      ((C : (a : R) → R[X]) (-b) : R[X])).roots =
  {-((↑a⁻¹ : R) * b)}
Tactic: rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
rw :
  (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        (-(C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
rw₁ :
  (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) (-b) : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
have rw₂ : Eq (α := Multiset R) {(↑a⁻¹ : R) * -b} {-((↑a⁻¹ : R) * b)}
Tactic: rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
rw :
  (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        (-(C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
rw₁ :
  (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) (-b) : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
rw₂ : Eq (α := Multiset R) {(↑a⁻¹ : R) * -b} {-((↑a⁻¹ : R) * b)}
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑a : R) : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {-((↑a⁻¹ : R) * b)}
have rw₃ : Eq (α := Multiset R) {-((↑a⁻¹ : R) * b)} {-((↑a⁻¹ : R) * b)}
Tactic: rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl : Multiset R[X]).bind roots
H : 0 ∉ hd :: tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
have H₁ : ¬0 = hd ∧ 0 ∉ tl
Tactic: rw [List.mem_cons, not_or] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl : Multiset R[X]).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
have rw : (hd * tl.prod).roots = (↑(hd :: tl) : Multiset R[X]).bind roots
Tactic: rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl : Multiset R[X]).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
rw : (hd * tl.prod).roots = (↑(hd :: tl) : Multiset R[X]).bind roots
⊢ (hd :: tl).prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
have rw₁ : hd.roots + tl.prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
Tactic: rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl : Multiset R[X]).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
rw : (hd * tl.prod).roots = (↑(hd :: tl) : Multiset R[X]).bind roots
rw₁ : hd.roots + tl.prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
⊢ (hd :: tl).prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
have rw₂ : hd.roots + tl.prod.roots = (hd ::ₘ (↑tl : Multiset R[X])).bind roots
Tactic: rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl : Multiset R[X]).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
rw : (hd * tl.prod).roots = (↑(hd :: tl) : Multiset R[X]).bind roots
rw₁ : hd.roots + tl.prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
rw₂ : hd.roots + tl.prod.roots = (hd ::ₘ (↑tl : Multiset R[X])).bind roots
⊢ (hd :: tl).prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
have rw₃ : hd.roots + tl.prod.roots = hd.roots + (↑tl : Multiset R[X]).bind roots
Tactic: rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl : Multiset R[X]).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
rw : (hd * tl.prod).roots = (↑(hd :: tl) : Multiset R[X]).bind roots
rw₁ : hd.roots + tl.prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
rw₂ : hd.roots + tl.prod.roots = (hd ::ₘ (↑tl : Multiset R[X])).bind roots
rw₃ : hd.roots + tl.prod.roots = hd.roots + (↑tl : Multiset R[X]).bind roots
⊢ (hd :: tl).prod.roots = (↑(hd :: tl) : Multiset R[X]).bind roots
have rw₄ : hd.roots + (↑tl : Multiset R[X]).bind roots = hd.roots + (↑tl : Multiset R[X]).bind roots
Tactic: rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
m : Multiset R[X]
⊢ 0 ∉ m → m.prod.roots = m.bind roots
have mk : ∀ (L : List R[X]),
  0 ∉ Quot.mk (⇑(List.isSetoid R[X]) : List R[X] → List R[X] → Prop) L →
    (prod (Quot.mk (⇑(List.isSetoid R[X]) : List R[X] → List R[X] → Prop) L)).roots =
      Multiset.bind (Quot.mk (⇑(List.isSetoid R[X]) : List R[X] → List R[X] → Prop) L) roots
Tactic: rcases m with ⟨L⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun (i : ι) ↦ (f i).roots
have rcases : ∀ (m : Multiset ι) (hm : m.Nodup),
  { val := m, nodup := hm : Finset ι }.prod f ≠ 0 →
    ({ val := m, nodup := hm : Finset ι }.prod f).roots =
      { val := m, nodup := hm : Finset ι }.val.bind fun (i : ι) ↦ (f i).roots
Tactic: rcases s with ⟨m, hm⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots
have zero : roots 1 = HSMul.hSMul (α := ℕ) 0 p.roots
Tactic: rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
zero : roots 1 = HSMul.hSMul (α := ℕ) 0 p.roots
⊢ (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots
have zero₁ : ∅ = HSMul.hSMul (α := ℕ) 0 p.roots
Tactic: rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
zero : roots 1 = HSMul.hSMul (α := ℕ) 0 p.roots
zero₁ : ∅ = HSMul.hSMul (α := ℕ) 0 p.roots
⊢ (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots
have zero₂ : Eq.{u + 1} (α := Multiset R) ∅ 0
Tactic: rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
zero : roots 1 = HSMul.hSMul (α := ℕ) 0 p.roots
zero₁ : ∅ = HSMul.hSMul (α := ℕ) 0 p.roots
zero₂ : Eq.{u + 1} (α := Multiset R) ∅ 0
⊢ (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots
have zero₃ : Eq.{u + 1} (α := Multiset R) 0 0
Tactic: rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ : ∀ (ihn : (HPow.hPow (α := R[X]) 0 n).roots = HSMul.hSMul (β := Multiset R) n (roots 0)),
  (HPow.hPow (α := R[X]) 0 (n + 1)).roots = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
Cleared hypotheses: p, ihn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
succ :
  ∀ (ihn : (HPow.hPow (α := R[X]) 0 n).roots = HSMul.hSMul (β := Multiset R) n (roots 0)),
    (HPow.hPow (α := R[X]) 0 (n + 1)).roots = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ₁ : ∀ (hp : p ≠ 0), (p ^ (n + 1)).roots = (n + 1) • p.roots
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ihn : (HPow.hPow (α := R[X]) 0 n).roots = HSMul.hSMul (β := Multiset R) n (roots 0)
⊢ (HPow.hPow (α := R[X]) 0 (n + 1)).roots = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
have succ : roots 0 = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
Tactic: rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ihn : (HPow.hPow (α := R[X]) 0 n).roots = HSMul.hSMul (β := Multiset R) n (roots 0)
succ : roots 0 = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
⊢ (HPow.hPow (α := R[X]) 0 (n + 1)).roots = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
have succ₁ : 0 = HSMul.hSMul (β := Multiset R) (n + 1) 0
Tactic: rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ihn : (HPow.hPow (α := R[X]) 0 n).roots = HSMul.hSMul (β := Multiset R) n (roots 0)
succ : roots 0 = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
succ₁ : 0 = HSMul.hSMul (β := Multiset R) (n + 1) 0
⊢ (HPow.hPow (α := R[X]) 0 (n + 1)).roots = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)
have succ₂ : Eq.{u + 1} (α := Multiset R) 0 0
Tactic: rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ : (p ^ n * p).roots = (n + 1) • p.roots
Tactic: rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
succ : (p ^ n * p).roots = (n + 1) • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ₁ : (p ^ n).roots + p.roots = (n + 1) • p.roots
Tactic: rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
succ : (p ^ n * p).roots = (n + 1) • p.roots
succ₁ : (p ^ n).roots + p.roots = (n + 1) • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ₂ : n • p.roots + p.roots = (n + 1) • p.roots
Tactic: rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
succ : (p ^ n * p).roots = (n + 1) • p.roots
succ₁ : (p ^ n).roots + p.roots = (n + 1) • p.roots
succ₂ : n • p.roots + p.roots = (n + 1) • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ₃ : n • p.roots + p.roots = n • p.roots + HSMul.hSMul (α := ℕ) 1 p.roots
Tactic: rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
succ : (p ^ n * p).roots = (n + 1) • p.roots
succ₁ : (p ^ n).roots + p.roots = (n + 1) • p.roots
succ₂ : n • p.roots + p.roots = (n + 1) • p.roots
succ₃ : n • p.roots + p.roots = n • p.roots + HSMul.hSMul (α := ℕ) 1 p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
have succ₄ : n • p.roots + p.roots = n • p.roots + p.roots
Tactic: rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
⊢ (p ^ n).roots = n • p.roots
have zero : (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots
Tactic: induction n with
  | zero => rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
  | succ n ihn =>
    rcases eq_or_ne p 0 with (rfl | hp)
    · rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
    · rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots
⊢ (p ^ n).roots = n • p.roots
have succ : ∀ (n : ℕ) (ihn : (p ^ n).roots = n • p.roots), (p ^ (n + 1)).roots = (n + 1) • p.roots
Tactic: induction n with
  | zero => rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
  | succ n ihn =>
    rcases eq_or_ne p 0 with (rfl | hp)
    · rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
    · rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).roots = HSMul.hSMul (β := Multiset R) n {0}
have rw : HSMul.hSMul (β := Multiset R) n (roots X) = HSMul.hSMul (β := Multiset R) n {0}
Tactic: rw [roots_pow, roots_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : HSMul.hSMul (β := Multiset R) n (roots X) = HSMul.hSMul (β := Multiset R) n {0}
⊢ (HPow.hPow (α := R[X]) X n).roots = HSMul.hSMul (β := Multiset R) n {0}
have rw₁ : HSMul.hSMul (β := Multiset R) n {0} = HSMul.hSMul (β := Multiset R) n {0}
Tactic: rw [roots_pow, roots_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).roots =
    HSMul.hSMul (β := Multiset R) n {0}
have rw : (HPow.hPow (α := R[X]) X n).roots = HSMul.hSMul (β := Multiset R) n {0}
Tactic: rw [roots_C_mul _ ha, roots_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
ha : a ≠ 0
n : ℕ
rw : (HPow.hPow (α := R[X]) X n).roots = HSMul.hSMul (β := Multiset R) n {0}
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).roots =
    HSMul.hSMul (β := Multiset R) n {0}
have rw₁ : HSMul.hSMul (β := Multiset R) n {0} = HSMul.hSMul (β := Multiset R) n {0}
Tactic: rw [roots_C_mul _ ha, roots_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ roots ((monomial n : (a : R) → R[X]) a) = HSMul.hSMul (β := Multiset R) n {0}
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).roots =
  HSMul.hSMul (β := Multiset R) n {0}
Tactic: rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
ha : a ≠ 0
n : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).roots =
    HSMul.hSMul (β := Multiset R) n {0}
⊢ roots ((monomial n : (a : R) → R[X]) a) = HSMul.hSMul (β := Multiset R) n {0}
have rw₁ : HSMul.hSMul (β := Multiset R) n {0} = HSMul.hSMul (β := Multiset R) n {0}
Tactic: rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
⊢ roots (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = s.val
have apply : (s.val.bind fun (i : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).roots) = s.val
Tactic: apply (roots_prod (fun a => X - C a) s ?_).trans
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
apply : (s.val.bind fun (i : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).roots) = s.val
⊢ roots (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = s.val
have apply₁ : Ne (α := R[X]) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0
Tactic: apply (roots_prod (fun a => X - C a) s ?_).trans
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
⊢ (s.val.bind fun (i : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).roots) = s.val
have simp_rw : (s.val.bind fun (i : R) ↦ {i}) = s.val
Tactic: simp_rw [roots_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
⊢ (s.val.bind fun (i : R) ↦ {i}) = s.val
have rw : Multiset.map (fun (i : R) ↦ i) s.val = s.val
Tactic: rw [Multiset.bind_singleton, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
rw : Multiset.map (fun (i : R) ↦ i) s.val = s.val
⊢ (s.val.bind fun (i : R) ↦ {i}) = s.val
have rw₁ : s.val = s.val
Tactic: rw [Multiset.bind_singleton, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
⊢ roots (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s)) = s
have rw : (s.bind fun (a : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots) = s
Tactic: rw [roots_multiset_prod, Multiset.bind_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
rw : (s.bind fun (a : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots) = s
⊢ roots (prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s)) = s
have a : 0 ∉ Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s
Tactic: rw [roots_multiset_prod, Multiset.bind_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
⊢ (s.bind fun (a : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots) = s
have simp_rw : (s.bind fun (a : R) ↦ {a}) = s
Tactic: simp_rw [roots_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
⊢ (s.bind fun (a : R) ↦ {a}) = s
have rw : Multiset.map (fun (a : R) ↦ a) s = s
Tactic: rw [Multiset.bind_singleton, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
rw : Multiset.map (fun (a : R) ↦ a) s = s
⊢ (s.bind fun (a : R) ↦ {a}) = s
have rw₁ : s = s
Tactic: rw [Multiset.bind_singleton, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s
have a : ¬∃ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0
Tactic: rw [Multiset.mem_map]