awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
zero : (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).reverse = p.reverse
succ :
  ∀ (n : ℕ) (ih : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse),
    (p * HPow.hPow (α := R[X]) X (n + 1)).reverse = p.reverse
⊢ (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

Premises used: pow_succ, mul_assoc, Polynomial.reverse_mul_X
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw : (p * HPow.hPow (α := R[X]) X n).reverse = p.reverse
rw₁ rw₂ : p.reverse = p.reverse
⊢ (HPow.hPow (α := R[X]) X n * p).reverse = p.reverse

Tactic:
rw [commute_X_pow p, reverse_mul_X_pow]

Premises used: Polynomial.reverse_mul_X_pow, Polynomial.commute_X_pow
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
t : R
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) t : R[X])).reverse =
    p.reverse + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree)

Tactic:
simp [reverse]

Premises used: Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
t : R
rw :
  (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) t : R[X])).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
rw₁ :
  p.reverse + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
rw₂ rw₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse
⊢ (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) p).reverse =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.reverse

Tactic:
rw [add_comm, reverse_add_C, add_comm]

Premises used: add_comm, Polynomial.reverse_add_C
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
f : R[X]
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) f.reverse * x ^ f.natDegree = eval₂ i x f

Tactic:
eval₂_reflect_mul_pow i _ _ f le_rfl

Premises used: le_rfl, Polynomial.eval₂_reflect_mul_pow, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
f : R[X]
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) f.reverse = 0 ↔ eval₂ i x f = 0

Tactic:
eval₂_reflect_eq_zero_iff i x _ _ le_rfl

Premises used: le_rfl, Polynomial.eval₂_reflect_eq_zero_iff, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Ring R
f : R[X]
N : ℕ
rw : reflect N (-1 * f) = -reflect N f
rw₁ : reflect N (-(C : (a : R) → R[X]) 1 * f) = -reflect N f
rw₂ : reflect N ((C : (a : R) → R[X]) (-1) * f) = -reflect N f
rw₃ : (C : (a : R) → R[X]) (-1) * reflect N f = -reflect N f
rw₄ : -(C : (a : R) → R[X]) 1 * reflect N f = -reflect N f
rw₅ : -1 * reflect N f = -reflect N f
rw₆ rw₇ : -reflect N f = -reflect N f
⊢ reflect N (-f) = -reflect N f

Tactic:
rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]

Premises used: Polynomial.C_1, neg_eq_neg_one_mul, Polynomial.reflect_C_mul, Polynomial.C_neg
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Ring R
f g : R[X]
N : ℕ
rw : reflect N (f + -g) = reflect N f - reflect N g
rw₁ : reflect N (f + -g) = reflect N f + -reflect N g
rw₂ : reflect N f + reflect N (-g) = reflect N f + -reflect N g
rw₃ rw₄ : reflect N f + -reflect N g = reflect N f + -reflect N g
⊢ reflect N (f - g) = reflect N f - reflect N g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]

Premises used: sub_eq_add_neg, Polynomial.reflect_add, Polynomial.reflect_neg
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Ring R
f : R[X]
rw : reflect (-f).natDegree (-f) = -f.reverse
rw₁ : reflect (-f).natDegree (-f) = -reflect f.natDegree f
rw₂ : -reflect (-f).natDegree f = -reflect f.natDegree f
rw₃ rw₄ : -reflect f.natDegree f = -reflect f.natDegree f
⊢ (-f).reverse = -f.reverse

Tactic:
rw [reverse, reverse, reflect_neg, natDegree_neg]

Premises used: Polynomial.reflect_neg, Polynomial.natDegree_neg, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
iR : DecidableEq R
p : R[X]
ip0 : Decidable (p = 0)
obtain :
  p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯
⊢ p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯

Tactic:
obtain rfl := Subsingleton.elim iR (Classical.decEq R)

Premises used: Subsingleton.elim, Classical.decEq, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ip0 : Decidable (p = 0)
obtain :
  p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯
⊢ p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯

Tactic:
obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))

Premises used: Classical.dec, Subsingleton.elim, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
⊢ p.roots =
    if h : p = 0 then ∅
    else
      Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq.{u + 1} (α := Multiset R) (roots 0) 0

Tactic:
dif_pos rfl

