awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a x : R
rw :
  HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]) ≠ 0 ∧
      (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔
    p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a
rw₁ :
  HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]) ≠ 0 ∧
      eval x (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = 0 ↔
    p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a
rw₂ :
  p ≠ (C : (a : R) → R[X]) a ∧ eval x (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = 0 ↔
    p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a
rw₃ :
  p ≠ (C : (a : R) → R[X]) a ∧ eval x p - eval x ((C : (a : R) → R[X]) a) = 0 ↔
    p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a
rw₄ :
  p ≠ (C : (a : R) → R[X]) a ∧ eval x p = eval x ((C : (a : R) → R[X]) a) ↔ p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a
rw₅ rw₆ : p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a ↔ p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a
⊢ x ∈ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).roots ↔ p ≠ (C : (a : R) → R[X]) a ∧ eval x p = a

Tactic:
rw [mem_roots', IsRoot.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]

Premises used: Polynomial.eval_C, sub_eq_zero, sub_ne_zero, Polynomial.IsRoot.def, Polynomial.mem_roots', Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a x : R
hp0 : 0 < p.degree
⊢ x ∈ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).roots ↔ eval x p = a

Tactic:
mem_roots_sub_C'.trans <| and_iff_right fun hp => hp0.not_ge <| hp.symm ▸ degree_C_le

Premises used: Polynomial.mem_roots_sub_C', Eq.rec, and_iff_right, Iff.trans, LT.lt.not_ge, Eq.symm, Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
a : ∀ (s : R), count s (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).roots = count s {r}
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).roots = {r}

Tactic:
ext s
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r s : R
a : rootMultiplicity s (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = count s {r}
a₁ : (if s = r then 1 else 0) = count s {r}
a₂ a₃ : Eq (α := ℕ) (if s = r then 1 else 0) (if s = r then 1 else 0)
⊢ count s (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).roots = count s {r}

Tactic:
rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

Premises used: Polynomial.count_roots, Polynomial.rootMultiplicity_X_sub_C, Multiset.count_singleton
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
a : ∀ (s : R), count s (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).roots = count s {r}
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).roots = {r}

Tactic:
classical
  ext s
  rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

Premises used: Polynomial.count_roots, Polynomial.rootMultiplicity_X_sub_C, Multiset.count_singleton
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).roots = {-r}

Tactic:
simpa using roots_X_sub_C (-r)

Premises used: Polynomial.roots_X_sub_C, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
rw : roots X = (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)).roots
rw₁ : roots X = (HSub.hSub (α := R[X]) X 0).roots
rw₂ rw₃ : Eq.{u + 1} (α := Multiset R) (roots X) (roots X)
⊢ Eq (α := Multiset R) (roots X) {0}

Tactic:
rw [← roots_X_sub_C, C_0, sub_zero]

Premises used: sub_zero, Polynomial.C_0, Polynomial.roots_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
x : R
H : x = 0
rw : Eq.{u + 1} (α := Multiset R) (roots ((C : (a : R) → R[X]) 0)) 0
rw₁ : Eq.{u + 1} (α := Multiset R) (roots 0) 0
rw₂ rw₃ : Eq.{u + 1} (α := Multiset R) 0 0
⊢ Eq.{u + 1} (α := Multiset R) (roots ((C : (a : R) → R[X]) x)) 0

Tactic:
rw [H, C_0, roots_zero]

Premises used: Polynomial.roots_zero, Polynomial.C_0
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
x : R
H : ¬x = 0
r : R
rw : rootMultiplicity r ((C : (a : R) → R[X]) x) = count r 0
rw₁ : rootMultiplicity r ((C : (a : R) → R[X]) x) = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ count r (roots ((C : (a : R) → R[X]) x)) = count r 0

Tactic:
rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)]

Premises used: Polynomial.not_isRoot_C, Polynomial.count_roots, Multiset.count_zero, Polynomial.rootMultiplicity_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
x : R
⊢ Eq.{u + 1} (α := Multiset R) (roots ((C : (a : R) → R[X]) x)) 0

Tactic:
exact
  if H : x = 0 then by rw [H, C_0, roots_zero]
  else
    Multiset.ext.mpr fun r => (by
      rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)])

Premises used: Iff.mpr, Multiset.ext
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
x : R
⊢ Eq.{u + 1} (α := Multiset R) (roots ((C : (a : R) → R[X]) x)) 0

Tactic:
classical exact
  if H : x = 0 then by rw [H, C_0, roots_zero]
  else
    Multiset.ext.mpr fun r => (by
      rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)])

Premises used: Iff.mpr, Multiset.ext
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq.{u + 1} (α := Multiset R) (roots 1) ∅

Tactic:
roots_C 1

