awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
by_contra by_contra₁ by_contra₂ : ∀ (hp : ¬p = 0), False
by_contra₃ : (hp : ¬p = 0) → Fintype R
⊢ p = 0

Tactic:
classical
  by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

Premises used: Fintype.false
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r 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
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
h : ∀ (x : R), eval x (p - q) = 0
⊢ p - q = 0

Tactic:
apply zero_of_eval_zero

Premises used: Polynomial.zero_of_eval_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
h : eval x p - eval x q = 0
h₁ : eval x p = eval x q
h₂ h₃ : eval x q = eval x q
⊢ eval x (p - q) = 0

Tactic:
rw [eval_sub, sub_eq_zero, ext]

Premises used: sub_eq_zero, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
⊢ p.aroots S = roots (map (algebraMap T S) p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
p : T[X]
a : S
rw :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ IsRoot (map (algebraMap T S) p) a ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval a (map (algebraMap T S) p) = 0 ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₂ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0 ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₃ rw₄ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0 ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ eval₂ (algebraMap T S) a p = 0
⊢ a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]

Premises used: Polynomial.IsRoot.def, Polynomial.aeval_def, Polynomial.mem_roots', Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
p : T[X]
a : S
rw : Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)
⊢ a ∈ p.aroots S ↔ p ≠ 0 ∧ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
rw [mem_aroots', Polynomial.map_ne_zero_iff]

Premises used: Polynomial.mem_aroots', Polynomial.map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
p : T[X]
a : S
⊢ Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)

Tactic:
FaithfulSMul.algebraMap_injective T S

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
p : T[X]
a : S
⊢ Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)

Tactic:
exact FaithfulSMul.algebraMap_injective T S

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
this : HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
rw : roots (map (algebraMap T S) (p * q)) = p.aroots S + q.aroots S
rw₁ : (HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q)).roots = p.aroots S + q.aroots S
rw₂ rw₃ : roots (map (algebraMap T S) p) + roots (map (algebraMap T S) q) = p.aroots S + q.aroots S
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
rw [aroots_def, Polynomial.map_mul, roots_mul this]

Premises used: Polynomial.map_mul, Polynomial.roots_mul, Polynomial.aroots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
suffices : HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
suffices map (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by
    rw [aroots_def, Polynomial.map_mul, roots_mul this]
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
rwa : Ne (α := S[X]) (map (algebraMap T S) (p * q)) 0
rwa₁ rwa₂ rwa₃ rwa₄ : p * q ≠ 0
⊢ HMul.hMul (α := S[X]) (map (algebraMap T S) p) (map (algebraMap T S) q) ≠ 0

Tactic:
rwa [← Polynomial.map_mul, Polynomial.map_ne_zero_iff
    (FaithfulSMul.algebraMap_injective T S)]

Premises used: Polynomial.map_mul, FaithfulSMul.algebraMap_injective, Polynomial.map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
r : T
rw :
  roots (map (algebraMap T S) (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X]))) =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₁ :
  (HSub.hSub (α := S[X]) (map (algebraMap T S : T →+* S) X)
        (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₂ :
  (HSub.hSub (α := S[X]) X (map (algebraMap T S : T →+* S) ((C : (a : T) → T[X]) r))).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₃ :
  (HSub.hSub (α := S[X]) (β := S[X]) X
        ((C : (a : S) → S[X]) (((algebraMap T S : T →+* S) : (a : T) → S) r) : S[X])).roots =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)
rw₄ rw₅ :
  Eq (α := Multiset S) (singleton (α := S) (((algebraMap T S : T →+* S) : (a : T) → S) r : S))
    (singleton (α := S) ((algebraMap T S : (a : T) → S) r : S))
⊢ (HSub.hSub (α := T[X]) (β := T[X]) X ((C : (a : T) → T[X]) r : T[X])).aroots S =
    singleton (α := S) ((algebraMap T S : (a : T) → S) r : S)

Tactic:
rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]

Premises used: Polynomial.map_X, Polynomial.roots_X_sub_C, Polynomial.map_sub, Polynomial.map_C, Polynomial.aroots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : roots (map (algebraMap T S) X) = {0}
rw₁ : Eq (α := Multiset S) (roots X) {0}
rw₂ rw₃ : Eq (α := Multiset S) {0} {0}
⊢ aroots.{w, v} (T := T) X S = {0}

Tactic:
rw [aroots_def, map_X, roots_X]

Premises used: Polynomial.map_X, Polynomial.roots_X, Polynomial.aroots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : roots (map (algebraMap T S) ((C : (a : T) → T[X]) a)) = 0
rw₁ : Eq.{v + 1} (α := Multiset S) (roots ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a))) 0
rw₂ rw₃ : Eq.{v + 1} (α := Multiset S) 0 0
⊢ aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = 0

Tactic:
rw [aroots_def, map_C, roots_C]