Premises used: Polynomial.roots, dif_pos, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
rw :
  (↑(Classical.choose (p := fun (x : Multiset R) ↦
            (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯).card :
      WithBot ℕ) ≤
    p.degree
⊢ (↑(Multiset.card.{u} (α := R)
          (if h : p = 0 then ∅
          else
            Classical.choose (p := fun (x : Multiset R) ↦
              (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯)) :
      WithBot ℕ) ≤
    p.degree

Tactic:
rw [dif_neg hp0]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ (↑(Classical.choose (p := fun (x : Multiset R) ↦
            (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯).card :
      WithBot ℕ) ≤
    p.degree

Tactic:
(Classical.choose_spec (exists_multiset_roots hp0)).1

Premises used: Polynomial.exists_multiset_roots, Classical.choose_spec, And.left
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ (↑(Classical.choose (p := fun (x : Multiset R) ↦
            (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯).card :
      WithBot ℕ) ≤
    p.degree

Tactic:
exact (Classical.choose_spec (exists_multiset_roots hp0)).1

Premises used: Polynomial.exists_multiset_roots, Classical.choose_spec, And.left
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
unfold :
  (↑(Multiset.card.{u} (α := R)
          (if h : p = 0 then ∅
          else
            Classical.choose (p := fun (x : Multiset R) ↦
              (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯)) :
      WithBot ℕ) ≤
    p.degree
unfold₁ :
  (↑(Classical.choose (p := fun (x : Multiset R) ↦
            (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯).card :
      WithBot ℕ) ≤
    p.degree
⊢ (↑p.roots.card : WithBot ℕ) ≤ p.degree

Tactic:
classical
  unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1

Premises used: Polynomial.roots, dif_neg
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
pos : ∀ (hp0 : p = 0), p.roots.card ≤ p.natDegree
neg : ∀ (hp0 : ¬p = 0), p.roots.card ≤ p.natDegree
⊢ p.roots.card ≤ p.natDegree

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
simp [hp0]
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

Premises used: Polynomial.degree_eq_natDegree, WithBot.coe_le_coe, Polynomial.card_roots, Iff.mp, le_of_eq, le_trans
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

Premises used: Polynomial.degree_eq_natDegree, WithBot.coe_le_coe, Polynomial.card_roots, Iff.mp, le_of_eq, le_trans
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
rw : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree

Tactic:
rw [sub_eq_add_neg, ← C_neg]

Premises used: sub_eq_add_neg, Polynomial.C_neg
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree

Tactic:
degree_add_C hp0

Premises used: Polynomial.degree_add_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree

Tactic:
exact degree_add_C hp0

Premises used: Polynomial.degree_add_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
h : p = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
pos : ∀ (hp : p = 0), count a p.roots = rootMultiplicity a p
neg : ∀ (hp : ¬p = 0), count a p.roots = rootMultiplicity a p
⊢ count a p.roots = rootMultiplicity a p

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p = 0
⊢ count a p.roots = rootMultiplicity a p

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : ¬p = 0
neg :
  count a
      (Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯) =
    rootMultiplicity a p
⊢ count a p.roots = rootMultiplicity a p

Tactic:
rw [roots_def, dif_neg hp]

Premises used: dif_neg, Polynomial.roots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a
      (Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯) =
    rootMultiplicity a p

Tactic:
(Classical.choose_spec (exists_multiset_roots hp)).2 a

Premises used: Polynomial.exists_multiset_roots, Classical.choose_spec, And.right
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a
      (Classical.choose (p := fun (x : Multiset R) ↦
        (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯) =
    rootMultiplicity a p

Tactic:
exact (Classical.choose_spec (exists_multiset_roots hp)).2 a

Premises used: Polynomial.exists_multiset_roots, Classical.choose_spec, And.right
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
pos : ∀ (hp : p = 0), count a p.roots = rootMultiplicity a p
neg neg₁ : ∀ (hp : ¬p = 0), count a p.roots = rootMultiplicity a p
neg₂ :
  ∀ (hp : ¬p = 0),
    count a
        (Classical.choose (p := fun (x : Multiset R) ↦
          (↑x.card : WithBot ℕ) ≤ p.degree ∧ ∀ (a : R), count a x = rootMultiplicity a p) ⋯) =
      rootMultiplicity a p
⊢ count a p.roots = rootMultiplicity a p

Tactic:
classical
  by_cases hp : p = 0
  · simp [hp]
  rw [roots_def, dif_neg hp]
  exact (Classical.choose_spec (exists_multiset_roots hp)).2 a

Premises used: Polynomial.roots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw : 0 < count a p.roots ↔ p ≠ 0 ∧ p.IsRoot a
rw₁ : 0 < rootMultiplicity a p ↔ p ≠ 0 ∧ p.IsRoot a
rw₂ rw₃ : p ≠ 0 ∧ p.IsRoot a ↔ p ≠ 0 ∧ p.IsRoot a
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
rw [← count_pos, count_roots p, rootMultiplicity_pos']

Premises used: Polynomial.count_roots, Multiset.count_pos, Polynomial.rootMultiplicity_pos'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
rw : 0 < count a p.roots ↔ p ≠ 0 ∧ p.IsRoot a
rw₁ : 0 < rootMultiplicity a p ↔ p ≠ 0 ∧ p.IsRoot a
rw₂ rw₃ : p ≠ 0 ∧ p.IsRoot a ↔ p ≠ 0 ∧ p.IsRoot a
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
classical
  rw [← count_pos, count_roots p, rootMultiplicity_pos']

Premises used: Multiset.count_pos, Polynomial.rootMultiplicity_pos'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ 0
⊢ a ∈ p.roots ↔ p.IsRoot a

Tactic:
mem_roots'.trans <| and_iff_right hp

Premises used: and_iff_right, Polynomial.mem_roots', Iff.trans
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
h : a ∈ p.roots
⊢ p ≠ 0

Tactic:
(mem_roots'.1 h).1

Premises used: And.left, Polynomial.mem_roots', Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
h : a ∈ p.roots
⊢ p.IsRoot a

Tactic:
(mem_roots'.1 h).2

Premises used: And.right, Polynomial.mem_roots', Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p.IsRoot = ⊥

Tactic:
⟨fun h ↦ ?_, fun h ↦ eq_zero_of_forall_notMem fun x hx ↦ h ▸ mem_roots hp0 |>.mp hx⟩

Premises used: Iff.intro, Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
refine : ∀ (h : p.roots = 0), p.IsRoot = ⊥
⊢ p.roots = 0 ↔ p.IsRoot = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ eq_zero_of_forall_notMem fun x hx ↦ h ▸ mem_roots hp0 |>.mp hx⟩
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
h₁ : ∀ (a : R), p.IsRoot a ↔ ⊥ a
⊢ p.IsRoot = ⊥

Tactic:
ext a
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ ?m.50 ∉ p.roots

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ p.IsRoot a ↔ ⊥ a

Tactic:
simp only [Pi.bot_apply, Prop.bot_eq_false, mem_roots hp0 |>.not.mp <| by simp [h]]

Premises used: Prop.bot_eq_false, Iff.not, Pi.bot_apply, Polynomial.mem_roots, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
inl :
  Eq.{u + 1} (α := Multiset R) (roots 0) 0 ↔ Eq.{u + 1} (α := R[X]) 0 0 ∨ Eq.{u + 1} (α := (a : R) → Prop) (IsRoot 0) ⊥
inr : ∀ (hp0 : p ≠ 0), p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
rcases eq_or_ne p 0 with rfl | hp0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq.{u + 1} (α := Multiset R) (roots 0) 0 ↔ Eq.{u + 1} (α := R[X]) 0 0 ∨ Eq.{u + 1} (α := (a : R) → Prop) (IsRoot 0) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
simp [roots_eq_zero_iff_isRoot_eq_bot hp0, hp0]

Premises used: Polynomial.roots_eq_zero_iff_isRoot_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Semiring S
p : S[X]
f : S →+* R
hf : Function.Injective.{v + 1, u + 1} (α := S) (β := R) (⇑f : (a : S) → R)
x : R
hp : p ≠ 0
rw : (map f p).IsRoot x ↔ eval₂ f x p = 0
rw₁ : eval x (map f p) = 0 ↔ eval₂ f x p = 0
rw₂ rw₃ : eval₂ f x p = 0 ↔ eval₂ f x p = 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0

Tactic:
rw [mem_roots ((Polynomial.map_ne_zero_iff hf).mpr hp), IsRoot, eval_map]

Premises used: Iff.mpr, Polynomial.eval_map, Polynomial.IsRoot, Polynomial.mem_roots, Polynomial.map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
x : R
w : p ≠ 0
rw : x ∈ p.roots ↔ eval₂ (algebraMap R R) x p = 0
rw₁ : x ∈ p.roots ↔ x ∈ roots (map (algebraMap R R) p)
rw₂ : x ∈ p.roots ↔ x ∈ (map (RingHom.id R) p).roots
rw₃ rw₄ : x ∈ p.roots ↔ x ∈ p.roots
⊢ x ∈ p.roots ↔ Eq (α := R) ((aeval x : (a : R[X]) → R) p : R) (0 : R)

Tactic:
rw [aeval_def, ← mem_roots_map_of_injective (FaithfulSMul.algebraMap_injective _ _) w,
    Algebra.algebraMap_self, map_id]

Premises used: Algebra.algebraMap_self, Polynomial.mem_roots_map_of_injective, Polynomial.map_id, Polynomial.aeval_def, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
Z : Finset R
h : Z.val ⊆ p.roots
⊢ #Z ≤ p.natDegree

Tactic:
(Multiset.card_le_card (Finset.val_le_iff_val_subset.2 h)).trans (Polynomial.card_roots' p)

Premises used: Iff.mpr, Multiset.card_le_card, Polynomial.card_roots', Finset.card, LE.le.trans, Finset.val_le_iff_val_subset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ 0
⊢ Set.Finite.{u} (α := R) {x : R | p.IsRoot x}

Tactic:
simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp]
    using p.roots.toFinset.finite_toSet

Premises used: Multiset.toFinset, Polynomial.roots, Finset.setOf_mem, Polynomial.mem_roots, Finset.finite_toSet, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ 0
⊢ Set.Finite.{u} (α := R) {x : R | p.IsRoot x}

Tactic:
classical
  simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp]
    using p.roots.toFinset.finite_toSet

Premises used: Finset.setOf_mem, Polynomial.mem_roots, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
h : Set.Infinite.{u} (α := R) {x : R | p.IsRoot x}
⊢ p = 0

Tactic:
not_imp_comm.mp finite_setOf_isRoot h

Premises used: not_imp_comm, Iff.mp, Polynomial.finite_setOf_isRoot
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : LinearOrder R
p : R[X]
hp : p ≠ 0
⊢ ∃ (x₀ : R), ∀ (x : R), p.IsRoot x → x ≤ x₀

Tactic:
Set.exists_upper_bound_image _ _ <| finite_setOf_isRoot hp

Premises used: Set.Mem, Polynomial.IsRoot, Set.exists_upper_bound_image, Polynomial.finite_setOf_isRoot
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : LinearOrder R
p : R[X]
hp : p ≠ 0
⊢ ∃ (x₀ : R), ∀ (x : R), p.IsRoot x → x₀ ≤ x

Tactic:
Set.exists_lower_bound_image _ _ <| finite_setOf_isRoot hp

Premises used: Set.Mem, Polynomial.IsRoot, Set.exists_lower_bound_image, Polynomial.finite_setOf_isRoot
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Set.Infinite.{u} (α := R) {x : R | eval x p = eval x q}
rw : p - q = 0
⊢ p = q

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Set.Infinite.{u} (α := R) {x : R | eval x p = eval x q}
h₁ : Set.Infinite.{u} (α := R) {x : R | (p - q).IsRoot x}
⊢ p - q = 0

Tactic:
apply eq_zero_of_infinite_isRoot

Premises used: Polynomial.eq_zero_of_infinite_isRoot
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Set.Infinite.{u} (α := R) {x : R | eval x p = eval x q}
⊢ Set.Infinite.{u} (α := R) {x : R | (p - q).IsRoot x}

Tactic:
simpa only [IsRoot, eval_sub, sub_eq_zero]

Premises used: sub_eq_zero, Polynomial.IsRoot, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
r : R
rw : count r (p * q).roots = count r p.roots + count r q.roots
rw₁ : rootMultiplicity r (p * q) = count r p.roots + count r q.roots
rw₂ : rootMultiplicity r (p * q) = rootMultiplicity r p + count r q.roots
rw₃ : rootMultiplicity r (p * q) = rootMultiplicity r p + rootMultiplicity r q
rw₄ rw₅ : rootMultiplicity r p + rootMultiplicity r q = rootMultiplicity r p + rootMultiplicity r q
⊢ count r (p * q).roots = count r (p.roots + q.roots)

Tactic:
rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Premises used: Polynomial.rootMultiplicity_mul, Polynomial.count_roots, Multiset.count_add
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
⊢ (p * q).roots = p.roots + q.roots

Tactic:
exact Multiset.ext.mpr fun r => by
    rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Premises used: Iff.mpr, Multiset.ext
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
⊢ (p * q).roots = p.roots + q.roots

Tactic:
classical
  exact Multiset.ext.mpr fun r => by
    rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Premises used: Iff.mpr, Multiset.ext
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ p.roots ≤ (p * k).roots

Tactic:
Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩

Premises used: Iff.mpr, Polynomial.roots, Polynomial.roots_mul, Exists.intro, Multiset.le_iff_exists_add
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ p.roots ≤ (p * k).roots

Tactic:
exact Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩

Premises used: Iff.mpr, Polynomial.roots, Polynomial.roots_mul, Exists.intro, Multiset.le_iff_exists_add