Premises used: OfNat.ofNat, Polynomial.roots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ha : a ≠ 0
pos : ∀ (hp : p = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots
neg : ∀ (hp : ¬p = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ha : a ≠ 0
hp : p = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots

Tactic:
simp only [roots_mul, *, Ne, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C,
      zero_add, mul_zero]

Premises used: Polynomial.C_eq_zero, or_self_iff, Ne, zero_add, mul_eq_zero, MulZeroClass.mul_zero, Polynomial.roots_mul, not_false_iff, Polynomial.roots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).roots = p.roots

Tactic:
simp only [roots_mul, *, Ne, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C,
      zero_add, mul_zero]

Premises used: Polynomial.C_eq_zero, or_self_iff, Ne, zero_add, mul_eq_zero, MulZeroClass.mul_zero, Polynomial.roots_mul, not_false_iff, Polynomial.roots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Associated p q
obtain : ∀ (u : R[X]ˣ), p.roots = (p * (↑u : R[X])).roots
⊢ p.roots = q.roots

Tactic:
obtain ⟨u, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
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
rw₂ rw₃ : p.roots = p.roots
⊢ p.roots = (p * (↑u : R[X])).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]

Premises used: Polynomial.eq_C_of_degree_eq_zero, Polynomial.roots_C_mul, Polynomial.coeff_coe_units_zero_ne_zero, mul_comm, Polynomial.degree_coe_units
-- Module: Mathlib.Algebra.Polynomial.Roots
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
rw₁ rw₂ : p.roots = p.roots
⊢ (a • p).roots = p.roots

Tactic:
rw [smul_eq_C_mul, roots_C_mul _ ha]

Premises used: Polynomial.roots_C_mul, Polynomial.smul_eq_C_mul
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw : (HSMul.hSMul (α := R) (-1) p).roots = p.roots
rw₁ rw₂ : p.roots = p.roots
⊢ (-p).roots = p.roots

Tactic:
rw [← neg_one_smul R p, roots_smul_nonzero p (neg_ne_zero.mpr one_ne_zero)]

Premises used: Iff.mpr, neg_one_smul, Polynomial.roots_smul_nonzero, neg_ne_zero, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ((↑a⁻¹ : R) * b) : R[X])).roots = {(↑a⁻¹ : R) * b}
⊢ (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 [← roots_C_mul _ (Units.ne_zero a⁻¹), mul_sub, ← mul_assoc, ← C_mul, ← C_mul,
    Units.inv_mul, C_1, one_mul]

Premises used: Polynomial.C_1, Polynomial.roots_C_mul, mul_sub, mul_assoc, Units.inv_mul, Units.ne_zero, Inv.inv, Polynomial.C_mul, one_mul
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ((↑a⁻¹ : R) * b) : R[X])).roots = {(↑a⁻¹ : R) * b}

Tactic:
roots_X_sub_C (a⁻¹ * b)

Premises used: Units.val, HMul.hMul, Polynomial.roots_X_sub_C, Inv.inv
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
b : R
a : Rˣ
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ((↑a⁻¹ : R) * b) : R[X])).roots = {(↑a⁻¹ : R) * b}

Tactic:
exact roots_X_sub_C (a⁻¹ * b)

Premises used: Units.val, HMul.hMul, Polynomial.roots_X_sub_C, Inv.inv
-- Module: Mathlib.Algebra.Polynomial.Roots
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)}
rw₃ 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)}

Tactic:
rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]

Premises used: Polynomial.roots_C_mul_X_sub_C_of_IsUnit, Polynomial.C_neg, sub_neg_eq_add, mul_neg
-- Module: Mathlib.Algebra.Polynomial.Roots
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
⊢ ¬0 = hd ∧ 0 ∉ tl

Tactic:
rw [List.mem_cons, not_or] at H

Premises used: not_or, List.mem_cons
-- Module: Mathlib.Algebra.Polynomial.Roots
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
rw₄ rw₅ : hd.roots + (↑tl : Multiset R[X]).bind roots = hd.roots + (↑tl : Multiset R[X]).bind roots
⊢ (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]

Premises used: Ne.symm, And.right, And.left, Polynomial.roots_mul, List.prod_ne_zero, Multiset.cons_coe, mul_ne_zero, List.prod_cons, Multiset.cons_bind
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
m : Multiset R[X]
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
⊢ 0 ∉ m → m.prod.roots = m.bind roots

Tactic:
rcases m with ⟨L⟩
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
m : Multiset R[X]
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:
simpa only [Multiset.prod_coe, quot_mk_to_coe''] using roots_list_prod L

Premises used: Polynomial.roots_list_prod, Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
ι : Type u_1
f : ι → R[X]
s : Finset ι
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
⊢ s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun (i : ι) ↦ (f i).roots

Tactic:
rcases s with ⟨m, hm⟩
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
ι : Type u_1
f : ι → R[X]
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:
simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)

Premises used: Multiset.map, Multiset.prod_eq_zero_iff, Polynomial.roots_multiset_prod, Multiset.bind_map
-- Module: Mathlib.Algebra.Polynomial.Roots
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
zero₃ zero₄ : Eq.{u + 1} (α := Multiset R) 0 0
⊢ (HPow.hPow (β := ℕ) p 0).roots = HSMul.hSMul (α := ℕ) 0 p.roots

Tactic:
rw [pow_zero, roots_one, zero_smul, empty_eq_zero]

