awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a : R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots.card ≤ n

Tactic:
WithBot.coe_le_coe.1 <|
    calc
      (Multiset.card (roots ((X : R[X]) ^ n - C a)) : WithBot ℕ) ≤ degree ((X : R[X]) ^ n - C a) :=
        card_roots (X_pow_sub_C_ne_zero hn a)
      _ = n := degree_X_pow_sub_C hn a

Premises used: Trans.trans, Polynomial.degree_X_pow_sub_C, WithBot.coe_le_coe, Polynomial.card_roots, Iff.mp, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
⊢ p.roots = S.val

Tactic:
(Multiset.eq_of_le_of_card_le ?_ ?_).symm

Premises used: Eq.symm, Multiset.eq_of_le_of_card_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
refine_1 : S.val ≤ p.roots
refine_2 : p.roots.card ≤ S.val.card
⊢ p.roots = S.val

Tactic:
refine (Multiset.eq_of_le_of_card_le ?_ ?_).symm

Premises used: Eq.symm, Multiset.eq_of_le_of_card_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
⊢ S.val ≤ p.roots

Tactic:
(Finset.val_le_iff_val_subset.mpr (fun x hx ↦ (p.mem_roots hp).mpr (hS x hx)))

Premises used: Iff.mpr, Polynomial.mem_roots, 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]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
⊢ S.val ≤ p.roots

Tactic:
exact (Finset.val_le_iff_val_subset.mpr (fun x hx ↦ (p.mem_roots hp).mpr (hS x hx)))

Premises used: Iff.mpr, Polynomial.mem_roots, 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]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ (↑(#S) : WithBot ℕ)
hp : p ≠ 0
⊢ p.roots.card ≤ S.val.card

Tactic:
simpa using (p.card_roots hp).trans hcard

Premises used: Polynomial.card_roots, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : (↑(#S) : WithBot ℕ) = p.degree
⊢ p.degree ≤ (↑(#S) : WithBot ℕ)

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : (↑(#S) : WithBot ℕ) = p.degree
contrapose! : ∀ (hcard : p = 0), (↑(#S) : WithBot ℕ) ≠ p.degree
⊢ p ≠ 0

Tactic:
contrapose! hcard
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p = 0
⊢ (↑(#S) : WithBot ℕ) ≠ p.degree

Tactic:
simp [hcard]
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.natDegree ≤ #S
hp : p ≠ 0
⊢ p.roots = S.val

Tactic:
roots_eq_of_degree_le_card_of_ne_zero hS (degree_le_of_natDegree_le hcard) hp

Premises used: Polynomial.degree_le_of_natDegree_le, Polynomial.roots_eq_of_degree_le_card_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : 0 < n
a x : R
rw : x ∈ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).roots ↔ x ^ n = a
rw₁ : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).IsRoot x ↔ x ^ n = a
rw₂ : eval x (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ x ^ n = a
rw₃ : eval x (HPow.hPow (α := R[X]) X n) - eval x ((C : (a : R) → R[X]) a) = 0 ↔ x ^ n = a
rw₄ : eval x (HPow.hPow (α := R[X]) X n) - a = 0 ↔ x ^ n = a
rw₅ : eval x X ^ n - a = 0 ↔ x ^ n = a
rw₆ : x ^ n - a = 0 ↔ x ^ n = a
rw₇ rw₈ : x ^ n = a ↔ x ^ n = a
⊢ x ∈ nthRoots n a ↔ x ^ n = a

Tactic:
rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]

Premises used: Polynomial.eval_C, sub_eq_zero, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot.def, Polynomial.nthRoots, Polynomial.mem_roots, Polynomial.eval_sub, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
⊢ nthRoots 0 r = 0

Tactic:
simp only [pow_zero, nthRoots, ← C_1, ← C_sub, roots_C]

Premises used: Polynomial.C_1, Polynomial.C_sub, pow_zero, Polynomial.nthRoots, Polynomial.roots_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
rw : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 0).roots = replicate n 0
rw₁ : (HPow.hPow (α := R[X]) X n - 0).roots = replicate n 0
rw₂ : (HPow.hPow (α := R[X]) X n).roots = replicate n 0
rw₃ : HSMul.hSMul (β := Multiset R) n (roots X) = replicate n 0
rw₄ : HSMul.hSMul (β := Multiset R) n {0} = replicate n 0
rw₅ rw₆ : Eq.{u_1 + 1} (α := Multiset R) (replicate n 0) (replicate n 0)
⊢ Eq.{u_1 + 1} (α := Multiset R) (nthRoots n 0) (replicate n 0)

Tactic:
rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]

Premises used: Polynomial.C, sub_zero, Polynomial.roots_pow, Polynomial.roots_X, Polynomial.nthRoots, RingHom.map_zero, Multiset.nsmul_singleton
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : n = 0
h : HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ (nthRoots n a).card ≤ n

Tactic:
simp [nthRoots, roots, h, empty_eq_zero, Multiset.card_zero]

Premises used: Polynomial.roots, Multiset.empty_eq_zero, Polynomial.nthRoots, Multiset.card_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) = 0
rw : degree.{u} (R := R) ((C : (a : R) → R[X]) (1 - a)) ≤ (↑0 : WithBot ℕ)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree ≤ (↑n : WithBot ℕ)

Tactic:
rw [hn, pow_zero, ← C_1, ← map_sub]

Premises used: Polynomial.C_1, map_sub, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) (1 - a)) ≤ (↑0 : WithBot ℕ)

Tactic:
degree_C_le

Premises used: Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) = 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) (1 - a)) ≤ (↑0 : WithBot ℕ)

Tactic:
exact degree_C_le

Premises used: Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
rw : LE.le (α := WithBot ℕ) (↑(nthRoots n a).card : WithBot ℕ) (↑n : WithBot ℕ)
⊢ (nthRoots n a).card ≤ n

Tactic:
rw [← Nat.cast_le (α := WithBot ℕ)]

Premises used: Nat.cast_le
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
rw :
  (↑(nthRoots n a).card : WithBot ℕ) ≤
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree
⊢ LE.le (α := WithBot ℕ) (↑(nthRoots n a).card : WithBot ℕ) (↑n : WithBot ℕ)

Tactic:
rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]

Premises used: Polynomial.degree_X_pow_sub_C, Nat.pos_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ (↑(nthRoots n a).card : WithBot ℕ) ≤
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree

Tactic:
card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a)

