awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  a ∈ (p.aroots S).toFinset ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₂ :
  a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₃ rw₄ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

Premises used: Polynomial.mem_aroots', Polynomial.rootSet_def, Finset.mem_coe, Multiset.mem_toFinset
-- 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
a : S
rw :
  a ∈ (↑(p.aroots S).toFinset : Set S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ :
  a ∈ (p.aroots S).toFinset ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₂ :
  a ∈ p.aroots S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₃ rw₄ :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔
    Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

Premises used: Polynomial.mem_aroots', Polynomial.rootSet_def, Finset.mem_coe, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
a : S
rw :
  Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
    p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
rw₁ rw₂ :
  p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S) ↔
    p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)
⊢ a ∈ p.rootSet S ↔ p ≠ 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]

Premises used: FaithfulSMul.algebraMap_injective, Polynomial.mem_rootSet', Polynomial.map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
inst_1 : IsDomain T
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : Module.IsTorsionFree T S
hp : p ≠ 0
a : S
⊢ a ∈ p.rootSet S ↔ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
mem_rootSet.trans <| and_iff_right hp

Premises used: and_iff_right, Iff.trans, Polynomial.mem_rootSet
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ (C : (a : R) → R[X]) a
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) (Set.preimage (β := R) (fun (x : R) ↦ eval x p) {a}) x ↔
      x ∈ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).rootSet R
⊢ Set.preimage (β := R) (fun (x : R) ↦ eval x p) {a} =
    (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).rootSet R

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
a : R
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p ≠ (C : (a : R) → R[X]) a
x : R
⊢ Membership.mem (γ := Set R) (Set.preimage (β := R) (fun (x : R) ↦ eval x p) {a}) x ↔
    x ∈ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).rootSet R

Tactic:
simp [mem_rootSet_of_ne (sub_ne_zero.mpr hp), sub_eq_zero]

Premises used: Iff.mpr, sub_eq_zero, sub_ne_zero, Polynomial.mem_rootSet_of_ne
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
hp : p.Monic
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ Eq.{u_1 + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
simp [Polynomial.mem_rootSet', (hp.map (algebraMap T S)).ne_zero]

Premises used: Algebra.algebraMap, Polynomial.mem_rootSet', Polynomial.Monic.map, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : CommRing S'
inst_5 : IsDomain S'
inst_6 : Algebra T S'
hp : Eq (α := S'[X]) (map (algebraMap T S') p) 0 → Eq (α := S[X]) (map (algebraMap T S) p) 0
f : S →ₐ[T] S'
x : S
hx : x ∈ p.rootSet S
rw :
  ∀ (hx : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval x : (a : T[X]) → S) p : S) (0 : S)),
    Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧
      Eq.{u_2 + 1} (α := S') (((aeval ((f : (a : S) → S') x) : T[X] →ₐ[T] S') : (a : T[X]) → S') p : S') (0 : S')
⊢ Membership.mem (α := S') (p.rootSet S') ((f : (a : S) → S') x : S')

Tactic:
rw [mem_rootSet'] at hx ⊢

Premises used: Polynomial.mem_rootSet'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : CommRing S'
inst_5 : IsDomain S'
inst_6 : Algebra T S'
hp : Eq (α := S'[X]) (map (algebraMap T S') p) 0 → Eq (α := S[X]) (map (algebraMap T S) p) 0
f : S →ₐ[T] S'
x : S
hx : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval x : (a : T[X]) → S) p : S) (0 : S)
rw : Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧ Eq.{u_2 + 1} (α := S') 0 0
⊢ Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧
    Eq.{u_2 + 1} (α := S') (((aeval ((f : (a : S) → S') x) : T[X] →ₐ[T] S') : (a : T[X]) → S') p : S') (0 : S')

Tactic:
rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]

Premises used: AlgHom.comp_apply, map_zero, And.right, Polynomial.aeval_algHom
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : CommRing S'
inst_5 : IsDomain S'
inst_6 : Algebra T S'
hp : Eq (α := S'[X]) (map (algebraMap T S') p) 0 → Eq (α := S[X]) (map (algebraMap T S) p) 0
f : S →ₐ[T] S'
x : S
hx : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval x : (a : T[X]) → S) p : S) (0 : S)
⊢ Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧ Eq.{u_2 + 1} (α := S') 0 0

Tactic:
⟨mt hp hx.1, rfl⟩

Premises used: mt, And.left, And.intro, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
inst_4 : CommRing S'
inst_5 : IsDomain S'
inst_6 : Algebra T S'
hp : Eq (α := S'[X]) (map (algebraMap T S') p) 0 → Eq (α := S[X]) (map (algebraMap T S) p) 0
f : S →ₐ[T] S'
x : S
hx : Ne (α := S[X]) (map (algebraMap T S) p) 0 ∧ Eq.{u_1 + 1} (α := S) ((aeval x : (a : T[X]) → S) p : S) (0 : S)
⊢ Ne (α := S'[X]) (map (algebraMap T S') p) 0 ∧ Eq.{u_2 + 1} (α := S') 0 0

Tactic:
exact ⟨mt hp hx.1, rfl⟩
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
p : T[X]
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
h : a ∈ p.rootSet S
hf : p = 0
rwa : ∀ (h : a ∈ rootSet.{w, v} (T := T) 0 S) (hf : p = 0), False
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : Membership.mem (γ := Set S) ∅ a) (hf : p = 0), False
⊢ False