Premises used: pow_zero, Multiset.empty_eq_zero, zero_smul, Polynomial.roots_one
-- Module: Mathlib.Algebra.Polynomial.Roots
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)
succ₁ : ∀ (hp : p ≠ 0), (p ^ (n + 1)).roots = (n + 1) • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
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
succ₂ succ₃ : Eq.{u + 1} (α := Multiset R) 0 0
⊢ (HPow.hPow (α := R[X]) 0 (n + 1)).roots = HSMul.hSMul (β := Multiset R) (n + 1) (roots 0)

Tactic:
rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]

Premises used: Polynomial.roots_zero, smul_zero, Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.Algebra.Polynomial.Roots
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
succ₄ succ₅ : n • p.roots + p.roots = n • p.roots + p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]

Premises used: pow_succ, pow_ne_zero, one_smul, add_smul, Polynomial.roots_mul, mul_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
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
succ : ∀ (n : ℕ) (ihn : (p ^ n).roots = n • p.roots), (p ^ (n + 1)).roots = (n + 1) • p.roots
⊢ (p ^ n).roots = n • 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]

Premises used: Polynomial.roots_zero, pow_succ, smul_zero, pow_zero, Multiset.empty_eq_zero, one_smul, zero_smul, Nat.succ_ne_zero, add_smul, Polynomial.roots_one, eq_or_ne, OfNat.ofNat, zero_pow, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
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}
rw₁ rw₂ : HSMul.hSMul (β := Multiset R) n {0} = HSMul.hSMul (β := Multiset R) n {0}
⊢ (HPow.hPow (α := R[X]) X n).roots = HSMul.hSMul (β := Multiset R) n {0}

Tactic:
rw [roots_pow, roots_X]

Premises used: Polynomial.roots_pow, Polynomial.roots_X
-- Module: Mathlib.Algebra.Polynomial.Roots
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}
rw₁ rw₂ : HSMul.hSMul (β := Multiset R) n {0} = 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}

Tactic:
rw [roots_C_mul _ ha, roots_X_pow]

Premises used: Polynomial.roots_C_mul, Polynomial.roots_X_pow
-- Module: Mathlib.Algebra.Polynomial.Roots
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}
rw₁ rw₂ : HSMul.hSMul (β := Multiset R) n {0} = HSMul.hSMul (β := Multiset R) n {0}
⊢ roots ((monomial n : (a : R) → R[X]) a) = HSMul.hSMul (β := Multiset R) n {0}

Tactic:
rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]

Premises used: Polynomial.roots_C_mul_X_pow, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Roots
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
apply₁ : Ne (α := R[X]) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0
⊢ roots (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = s.val

Tactic:
apply (roots_prod (fun a => X - C a) s ?_).trans

Premises used: Polynomial.C, HSub.hSub, Polynomial.roots_prod, Polynomial.X, DFunLike.coe, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
simp_rw : (s.val.bind fun (i : R) ↦ {i}) = s.val
⊢ (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:
simp_rw [roots_X_sub_C]

Premises used: Polynomial.roots_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Roots
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
rw₁ rw₂ : s.val = s.val
⊢ (s.val.bind fun (i : R) ↦ {i}) = s.val

Tactic:
rw [Multiset.bind_singleton, Multiset.map_id']

Premises used: Multiset.bind_singleton, Multiset.map_id'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
⊢ Ne (α := R[X]) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0

Tactic:
prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Finset R
⊢ Ne (α := R[X]) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0

Tactic:
refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
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
a : 0 ∉ Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 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

Tactic:
rw [roots_multiset_prod, Multiset.bind_map]

Premises used: Polynomial.roots_multiset_prod, Multiset.bind_map
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
simp_rw : (s.bind fun (a : R) ↦ {a}) = s
⊢ (s.bind fun (a : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots) = s

Tactic:
simp_rw [roots_X_sub_C]

Premises used: Polynomial.roots_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
rw : Multiset.map (fun (a : R) ↦ a) s = s
rw₁ rw₂ : s = s
⊢ (s.bind fun (a : R) ↦ {a}) = s

Tactic:
rw [Multiset.bind_singleton, Multiset.map_id']

Premises used: Multiset.bind_singleton, Multiset.map_id'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
a : ¬∃ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ 0 ∉ Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s

Tactic:
rw [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
a : R
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ False

Tactic:
X_sub_C_ne_zero a h

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
a : R
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ False

Tactic:
exact X_sub_C_ne_zero a h

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
⊢ roots ((ofMultiset : (a : Multiset R) → R[X]) s) = s

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Function.RightInverse.{u + 1, u + 1} (α := R[X]) (⇑ofMultiset : (a : Multiset R) → R[X]) roots

Tactic:
roots_ofMultiset

Premises used: Function.LeftInverse, Polynomial.roots_ofMultiset, Function.RightInverse
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Function.Injective.{u + 1, u + 1} (α := Multiset R) (β := R[X]) (⇑ofMultiset : (a : Multiset R) → R[X])

Tactic:
rightInverse_ofMultiset_roots R |>.injective

Premises used: Polynomial.rightInverse_ofMultiset_roots, Function.RightInverse.injective