awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
f : k[X]
hf : f.Monic
h : Irreducible f
⊢ Splits.{u} (R := AlgebraicClosure k)
    (∏ i : Fin (↑⟨f, hf⟩ : k[X]).natDegree,
      map (Ideal.Quotient.mk (maxIdeal k))
        (HSub.hSub (α := (MvPolynomial (Vars k) k)[X]) (β := (MvPolynomial (Vars k) k)[X]) X
          ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
              (MvPolynomial.X
                (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                  (Subtype.mk (p := fun (f : k[X]) ↦ f.Monic) f hf) i)) :
            (MvPolynomial (Vars k) k)[X])))

Tactic:
Splits.prod fun _ _ ↦ (Splits.X_sub_C _).map _

Premises used: Ideal.Quotient.mk, MvPolynomial.X, Subtype.mk, Polynomial.Splits.X_sub_C, AlgebraicClosure.maxIdeal, Sigma.mk, Polynomial.Splits.map, AlgebraicClosure, Polynomial.Splits.prod
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
f : k[X]
hf : f.Monic
h : Irreducible f
⊢ Splits.{u} (R := AlgebraicClosure k)
    (∏ i : Fin (↑⟨f, hf⟩ : k[X]).natDegree,
      map (Ideal.Quotient.mk (maxIdeal k))
        (HSub.hSub (α := (MvPolynomial (Vars k) k)[X]) (β := (MvPolynomial (Vars k) k)[X]) X
          ((C : (a : MvPolynomial (Vars k) k) → (MvPolynomial (Vars k) k)[X])
              (MvPolynomial.X
                (Sigma.mk (β := fun (f : Monics k) ↦ Fin (↑f : k[X]).natDegree)
                  (Subtype.mk (p := fun (f : k[X]) ↦ f.Monic) f hf) i)) :
            (MvPolynomial (Vars k) k)[X])))

Tactic:
exact Splits.prod fun _ _ ↦ (Splits.X_sub_C _).map _

Premises used: Polynomial.Splits.X_sub_C, Polynomial.Splits.map, Polynomial.Splits.prod
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
⊢ IsAlgClosed.{u} (AlgebraicClosure k)

Tactic:
IsAlgClosure.isAlgClosed k

Premises used: IsAlgClosure.isAlgClosed
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
inst_1 : CharZero k
⊢ CharZero.{u} (AlgebraicClosure k)

Tactic:
charZero_of_injective_algebraMap (RingHom.injective (algebraMap k (AlgebraicClosure k)))

Premises used: Algebra.algebraMap, RingHom.injective, AlgebraicClosure, charZero_of_injective_algebraMap
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
p : ℕ
inst_1 : CharP k p
⊢ CharP.{u} (AlgebraicClosure k) p

Tactic:
charP_of_injective_algebraMap (RingHom.injective (algebraMap k (AlgebraicClosure k))) p

Premises used: Algebra.algebraMap, charP_of_injective_algebraMap, RingHom.injective, AlgebraicClosure
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
K : Type u_1
L : Type u_2
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
E : IntermediateField K L
inst_4 : Algebra.IsAlgebraic.{u_1, u_2} K ↥E
⊢ IsAlgClosure.{u_1, u_2} K (AlgebraicClosure ↥E)

Tactic:
⟨AlgebraicClosure.isAlgClosed E, Algebra.IsAlgebraic.trans K E (AlgebraicClosure E)⟩

Premises used: IsAlgClosure.mk, Membership.mem, Algebra.IsAlgebraic.trans, Subtype, AlgebraicClosure.isAlgClosed, AlgebraicClosure
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ Normal.{u_1, u_2} K (AlgebraicClosure ↥K⟮x⟯)

Tactic:
have : Algebra.IsAlgebraic K K⟮x⟯ := isAlgebraic_adjoin_simple hx
  IsAlgClosure.normal _ _

Premises used: Membership.mem, Subtype, IntermediateField.isAlgebraic_adjoin_simple, IntermediateField.adjoin, IsAlgClosure.normal, Singleton.singleton, AlgebraicClosure
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
⊢ Normal.{u_1, u_2} K (AlgebraicClosure ↥K⟮x, y⟯)