Premises used: Polynomial.map_C, Polynomial.aroots_def, Polynomial.roots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : aroots.{w, u_1} (T := T) ((C : (a : T) → T[X]) 0) S = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Multiset S) 0 0
⊢ aroots.{w, u_1} (T := T) 0 S = 0

Tactic:
rw [← C_0, aroots_C]

Premises used: Polynomial.C_0, Polynomial.aroots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
⊢ aroots.{w, v} (T := T) 1 S = 0

Tactic:
aroots_C 1

Premises used: OfNat.ofNat, Polynomial.aroots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
p : T[X]
rw : roots (map (algebraMap T S) (-p)) = p.aroots S
rw₁ : roots (-map (algebraMap T S) p) = p.aroots S
rw₂ rw₃ : roots (map (algebraMap T S) p) = p.aroots S
⊢ (-p).aroots S = p.aroots S

Tactic:
rw [aroots, Polynomial.map_neg, roots_neg]

Premises used: Polynomial.aroots, Polynomial.roots_neg, Polynomial.map_neg
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
ha₁ : Ne.{v + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) p).aroots S = p.aroots S

Tactic:
rw [aroots_def, Polynomial.map_mul, map_C, roots_C_mul]

Premises used: Polynomial.map_mul, Polynomial.roots_C_mul, Polynomial.map_C, Polynomial.aroots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
ha₁ : Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)
⊢ Ne.{v + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)

Tactic:
rwa [map_ne_zero_iff]

Premises used: map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)

Tactic:
FaithfulSMul.algebraMap_injective T S

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ Function.Injective.{w + 1, v + 1} (α := T) (β := S) (⇑(algebraMap T S) : (a : T) → S)

Tactic:
exact FaithfulSMul.algebraMap_injective T S

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
rw : (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) p).aroots S = p.aroots S
rw₁ rw₂ : p.aroots S = p.aroots S
⊢ (a • p).aroots S = p.aroots S

Tactic:
rw [smul_eq_C_mul, aroots_C_mul _ ha]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.aroots_C_mul
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
p : T[X]
n : ℕ
rw : roots (map (algebraMap T S) (p ^ n)) = n • p.aroots S
rw₁ : (HPow.hPow (α := S[X]) (map (algebraMap T S) p) n).roots = n • p.aroots S
rw₂ rw₃ : n • roots (map (algebraMap T S) p) = n • p.aroots S
⊢ (p ^ n).aroots S = n • p.aroots S

Tactic:
rw [aroots_def, Polynomial.map_pow, roots_pow]

Premises used: Polynomial.roots_pow, Polynomial.map_pow, Polynomial.aroots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
n : ℕ
rw : n • aroots.{w, v} (T := T) X S = HSMul.hSMul (β := Multiset S) n {0}
rw₁ rw₂ : HSMul.hSMul (β := Multiset S) n {0} = HSMul.hSMul (β := Multiset S) n {0}
⊢ (HPow.hPow (α := T[X]) X n).aroots S = HSMul.hSMul (β := Multiset S) n {0}

Tactic:
rw [aroots_pow, aroots_X]

Premises used: Polynomial.aroots_X, Polynomial.aroots_pow
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
rw : (HPow.hPow (α := T[X]) X n).aroots S = HSMul.hSMul (β := Multiset S) n {0}
rw₁ rw₂ : HSMul.hSMul (β := Multiset S) n {0} = HSMul.hSMul (β := Multiset S) n {0}
⊢ (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) X n)).aroots S =
    HSMul.hSMul (β := Multiset S) n {0}

Tactic:
rw [aroots_C_mul _ ha, aroots_X_pow]

Premises used: Polynomial.aroots_C_mul, Polynomial.aroots_X_pow
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
rw :
  (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) X n)).aroots S =
    HSMul.hSMul (β := Multiset S) n {0}
rw₁ rw₂ : HSMul.hSMul (β := Multiset S) n {0} = HSMul.hSMul (β := Multiset S) n {0}
⊢ aroots.{w, v} (T := T) ((monomial n : (a : T) → T[X]) a) S = HSMul.hSMul (β := Multiset S) n {0}

Tactic:
rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.aroots_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing T
p : T[X]
inst_3 : CommRing S
inst_4 : Algebra T S
inst_5 : Algebra S R
inst_6 : Algebra T R
inst_7 : IsScalarTower T S R
rw : roots (map (algebraMap S R) (map (algebraMap T S) p)) = p.aroots R
rw₁ : roots (map (algebraMap S R) (map (algebraMap T S) p)) = roots (map (algebraMap T R) p)
rw₂ :
  roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p) =
    roots (map (algebraMap T R) p)
rw₃ rw₄ :
  roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p) =
    roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S R) (algebraMap T S)) p)
⊢ aroots (map (algebraMap T S) p) R = p.aroots R