Premises used: Polynomial.nthRoots, Nat.pos_of_ne_zero, Polynomial.card_roots, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ (↑(nthRoots n a).card : WithBot ℕ) ≤
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree

Tactic:
exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a)

Premises used: Nat.pos_of_ne_zero, Polynomial.card_roots, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
⊢ (nthRoots n a).card ≤ n

Tactic:
exact
  (if hn : n = 0 then
    if h : (X : R[X]) ^ n - C a = 0 then by
      simp [nthRoots, roots, h, empty_eq_zero, Multiset.card_zero]
    else
      WithBot.coe_le_coe.1
        (le_trans (card_roots h)
          (by
            rw [hn, pow_zero, ← C_1, ← map_sub]
            exact degree_C_le))
  else by
    rw [← Nat.cast_le (α := WithBot ℕ)]
    rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
    exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))

Premises used: Polynomial.C, HSub.hSub, WithBot.coe_le_coe, dite, HPow.hPow, Polynomial.card_roots, Iff.mp, OfNat.ofNat, Polynomial.X, Eq, DFunLike.coe, le_trans
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
a : R
⊢ (nthRoots n a).card ≤ n

Tactic:
classical exact
  (if hn : n = 0 then
    if h : (X : R[X]) ^ n - C a = 0 then by
      simp [nthRoots, roots, h, empty_eq_zero, Multiset.card_zero]
    else
      WithBot.coe_le_coe.1
        (le_trans (card_roots h)
          (by
            rw [hn, pow_zero, ← C_1, ← map_sub]
            exact degree_C_le))
  else by
    rw [← Nat.cast_le (α := WithBot ℕ)]
    rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
    exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
⊢ LT.lt (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
simp_rw : nthRoots 2 r = 0 ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
simp_rw₁ : (∀ (a : R), a ∉ nthRoots 2 r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
simp_rw₂ : (∀ (a : R), ¬HPow.hPow (β := ℕ) a 2 = r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
simp_rw₃ : (¬∃ (x : R), HPow.hPow (β := ℕ) x 2 = r) ↔ ¬∃ (r_1 : R), r = HPow.hPow (β := ℕ) r_1 2
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r

Tactic:
simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_notMem, mem_nthRoots (by simp : 0 < 2),
    ← not_exists, eq_comm]

Premises used: Multiset.eq_zero_iff_forall_notMem, not_exists, eq_comm, isSquare_iff_exists_sq, Polynomial.mem_nthRoots
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
n : ℕ
R : Type u_1
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
⊢ (nthRoots n a).toFinset = (nthRoots n a).toFinset

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
n : ℕ
R : Type u_1
a : R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
⊢ (nthRoots n a).toFinset = (nthRoots n a).toFinset

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
h : 0 < n
a x : R
rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
rw₁ : x ∈ nthRoots n a ↔ x ^ n = a
rw₂ rw₃ : x ^ n = a ↔ x ^ n = a
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a

Tactic:
rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]

Premises used: Polynomial.nthRootsFinset_def, Polynomial.mem_nthRoots, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
h : 0 < n
a x : R
rw : x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
rw₁ : x ∈ nthRoots n a ↔ x ^ n = a
rw₂ rw₃ : x ^ n = a ↔ x ^ n = a
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a

Tactic:
classical
  rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]

Premises used: Polynomial.nthRootsFinset_def, Polynomial.mem_nthRoots, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
⊢ nthRootsFinset 0 a = ∅

Tactic:
simp [nthRootsFinset_def]

Premises used: Polynomial.nthRootsFinset_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
⊢ nthRootsFinset 0 a = ∅

Tactic:
classical simp [nthRootsFinset_def]

Premises used: Polynomial.nthRootsFinset_def
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
pos :
  ∀ (hn : n = 0),
    Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
      ((f : (a : R) → S) x : S)
neg :
  ∀ (hn : ¬n = 0),
    Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
      ((f : (a : R) → S) x : S)
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : n = 0
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)