Tactic:
have : Algebra.IsAlgebraic K K⟮x, y⟯ := isAlgebraic_adjoin_pair hx hy
  IsAlgClosure.normal _ _

Premises used: Membership.mem, Subtype, Insert.insert, IntermediateField.isAlgebraic_adjoin_pair, IntermediateField.adjoin, IsAlgClosure.normal, Singleton.singleton, AlgebraicClosure
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : IsAlgClosed k
inst_2 : CommRing K
f : K →+* k
p : K[X]
⊢ (map f p).Splits

Tactic:
IsAlgClosed.splits (p.map f)

Premises used: IsAlgClosed.splits, Polynomial.map
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : IsAlgClosed k
inst_2 : Field K
f : k →+* K
p : k[X]
⊢ (map f p).Splits

Tactic:
(IsAlgClosed.splits p).map f

Premises used: IsAlgClosed.splits, Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
hp : p.degree ≠ 0
⊢ ∃ (x : k), p.IsRoot x

Tactic:
(IsAlgClosed.splits p).exists_eval_eq_zero hp

Premises used: Polynomial.IsRoot, IsAlgClosed.splits, Polynomial.Splits.exists_eval_eq_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
rw : Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0
⊢ (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0

Tactic:
rw [degree_X_pow_sub_C hn x]

Premises used: Polynomial.degree_X_pow_sub_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0

Tactic:
ne_of_gt (WithBot.coe_lt_coe.2 hn)

Premises used: Iff.mpr, ne_of_gt, WithBot.coe_lt_coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0

Tactic:
exact ne_of_gt (WithBot.coe_lt_coe.2 hn)

Premises used: Iff.mpr, ne_of_gt, WithBot.coe_lt_coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0

Tactic:
have : degree (X ^ n - C x) ≠ 0 := by
    rw [degree_X_pow_sub_C hn x]
    exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
obtain :
  ∀ (z : k) (hz : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).IsRoot z),
    ∃ (z : k), z ^ n = x
⊢ ∃ (z : k), z ^ n = x

Tactic:
obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this

Premises used: Polynomial.C, HSub.hSub, IsAlgClosed.exists_root, HPow.hPow, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
z : k
hz : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).IsRoot z
h : z ^ n = x
⊢ ∃ (z : k), z ^ n = x

Tactic:
use z
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
z : k
hz : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).IsRoot z
⊢ z ^ n - x = 0

Tactic:
simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot.def, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x

Tactic:
sub_eq_zero.1 hz

Premises used: sub_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x

Tactic:
exact sub_eq_zero.1 hz

Premises used: sub_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
rcases : ∀ (z : k), ∃ (z_1 : k), HPow.hPow (β := ℕ) z 2 = z_1 * z_1
⊢ ∃ (z : k), x = z * z

Tactic:
rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩

Premises used: IsAlgClosed.exists_pow_nat_eq, zero_lt_two, rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
z : k
⊢ ∃ (z_1 : k), HPow.hPow (β := ℕ) z 2 = z_1 * z_1

Tactic:
⟨z, sq z⟩

Premises used: sq, Exists.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
z : k
⊢ ∃ (z_1 : k), HPow.hPow (β := ℕ) z 2 = z_1 * z_1

Tactic:
exact ⟨z, sq z⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
hp : p = (C : (a : k) → k[X]) (p.coeff 0)
rw : Eq.{u + 1} (α := Multiset k) (roots ((C : (a : k) → k[X]) (p.coeff 0))) 0
rw₁ rw₂ : Eq.{u + 1} (α := Multiset k) 0 0
⊢ p.roots = 0

Tactic:
rw [hp, roots_C]

Premises used: Polynomial.roots_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
refine : ∀ (h : p.roots = 0), p = (C : (a : k) → k[X]) (p.coeff 0)
⊢ p.roots = 0 ↔ p = (C : (a : k) → k[X]) (p.coeff 0)

Tactic:
refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
h : p.roots = 0
inl : ∀ (hd : p.degree ≤ 0), p = (C : (a : k) → k[X]) (p.coeff 0)
inr : ∀ (hd : 0 < p.degree), p = (C : (a : k) → k[X]) (p.coeff 0)
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)

Tactic:
rcases le_or_gt (degree p) 0 with hd | hd

