awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
this :
  (C : (a : k) → k[X]) 0 * HPow.hPow (α := k[X]) X n +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X =
    0 * HPow.hPow (α := k[X]) X n + HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X
pos : ∀ (ha : a = 0), f.natDegree ≠ 0
neg : ∀ (ha : ¬a = 0), f.natDegree ≠ 0
⊢ f.natDegree ≠ 0

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
this :
  (C : (a : k) → k[X]) 0 * HPow.hPow (α := k[X]) X n +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X =
    0 * HPow.hPow (α := k[X]) X n + HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X
ha : a = 0
⊢ f.natDegree ≠ 0

Tactic:
grind [zero_add]

Premises used: zero_add
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
this :
  (C : (a : k) → k[X]) 0 * HPow.hPow (α := k[X]) X n +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X =
    0 * HPow.hPow (α := k[X]) X n + HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X
ha : ¬a = 0
⊢ f.natDegree ≠ 0

Tactic:
grind [natDegree_add_eq_left_of_natDegree_lt]

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
⊢ f.degree ≠ 0

Tactic:
have hdeg : f.degree ≠ 0 := degree_ne_of_natDegree_ne (n := 0) <| by
    have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind
    by_cases ha : a = 0
    · grind [zero_add]
    · grind [natDegree_add_eq_left_of_natDegree_lt]
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
hdeg : f.degree ≠ 0
⊢ f.Separable

Tactic:
have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
hdeg : f.degree ≠ 0
hsep : f.Separable
obtain : ∀ (x : k) (hx : f.IsRoot x), ∃ (x : k), a * x ^ n + b * x + c = 0
⊢ ∃ (x : k), a * x ^ n + b * x + c = 0

Tactic:
obtain ⟨x, hx⟩ := exists_root f hdeg hsep

Premises used: IsSepClosed.exists_root
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ a * x ^ n + b * x + c = 0

Tactic:
simpa [f] using hx
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ ∃ (x : k), a * x ^ n + b * x + c = 0

Tactic:
exact ⟨x, by simpa [f] using hx⟩
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p n : ℕ
a b c : k
inst_2 : CharP k p
hn : p ∣ n
hn' : 2 ≤ n
hb : b ≠ 0
⊢ ∃ (x : k), a * x ^ n + b * x + c = 0

Tactic:
exists_root_C_mul_X_pow_add_C_mul_X_add_C a b c ((CharP.cast_eq_zero_iff k p n).2 hn) hn' hb

Premises used: Iff.mpr, CharP.cast_eq_zero_iff, IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : PerfectField k
⊢ IsAlgClosed k

Tactic:
IsAlgClosed.of_exists_root k fun p _ h ↦ exists_root p ((degree_pos_of_irreducible h).ne')
    (PerfectField.separable_of_irreducible h)

Premises used: PerfectField.separable_of_irreducible, LT.lt.ne', Polynomial.degree_pos_of_irreducible, IsAlgClosed.of_exists_root, IsSepClosed.exists_root
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
h : n = 0
⊢ NeZero.{u} (R := k) 0

Tactic:
rw [h, Nat.cast_zero] at hn

Premises used: Nat.cast_zero
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
h : n = 0
hn₁ : NeZero.{u} (R := k) 0
⊢ n = 0

Tactic:
rw [h, Nat.cast_zero] at hn

Premises used: Nat.cast_zero
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) 0
h : n = 0
⊢ False

Tactic:
hn.out rfl

Premises used: NeZero.out, rfl
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) 0
h : n = 0
⊢ False

Tactic:
exact hn.out rfl

Premises used: NeZero.out, rfl
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
⊢ 0 < n

Tactic:
have hn' : 0 < n := Nat.pos_of_ne_zero fun h => by
    rw [h, Nat.cast_zero] at hn
    exact hn.out rfl
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
⊢ Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0