Tactic:
rwa [hf, rootSet_zero] at h

Premises used: Polynomial.rootSet_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
S : Type v
T : Type w
inst : CommRing T
p : T[X]
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a : S
hx : a ∈ p.rootSet S
⊢ Eq.{v + 1} (α := S) ((aeval a : (a : T[X]) → S) p : S) (0 : S)

Tactic:
(mem_rootSet'.1 hx).2

Premises used: And.right, Polynomial.mem_rootSet', Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f : (a : S) → S') (p.rootSet S) (p.rootSet S')

Tactic:
rootSet_maps_to' (fun h₀ => ?_) f

Premises used: Polynomial.rootSet_maps_to'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
refine : ∀ (h₀ : Eq (α := S'[X]) (map (algebraMap T S') p) 0), Eq (α := S[X]) (map (algebraMap T S) p) 0
⊢ Set.MapsTo (⇑f : (a : S) → S') (p.rootSet S) (p.rootSet S')

Tactic:
refine rootSet_maps_to' (fun h₀ => ?_) f

Premises used: Polynomial.rootSet_maps_to'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ rwa rwa₁ rwa₂ rwa₃ : Eq (α := S'[X]) (map (algebraMap T S') p) 0
⊢ Eq (α := S'[X]) (map (algebraMap T S') p) (map (algebraMap T S') 0)

Tactic:
rwa [Polynomial.map_zero]

Premises used: Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
p : T[X]
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : Eq (α := S'[X]) (map (algebraMap T S') p) 0
obtain : ∀ (h₀ : Eq (α := S'[X]) (map (algebraMap T S') 0) 0), Eq (α := S[X]) (map (algebraMap T S) 0) 0
⊢ Eq (α := S[X]) (map (algebraMap T S) p) 0

Tactic:
obtain rfl : p = 0 :=
    map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])

Premises used: Polynomial.map_injective, FaithfulSMul.algebraMap_injective, rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : Eq (α := S'[X]) (map (algebraMap T S') 0) 0
⊢ Eq (α := S[X]) (map (algebraMap T S) 0) 0

Tactic:
Polynomial.map_zero _

Premises used: Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
T : Type w
inst : CommRing T
inst_1 : IsDomain T
S : Type u_1
S' : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : Algebra T S
inst_5 : CommRing S'
inst_6 : IsDomain S'
inst_7 : Algebra T S'
inst_8 : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : Eq (α := S'[X]) (map (algebraMap T S') 0) 0
⊢ Eq (α := S[X]) (map (algebraMap T S) 0) 0

Tactic:
exact Polynomial.map_zero _