Premises used: Polynomial.degree, le_or_gt, OfNat.ofNat
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)

Tactic:
eq_C_of_degree_le_zero hd

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)

Tactic:
exact eq_C_of_degree_le_zero hd

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
inr : ∀ (z : k) (hz : p.IsRoot z), p = (C : (a : k) → k[X]) (p.coeff 0)
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)

Tactic:
obtain ⟨z, hz⟩ := IsAlgClosed.exists_root p hd.ne'

Premises used: LT.lt.ne', IsAlgClosed.exists_root
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : p.IsRoot z
⊢ Membership.mem (γ := Multiset k) 0 z

Tactic:
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz

Premises used: Polynomial.ne_zero_of_degree_gt, Polynomial.mem_roots
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : Membership.mem (γ := Multiset k) 0 z
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)

Tactic:
simp at hz
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
⊢ p.roots = 0 ↔ p.natDegree = 0

Tactic:
roots_eq_zero_iff.trans eq_C_coeff_zero_iff_natDegree_eq_zero

Premises used: Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero, Iff.trans, IsAlgClosed.roots_eq_zero_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
⊢ p.roots = 0 ↔ p.degree ≤ 0

Tactic:
roots_eq_zero_iff_natDegree_eq_zero.trans natDegree_eq_zero_iff_degree_le_zero

Premises used: IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero, Iff.trans, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
have :
  ∀ (w : k[X]),
    Multiset.prod
            (Multiset.map (fun (a : k) ↦ HSub.hSub (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) a : k[X])) p.roots) *
          w =
        p →
      ∀ (hdeg : p.roots.card + w.natDegree = p.natDegree) (hroots : w.roots = 0), p.roots.card = p.natDegree
⊢ p.roots.card = p.natDegree

Tactic:
have ⟨_, _, hdeg, hroots⟩ := exists_prod_multiset_X_sub_C_mul p
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
w : k[X]
left :
  Multiset.prod
        (Multiset.map (fun (a : k) ↦ HSub.hSub (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) a : k[X])) p.roots) *
      w =
    p
hdeg : p.roots.card + w.natDegree = p.natDegree
hroots : w.roots = 0
⊢ p.roots.card = p.natDegree

Tactic:
simp [← hdeg, roots_eq_zero_iff_natDegree_eq_zero.mp hroots]

Premises used: IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : Semiring A
inst_1 : Field B
inst_2 : IsAlgClosed B
f : A →+* B
p : A[X]
hf : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) p.leadingCoeff : B) (0 : B)
⊢ (map f p).roots.card = p.natDegree

Tactic:
natDegree_map_of_leadingCoeff_ne_zero _ hf ▸ card_roots_eq_natDegree

Premises used: IsAlgClosed.card_roots_eq_natDegree, Eq.rec, Polynomial.natDegree_map_of_leadingCoeff_ne_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : Semiring A
inst_1 : Field B
inst_2 : IsAlgClosed B
f : A →+* B
p : A[X]
h : IsUnit p.leadingCoeff
⊢ (map f p).roots.card = p.natDegree

Tactic:
natDegree_map_eq_of_isUnit_leadingCoeff f h ▸ card_roots_eq_natDegree

Premises used: IsAlgClosed.card_roots_eq_natDegree, Eq.rec, Polynomial.natDegree_map_eq_of_isUnit_leadingCoeff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : Semiring A
inst_1 : Field B
inst_2 : IsAlgClosed B
f : A →+* B
p : A[X]
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ (map f p).roots.card = p.natDegree

Tactic:
natDegree_map_eq_of_injective hf _ ▸ card_roots_eq_natDegree

Premises used: IsAlgClosed.card_roots_eq_natDegree, Eq.rec, Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : IsSimpleRing A
inst_2 : Field B
inst_3 : IsAlgClosed B
f : A →+* B
p : A[X]
⊢ (map f p).roots.card = p.natDegree

Tactic:
natDegree_map f ▸ card_roots_eq_natDegree

Premises used: IsAlgClosed.card_roots_eq_natDegree, Polynomial.natDegree_map, Eq.rec
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Field B
inst_2 : IsAlgClosed B
inst_3 : Algebra A B
p : A[X]
hf : Ne.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) p.leadingCoeff : B) (0 : B)
⊢ (p.aroots B).card = p.natDegree