Tactic:
(WithBot.coe_lt_coe.2 hn').ne'

Premises used: Iff.mpr, LT.lt.ne', WithBot.coe_lt_coe
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
⊢ Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0

Tactic:
exact (WithBot.coe_lt_coe.2 hn').ne'

Premises used: Iff.mpr, LT.lt.ne', WithBot.coe_lt_coe
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
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 (WithBot.coe_lt_coe.2 hn').ne'
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
pos : ∀ (hx : x = 0), ∃ (z : k), z ^ n = x
neg : ∀ (hx : ¬x = 0), ∃ (z : k), z ^ n = x
⊢ ∃ (z : k), z ^ n = x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
hx : x = 0
rw : HPow.hPow (α := k) 0 n = 0
rw₁ rw₂ : Eq.{u + 1} (α := k) 0 0
⊢ HPow.hPow (α := k) 0 n = x

Tactic:
rw [hx, pow_eq_zero_iff hn'.ne']

Premises used: pow_eq_zero_iff, LT.lt.ne'
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
hx : x = 0
⊢ ∃ (z : k), z ^ n = x

Tactic:
exact ⟨0, by rw [hx, pow_eq_zero_iff hn'.ne']⟩
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
hx : ¬x = 0
neg :
  ∀ (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 _ this <| separable_X_pow_sub_C x hn.out hx

Premises used: Polynomial.separable_X_pow_sub_C, NeZero.out, IsSepClosed.exists_root
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
hx : ¬x = 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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
this : (HSub.hSub (β := k[X]) (HPow.hPow (α := k[X]) X n) ((C : (a : k) → k[X]) x : k[X])).degree ≠ 0
hx : ¬x = 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

Tactic:
simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz

Premises used: Polynomial.eval_C, sub_eq_zero, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot.def, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
h2 : NeZero.{u} (R := k) 2
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 2 with ⟨z, rfl⟩

Premises used: IsSepClosed.exists_pow_nat_eq, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
h2 : NeZero.{u} (R := k) 2
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
h2 : NeZero.{u} (R := k) 2
z : k
⊢ ∃ (z_1 : k), HPow.hPow (β := ℕ) z 2 = z_1 * z_1

Tactic:
exact ⟨z, sq z⟩
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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⟩ := IsSepClosed.exists_root p hd.ne' hsep

Premises used: LT.lt.ne', IsSepClosed.exists_root
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
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.IsSepClosed
Goal:
K : Type v
inst : Field K
k : Type u_1
inst_1 : CommSemiring k
inst_2 : IsSepClosed K
f : k →+* K
hf : Function.Injective.{u_1 + 1, v + 1} (α := k) (β := K) (⇑f : (a : k) → K)
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
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.IsSepClosed
Goal:
K : Type v
inst : Field K
k : Type u_1
inst_1 : CommSemiring k
inst_2 : IsSepClosed K
f : k →+* K
hf : Function.Injective.{u_1 + 1, v + 1} (α := k) (β := K) (⇑f : (a : k) → K)
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
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.IsSepClosed
Goal:
K : Type v
inst : Field K
k : Type u_1
inst_1 : CommRing k
inst_2 : IsSimpleRing k
inst_3 : IsSepClosed K
f : k →+* K
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ ∃ (x : K), eval₂ f x p = 0

Tactic:
exists_eval₂_eq_zero_of_injective _ f.injective _ hp hsep

Premises used: RingHom.injective, IsSepClosed.exists_eval₂_eq_zero_of_injective
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
K : Type v
inst : Field K
k : Type u_1
inst_1 : CommSemiring k
inst_2 : IsSepClosed K
inst_3 : Algebra k K
inst_4 : FaithfulSMul k K
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ ∃ (x : K), Eq.{v + 1} (α := K) ((aeval x : (a : k[X]) → K) p : K) (0 : K)

Tactic:
exists_eval₂_eq_zero_of_injective _ (FaithfulSMul.algebraMap_injective ..) p hp hsep

Premises used: MonoidHomClass.toMonoidHom, FaithfulSMul.algebraMap_injective, RingHomClass.toRingHom, IsSepClosed.exists_eval₂_eq_zero_of_injective
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) p.leadingCoeff⁻¹ : k[X])

Tactic:
aesop
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
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) (hs.mul_unit (by aesop))

Premises used: Iff.mpr, Polynomial.C, HMul.hMul, Polynomial.irreducible_mul_leadingCoeff_inv, Polynomial.Separable.mul_unit, Polynomial.leadingCoeff, Inv.inv, Polynomial.monic_mul_leadingCoeff_inv, Irreducible.ne_zero, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ (x : k), eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ (x : k), eval x p = 0
⊢ ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0

Tactic:
replace H (p : k[X]) (hp : Irreducible p) (hs : Separable 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) (hs.mul_unit (by aesop))
    exact ⟨x, by simpa [hp.ne_zero] using hx⟩
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
⊢ IsSepClosed k

Tactic:
⟨fun p hp ↦ ?_⟩

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

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

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

Tactic:
simp [hp0]
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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 (hp.of_dvd (UniqueFactorizationMonoid.dvd_of_mem_factors hf))

Premises used: UniqueFactorizationMonoid.dvd_of_mem_factors, Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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 := ⋯
x : k
hx : eval x f = 0
⊢ f.Splits

Tactic:
Splits.of_degree_eq_one (degree_eq_one_of_irreducible_of_root h hx)

Premises used: Polynomial.Splits.of_degree_eq_one, Polynomial.degree_eq_one_of_irreducible_of_root
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p) (hs : p.Separable), ∃ (x : k), eval x p = 0
p : k[X]
hp : p.Separable
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 := ⋯
x : k
hx : eval x f = 0
⊢ f.Splits

Tactic:
exact Splits.of_degree_eq_one (degree_eq_one_of_irreducible_of_root h hx)

Premises used: Polynomial.Splits.of_degree_eq_one, Polynomial.degree_eq_one_of_irreducible_of_root
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hp : Irreducible p
hsep : p.Separable
⊢ p.degree = 1

Tactic:
(IsSepClosed.splits_of_separable p hsep).degree_eq_one_of_irreducible hp

Premises used: Polynomial.Splits.degree_eq_one_of_irreducible, IsSepClosed.splits_of_separable