Premises used: Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
p : S[X]
inst_3 : Algebra S R
h : Function.Injective.{v + 1, u + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ Eq.{u + 1} (α := R) ((aeval x : (a : S[X]) → R) p : R) (0 : R)

Tactic:
Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

Premises used: Set.Mem, Polynomial.rootSet, Polynomial.mem_roots_map_of_injective, Iff.trans, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
p : S[X]
inst_3 : Algebra S R
h : Function.Injective.{v + 1, u + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ Eq.{u + 1} (α := R) ((aeval x : (a : S[X]) → R) p : R) (0 : R)

Tactic:
exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

Premises used: Polynomial.mem_roots_map_of_injective, Iff.trans, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
p : S[X]
inst_3 : Algebra S R
h : Function.Injective.{v + 1, u + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ Eq.{u + 1} (α := R) ((aeval x : (a : S[X]) → R) p : R) (0 : R)

Tactic:
classical
  exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

Premises used: Polynomial.mem_roots_map_of_injective, Iff.trans, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
h : 0 < n
a : R
h₁ : ∀ (x : R), x ∈ (↑(nthRootsFinset n a) : Set R) ↔ Membership.mem (γ := Set R) {r : R | r ^ n = a} x
⊢ (↑(nthRootsFinset n a) : Set R) = {r : R | r ^ n = a}

Tactic:
ext x
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
h : 0 < n
a x : R
⊢ x ∈ (↑(nthRootsFinset n a) : Set R) ↔ Membership.mem (γ := Set R) {r : R | r ^ n = a} x

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
x : R
hx : x ∈ f.rootSet R
⊢ g • x ∈ f.rootSet R

Tactic:
simp [mem_rootSet', aeval_smul, aeval_eq_zero_of_mem_rootSet hx, (mem_rootSet'.mp hx).1]

Premises used: Polynomial.aeval_eq_zero_of_mem_rootSet, Polynomial.aeval_smul, And.left, Polynomial.mem_rootSet', Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
⊢ g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R

Tactic:
⟨?_, smul_mem_rootSet g⟩

Premises used: Polynomial.smul_mem_rootSet, Iff.intro
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
refine : g • x ∈ f.rootSet R → x ∈ f.rootSet R
⊢ g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R

Tactic:
refine ⟨?_, smul_mem_rootSet g⟩
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
obtain : ∀ (g : Gˣ), (↑g : G) • x ∈ f.rootSet R → x ∈ f.rootSet R
⊢ g • x ∈ f.rootSet R → x ∈ f.rootSet R

Tactic:
obtain ⟨g, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
x : R
g : Gˣ
⊢ (↑g : G) • x ∈ f.rootSet R → x ∈ f.rootSet R

Tactic:
fun hx ↦ inv_smul_smul g x ▸ smul_mem_rootSet _ hx

Premises used: Units.val, Polynomial.smul_mem_rootSet, Eq.rec, inv_smul_smul, Inv.inv
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
x : R
g : Gˣ
⊢ (↑g : G) • x ∈ f.rootSet R → x ∈ f.rootSet R

Tactic:
exact fun hx ↦ inv_smul_smul g x ▸ smul_mem_rootSet _ hx
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Group G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
x : R
⊢ g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R

Tactic:
smul_mem_rootSet_iff_of_isUnit (Group.isUnit g)

Premises used: Group.isUnit, Polynomial.smul_mem_rootSet_iff_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : Algebra S R
G : Type u_1
inst_4 : Monoid G
inst_5 : MulSemiringAction G R
inst_6 : SMulCommClass G S R
f : S[X]
g : G
x : (↑(f.rootSet R) : Type u)
⊢ (↑(g • x) : R) = g • (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
by_contra : ∀ (hp : ¬p = 0), False
⊢ p = 0

Tactic:
by_contra hp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ False

Tactic:
lt_irrefl #p.roots.toFinset ?_

Premises used: Multiset.toFinset, Polynomial.roots, lt_irrefl, Finset.card
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
refine : #p.roots.toFinset < #p.roots.toFinset
⊢ False

Tactic:
refine lt_irrefl #p.roots.toFinset ?_

Premises used: Multiset.toFinset, Polynomial.roots, lt_irrefl, Finset.card
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ #p.roots.toFinset ≤ p.roots.card

Tactic:
Multiset.toFinset_card_le _

Premises used: Multiset.toFinset_card_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
Polynomial.card_roots' p

Premises used: Polynomial.card_roots'
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ p.natDegree < Fintype.card ι

Tactic:
hcard
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ Fintype.card ι = Fintype.card.{u_1} (↑(Set.range f) : Type u_1)

Tactic:
(Set.card_range_of_injective hf).symm

Premises used: Set.card_range_of_injective, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
rw : #(Set.range f).toFinset = #(image f univ)
rw₁ rw₂ : #(image f univ) = #(image f univ)
⊢ Fintype.card.{u_1} (↑(Set.range f) : Type u_1) = #(image f univ)

Tactic:
rw [← Set.toFinset_card, Set.toFinset_range]

Premises used: Set.toFinset_range, Set.toFinset_card
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ #(image f univ) ≤ #p.roots.toFinset

Tactic:
Finset.card_mono ?_

Premises used: Finset.card_mono
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
_ : image f univ ≤ p.roots.toFinset
⊢ #p.roots.toFinset < #p.roots.toFinset

Tactic:
calc
    #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
    _ ≤ natDegree p := Polynomial.card_roots' p
    _ < Fintype.card ι := hcard
    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
    _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
    _ ≤ #p.roots.toFinset := Finset.card_mono ?_

Premises used: Multiset.toFinset, Polynomial.roots, Finset.univ, Multiset.toFinset_card_le, Set.Elem, Fintype.card, Set.card_range_of_injective, Polynomial.card_roots', Multiset.card, Set.range, Polynomial.natDegree, Eq.symm, Finset.image, Finset.card_mono
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x : R
simp : ∀ (x_1 : ι) (h : f x_1 = x), eval x p = 0
⊢ x ∈ image f univ → x ∈ p.roots.toFinset

Tactic:
simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]

Premises used: Finset.mem_univ, Finset.mem_image, forall_exists_index, Polynomial.IsRoot.def, ne_eq, Polynomial.mem_roots', not_false_eq_true, Multiset.mem_toFinset, true_and
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x : ι
⊢ eval (f x) p = 0

Tactic:
heval _
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
ι : Type u_2
inst_2 : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x : ι
⊢ eval (f x) p = 0

Tactic:
exact heval _