Tactic:
simp [hn] at hx
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
neg : HPow.hPow (α := S) ((f : (a : R) → S) x : S) n = (f : (a : R) → S) a
neg₁ : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (x ^ n) : S) ((f : (a : R) → S) a : S)
neg₂ neg₃ : Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) a : S)
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) a) : Finset S)
    ((f : (a : R) → S) x : S)

Tactic:
rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]

Premises used: map_pow, Nat.pos_of_ne_zero, Iff.mp, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
x : R
hx : Membership.mem (γ := Finset R) (nthRootsFinset n 1) x
f : F
rw :
  Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) 1) : Finset S)
    ((f : (a : R) → S) x : S)
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n 1) ((f : (a : R) → S) x : S)

Tactic:
rw [← (map_one f)]

Premises used: map_one
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
x : R
hx : Membership.mem (γ := Finset R) (nthRootsFinset n 1) x
f : F
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) 1) : Finset S)
    ((f : (a : R) → S) x : S)

Tactic:
map_mem_nthRootsFinset hx _

Premises used: Polynomial.map_mem_nthRootsFinset, Set.Mem, setOf
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
S : Type u_1
F : Type u_2
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
x : R
hx : Membership.mem (γ := Finset R) (nthRootsFinset n 1) x
f : F
⊢ Membership.mem.{u_1, u_1} (α := S) (γ := Finset S) (nthRootsFinset n ((f : (a : R) → S) 1) : Finset S)
    ((f : (a : R) → S) x : S)

Tactic:
exact map_mem_nthRootsFinset hx _

Premises used: Polynomial.map_mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset 0 a₁
hη₂ : η₂ ∈ nthRootsFinset 0 a₂
⊢ η₁ * η₂ ∈ nthRootsFinset 0 (a₁ * a₂)

Tactic:
simp only [nthRootsFinset_zero, notMem_empty] at hη₁

Premises used: Finset.notMem_empty, Polynomial.nthRootsFinset_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ∈ nthRootsFinset (n + 1) a₁
hη₂ : η₂ ∈ nthRootsFinset (n + 1) a₂
succ : ∀ (hη₁ : η₁ ^ n.succ = a₁) (hη₂ : η₂ ^ n.succ = a₂), (η₁ * η₂) ^ n.succ = a₁ * a₂
⊢ η₁ * η₂ ∈ nthRootsFinset (n + 1) (a₁ * a₂)

Tactic:
rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢

Premises used: Nat.succ_pos, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
succ : η₁ ^ n.succ * η₂ ^ n.succ = a₁ * a₂
succ₁ : a₁ * η₂ ^ n.succ = a₁ * a₂
succ₂ succ₃ : a₁ * a₂ = a₁ * a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂

Tactic:
rw [mul_pow, hη₁, hη₂]

Premises used: mul_pow
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset n a₁
hη₂ : η₂ ∈ nthRootsFinset n a₂
zero : ∀ (hη₁ : η₁ ∈ nthRootsFinset 0 a₁) (hη₂ : η₂ ∈ nthRootsFinset 0 a₂), η₁ * η₂ ∈ nthRootsFinset 0 (a₁ * a₂)
succ :
  ∀ (n : ℕ) (hη₁ : η₁ ∈ nthRootsFinset (n + 1) a₁) (hη₂ : η₂ ∈ nthRootsFinset (n + 1) a₂),
    η₁ * η₂ ∈ nthRootsFinset (n + 1) (a₁ * a₂)
⊢ η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂)

Tactic:
cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]

Premises used: Finset.notMem_empty, Nat.succ_pos, Polynomial.nthRootsFinset_zero, mul_pow, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset 0 a
⊢ False

Tactic:
simp only [nthRootsFinset_zero, notMem_empty] at hη

Premises used: Finset.notMem_empty, Polynomial.nthRootsFinset_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
n : ℕ
hη : 0 ∈ nthRootsFinset (n + 1) a
⊢ 0 = a

Tactic:
rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη

Premises used: Nat.succ_ne_zero, Nat.succ_pos, zero_pow, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
n : ℕ
hη : 0 = a
⊢ False

Tactic:
ha hη.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
n : ℕ
hη : 0 = a
⊢ False

Tactic:
exact ha hη.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset n a
zero : ∀ (hη : 0 ∈ nthRootsFinset 0 a), False
succ : ∀ (n : ℕ) (hη : 0 ∈ nthRootsFinset (n + 1) a), False
⊢ False

Tactic:
cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
    exact ha hη.symm

Premises used: Finset.notMem_empty, Nat.succ_ne_zero, Nat.succ_pos, Polynomial.nthRootsFinset_zero, zero_pow, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
n : ℕ
inst : CommRing R
inst_1 : IsDomain R
hn : 0 < n
rw : HPow.hPow (α := R) 1 n = 1
rw₁ rw₂ : Eq.{u + 1} (α := R) 1 1
⊢ Membership.mem (γ := Finset R) (nthRootsFinset n 1) 1

Tactic:
rw [mem_nthRootsFinset hn, one_pow]

Premises used: one_pow, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)

Tactic:
simp [← sq_sub_sq]

Premises used: sq_sub_sq
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)

Tactic:
have h₁ : (X ^ 2 - C 1 : R[X]) = (X + C 1) * (X - C 1) := by simp [← sq_sub_sq]
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
h₁ :
  HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)
h : HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 = 0
⊢ False

Tactic:
simpa using congrArg (coeff · 0) h

Premises used: congrArg, Polynomial.coeff, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
h₁ :
  HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)
⊢ HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 ≠ 0

Tactic:
have h₂ : (X ^ 2 - C 1 : R[X]) ≠ 0 := fun h ↦ by simpa using congrArg (coeff · 0) h
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
h₁ :
  HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)
h₂ : HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 ≠ 0
rw : HAdd.hAdd (α := Multiset R) {-1} {1} = {-1, 1}
⊢ Eq (α := Multiset R) (nthRoots 2 1) {-1, 1}

Tactic:
rw [nthRoots, h₁, roots_mul (h₁ ▸ h₂), roots_X_add_C, roots_X_sub_C]

Premises used: Polynomial.roots_X_sub_C, Polynomial.nthRoots, Polynomial.roots_mul, Polynomial.roots_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Roots
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
h₁ :
  HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 1)
h₂ : HPow.hPow (α := R[X]) (β := ℕ) X 2 - (C : (a : R) → R[X]) 1 ≠ 0
⊢ HAdd.hAdd (α := Multiset R) {-1} {1} = {-1, 1}

Tactic:
rfl
-- 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 : ∀ (hp : ¬p = 0), False
⊢ p = 0

Tactic:
by_contra hp
-- 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
hp : ¬p = 0
⊢ False

Tactic:
@Fintype.false R _ ?_

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 : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
refine : Fintype R
⊢ False

Tactic:
refine @Fintype.false R _ ?_

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 : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ Fintype R

Tactic:
exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