Tactic:
rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map, Polynomial.aroots_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : DecidableEq S
⊢ (↑(p.aroots S).toFinset : Set S) = (↑(p.aroots S).toFinset : Set S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : DecidableEq S
⊢ (↑(p.aroots S).toFinset : Set S) = (↑(p.aroots S).toFinset : Set S)

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
rw₁ : (↑(toFinset 0) : Set S) = ∅
rw₂ : (↑∅ : Set S) = ∅
rw₃ rw₄ : Eq.{v + 1} (α := Set S) ∅ ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅

Tactic:
rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

Premises used: Finset.coe_empty, Polynomial.rootSet_def, Multiset.toFinset_zero, Polynomial.aroots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : T
rw : (↑(aroots.{w, v} (T := T) ((C : (a : T) → T[X]) a) S).toFinset : Set S) = ∅
rw₁ : (↑(toFinset 0) : Set S) = ∅
rw₂ : (↑∅ : Set S) = ∅
rw₃ rw₄ : Eq.{v + 1} (α := Set S) ∅ ∅
⊢ rootSet.{w, v} (T := T) ((C : (a : T) → T[X]) a) S = ∅

Tactic:
classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

Premises used: Finset.coe_empty, Polynomial.rootSet_def, Multiset.toFinset_zero, Polynomial.aroots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : rootSet.{w, u_1} (T := T) ((C : (a : T) → T[X]) 0) S = ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set S) ∅ ∅
⊢ rootSet.{w, u_1} (T := T) 0 S = ∅

Tactic:
rw [← C_0, rootSet_C]

Premises used: Polynomial.C_0, Polynomial.rootSet_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : rootSet.{w, u_1} (T := T) ((C : (a : T) → T[X]) 1) S = ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set S) ∅ ∅
⊢ rootSet.{w, u_1} (T := T) 1 S = ∅

Tactic:
rw [← C_1, rootSet_C]

Premises used: Polynomial.C_1, Polynomial.rootSet_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
rw : (↑((-p).aroots S).toFinset : Set S) = p.rootSet S
rw₁ : (↑(p.aroots S).toFinset : Set S) = p.rootSet S
rw₂ rw₃ : (↑(p.aroots S).toFinset : Set S) = (↑(p.aroots S).toFinset : Set S)
⊢ (-p).rootSet S = p.rootSet S

Tactic:
rw [rootSet, aroots_neg, rootSet]

Premises used: Polynomial.rootSet, Polynomial.aroots_neg
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
⊢ (p.rootSet S).Finite

Tactic:
Set.toFinite _

Premises used: Set.toFinite
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
⊢ Set.Finite.{u_1} (α := R[X]) fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)

Premises used: Set.Finite.subset, Set.Finite.of_finite_image, Set.Finite.pi
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
refine_1 :
  (π '' fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆
    Set.pi (α := fun (i : Fin (d + 1)) ↦ R) Set.univ fun (x : Fin (d + 1)) ↦ U
refine_2 : Set.InjOn π fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
⊢ Set.Finite.{u_1} (α := R[X]) fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)

Premises used: Set.Finite.subset, Set.Finite.of_finite_image, Set.Finite.pi
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
⊢ (π '' fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆
    Set.pi (α := fun (i : Fin (d + 1)) ↦ R) Set.univ fun (x : Fin (d + 1)) ↦ U

Tactic:
Set.image_subset_iff.2 fun f hf i _ => hf.2 i

Premises used: Iff.mpr, Fin.val, And.right, Set.image_subset_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
⊢ (π '' fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆
    Set.pi (α := fun (i : Fin (d + 1)) ↦ R) Set.univ fun (x : Fin (d + 1)) ↦ U

Tactic:
exact Set.image_subset_iff.2 fun f hf i _ => hf.2 i
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
⊢ Set.InjOn π fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_

Premises used: Iff.mpr, Polynomial.ext_iff_natDegree_le, And.left, Set.InjOn
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
refine_2 :
  ∀ (x : R[X]) (hx : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) x)
    (y : R[X]) (hy : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) y)
    (hxy : π x = π y) (i : ℕ) (hi : i ≤ d), x.coeff i = y.coeff i
⊢ Set.InjOn π fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_

Premises used: Iff.mpr, Polynomial.ext_iff_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
x : R[X]
hx : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) x
y : R[X]
hy : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) y
hxy : π x = π y
i : ℕ
hi : i ≤ d
⊢ x.coeff i = y.coeff i

Tactic:
id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩

Premises used: Fin.mk, id, Nat.lt_succ_of_le, congr_fun
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun (f : R[X]) (i : Fin (d + 1)) ↦ f.coeff (↑i : ℕ)
x : R[X]
hx : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) x
y : R[X]
hy : Membership.mem (γ := Set R[X]) (fun (f : R[X]) ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) y
hxy : π x = π y
i : ℕ
hi : i ≤ d
⊢ x.coeff i = y.coeff i

Tactic:
exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩

Premises used: Fin.mk, id, Nat.lt_succ_of_le, congr_fun