Tactic:
card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero hf

Premises used: IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Field B
inst_2 : IsAlgClosed B
inst_3 : Algebra A B
p : A[X]
h : IsUnit p.leadingCoeff
⊢ (p.aroots B).card = p.natDegree

Tactic:
card_roots_map_eq_natDegree_of_isUnit_leadingCoeff _ h

Premises used: IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Field B
inst_2 : IsAlgClosed B
inst_3 : Algebra A B
inst_4 : FaithfulSMul A B
p : A[X]
⊢ (p.aroots B).card = p.natDegree

Tactic:
card_roots_map_eq_natDegree_of_injective _ <| FaithfulSMul.algebraMap_injective _ _

Premises used: IsAlgClosed.card_roots_map_eq_natDegree_of_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p q : k[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ p ∣ q ↔ p.roots ≤ q.roots

Tactic:
Splits.dvd_iff_roots_le_roots (splits _) hp hq

Premises used: Polynomial.Splits.dvd_iff_roots_le_roots, IsAlgClosed.splits
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p q : k[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ Associated p q ↔ p.roots = q.roots

Tactic:
⟨Associated.roots_eq, fun h ↦ associated_of_dvd_dvd
    (dvd_iff_roots_le_roots hp hq |>.mpr <| le_of_eq h)
    (dvd_iff_roots_le_roots hq hp |>.mpr <| le_of_eq h.symm)⟩

Premises used: Iff.mpr, associated_of_dvd_dvd, Iff.intro, Associated.roots_eq, le_of_eq, Eq.symm, IsAlgClosed.dvd_iff_roots_le_roots
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
R : Type u_1
inst_1 : Semiring R
inst_2 : IsAlgClosed k
f : R →+* k
hf : Function.Injective.{u_1 + 1, u + 1} (α := R) (β := k) (⇑f : (a : R) → k)
p : R[X]
hp rwa rwa₁ rwa₂ rwa₃ : p.degree ≠ 0
⊢ (map f p).degree ≠ 0

Tactic:
rwa [degree_map_eq_of_injective hf]

Premises used: Polynomial.degree_map_eq_of_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
R : Type u_1
inst_1 : Semiring R
inst_2 : IsAlgClosed k
f : R →+* k
hf : Function.Injective.{u_1 + 1, u + 1} (α := R) (β := k) (⇑f : (a : R) → k)
p : R[X]
hp : p.degree ≠ 0
x : k
hx : (map f p).IsRoot x
rwa : eval x (map f p) = 0
rwa₁ rwa₂ rwa₃ rwa₄ : (map f p).IsRoot x
⊢ eval₂ f x p = 0

Tactic:
rwa [eval₂_eq_eval_map, ← IsRoot]

Premises used: Polynomial.IsRoot, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
R : Type u_1
inst_1 : Ring R
inst_2 : IsSimpleRing R
inst_3 : IsAlgClosed k
f : R →+* k
p : R[X]
hp : p.degree ≠ 0
⊢ ∃ (x : k), eval₂ f x p = 0

Tactic:
exists_eval₂_eq_zero_of_injective _ f.injective _ hp

Premises used: IsAlgClosed.exists_eval₂_eq_zero_of_injective, RingHom.injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
R : Type u_1
inst_1 : CommSemiring R
inst_2 : IsAlgClosed k
inst_3 : Algebra R k
hinj : Function.Injective.{u_1 + 1, u + 1} (α := R) (β := k) (⇑(algebraMap R k) : (a : R) → k)
p : R[X]
hp : p.degree ≠ 0
⊢ ∃ (x : k), Eq.{u + 1} (α := k) ((aeval x : (a : R[X]) → k) p : k) (0 : k)

Tactic:
exists_eval₂_eq_zero_of_injective (algebraMap R k) hinj p hp

Premises used: Algebra.algebraMap, IsAlgClosed.exists_eval₂_eq_zero_of_injective, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
R : Type u_1
inst_1 : CommSemiring R
inst_2 : IsAlgClosed k
inst_3 : Algebra R k
inst_4 : FaithfulSMul R k
p : R[X]
hp : p.degree ≠ 0
⊢ ∃ (x : k), Eq.{u + 1} (α := k) ((aeval x : (a : R[X]) → k) p : k) (0 : k)

Tactic:
exists_aeval_eq_zero_of_injective _ (FaithfulSMul.algebraMap_injective ..) _ hp

Premises used: IsAlgClosed.exists_aeval_eq_zero_of_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
obtain :
  ∀ (x : k) (hx : eval x (HMul.hMul (β := k[X]) p ((C : (a : k) → k[X]) p.leadingCoeff⁻¹ : k[X])) = 0),
    ∃ (x : k), eval x p = 0
⊢ ∃ (x : k), eval x p = 0

Tactic:
obtain ⟨x, hx⟩ := H (p * C (leadingCoeff p)⁻¹) (monic_mul_leadingCoeff_inv hp.ne_zero)
      (irreducible_mul_leadingCoeff_inv.mpr hp)

Premises used: Iff.mpr, Polynomial.C, HMul.hMul, Polynomial.irreducible_mul_leadingCoeff_inv, Polynomial.leadingCoeff, Inv.inv, Polynomial.monic_mul_leadingCoeff_inv, Irreducible.ne_zero, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
x : k
hx : eval x (HMul.hMul (β := k[X]) p ((C : (a : k) → k[X]) p.leadingCoeff⁻¹ : k[X])) = 0
⊢ eval x p = 0

Tactic:
simpa [hp.ne_zero] using hx

Premises used: Irreducible.ne_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
x : k
hx : eval x (HMul.hMul (β := k[X]) p ((C : (a : k) → k[X]) p.leadingCoeff⁻¹ : k[X])) = 0
⊢ ∃ (x : k), eval x p = 0

Tactic:
exact ⟨x, by simpa [hp.ne_zero] using hx⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ (x : k), eval x p = 0
⊢ ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0

Tactic:
replace H (p : k[X]) (hp : Irreducible p) : ∃ x, p.eval x = 0 := by
    obtain ⟨x, hx⟩ := H (p * C (leadingCoeff p)⁻¹) (monic_mul_leadingCoeff_inv hp.ne_zero)
      (irreducible_mul_leadingCoeff_inv.mpr hp)
    exact ⟨x, by simpa [hp.ne_zero] using hx⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
⊢ IsAlgClosed k

Tactic:
⟨fun p ↦ ?_⟩

Premises used: IsAlgClosed.mk
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
refine : ∀ (p : k[X]), p.Splits
⊢ IsAlgClosed k

Tactic:
refine ⟨fun p ↦ ?_⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
pos : ∀ (hp0 : p = 0), p.Splits
neg : ∀ (hp0 : ¬p = 0), p.Splits
⊢ p.Splits

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
hp0 : p = 0
⊢ p.Splits

Tactic:
simp [hp0]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
hp0 : ¬p = 0
neg : ∀ (u : k[X]ˣ) (hu : (UniqueFactorizationMonoid.factors p).prod * (↑u : k[X]) = p), p.Splits
⊢ p.Splits

Tactic:
obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hp0

Premises used: UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * (↑u : k[X]) = p
neg : ((UniqueFactorizationMonoid.factors p).prod * (↑u : k[X])).Splits
⊢ p.Splits

Tactic:
rw [← hu]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * (↑u : k[X]) = p
⊢ ((UniqueFactorizationMonoid.factors p).prod * (↑u : k[X])).Splits

Tactic:
(Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits

Premises used: Polynomial.Splits.multisetProd, IsUnit.splits, Units.isUnit, Polynomial.Splits.mul
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * (↑u : k[X]) = p
neg : ∀ (f : k[X]) (hf : f ∈ UniqueFactorizationMonoid.factors p), f.Splits
⊢ ((UniqueFactorizationMonoid.factors p).prod * (↑u : k[X])).Splits

Tactic:
refine (Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits

Premises used: Polynomial.Splits.multisetProd, IsUnit.splits, Units.isUnit, Polynomial.Splits.mul
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * (↑u : k[X]) = p
f : k[X]
hf : f ∈ UniqueFactorizationMonoid.factors p
h : Irreducible f := ⋯
neg : ∀ (x : k) (hx : eval x f = 0), f.Splits
⊢ f.Splits

Tactic:
obtain ⟨x, hx⟩ := H f h