awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
k : ℤ
hk : k ≠ 0
inl : ∀ (n : ℕ) (hk : Ne (α := ℤ) (↑n : ℤ) 0), ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)
⊢ ∃ (r : R), x = r ^ k
have inr : ∀ (n : ℕ) (hk : Ne (α := ℤ) (-(↑n : ℤ)) 0), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
Tactic: rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (-(↑n : ℤ)) 0
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
have inr : ∀ (r : R) (hr : x = r ^ n), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
Tactic: rcases exists_eq_pow_of_isSquare hx (by simpa using hk) with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
h : 0 ≤ x
⊢ IsSquare x
have suffices : IsSquare (-x) → x = 0
Tactic: suffices IsSquare (-x) → x = 0 by aesop
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
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.natDegree ≠ 0
have 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
Tactic: have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ f.natDegree ≠ 0
have pos : ∀ (ha : a = 0), f.natDegree ≠ 0
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ f.natDegree ≠ 0
have neg : ∀ (ha : ¬a = 0), f.natDegree ≠ 0
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
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])
⊢ ∃ (x : k), a * x ^ n + b * x + c = 0
have hdeg : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
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
⊢ ∃ (x : k), a * x ^ n + b * x + c = 0
have hsep : f.Separable
Tactic: have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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), a * x ^ n + b * x + c = 0
have obtain : ∀ (x : k) (hx : f.IsRoot x), ∃ (x : k), a * x ^ n + b * x + c = 0
Tactic: obtain ⟨x, hx⟩ := exists_root f hdeg hsep
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
h : n = 0
⊢ False
have hn₁ : NeZero.{u} (R := k) 0
Tactic: rw [h, Nat.cast_zero] at hn
Cleared hypotheses: hn, h
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
⊢ ∃ (z : k), z ^ n = x
have hn' : 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
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
have rw : Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0
Tactic: rw [degree_X_pow_sub_C hn' x]
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
n : ℕ
hn : NeZero.{u} (R := k) (↑n : k)
hn' : 0 < n
⊢ ∃ (z : k), z ^ n = x
have this : (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'
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ ∃ (z : k), z ^ n = x
have pos : ∀ (hx : x = 0), ∃ (z : k), z ^ n = x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ ∃ (z : k), z ^ n = x
have neg : ∀ (hx : ¬x = 0), ∃ (z : k), z ^ n = x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ HPow.hPow (α := k) 0 n = x
have rw : HPow.hPow (α := k) 0 n = 0
Tactic: rw [hx, pow_eq_zero_iff hn'.ne']
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ HPow.hPow (α := k) 0 n = x
have rw₁ : Eq.{u + 1} (α := k) 0 0
Tactic: rw [hx, pow_eq_zero_iff hn'.ne']
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
have 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
Tactic: obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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 : k), z ^ n = x
have h : z ^ n = x
Tactic: use z
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
x : k
h2 : NeZero.{u} (R := k) 2
⊢ ∃ (z : k), x = z * z
have rcases : ∀ (z : k), ∃ (z_1 : k), HPow.hPow (β := ℕ) z 2 = z_1 * z_1
Tactic: rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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)
⊢ p.roots = 0
have rw : Eq.{u + 1} (α := Multiset k) (roots ((C : (a : k) → k[X]) (p.coeff 0))) 0
Tactic: rw [hp, roots_C]
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ p.roots = 0
have rw₁ : Eq.{u + 1} (α := Multiset k) 0 0
Tactic: rw [hp, roots_C]
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
⊢ p.roots = 0 ↔ p = (C : (a : k) → k[X]) (p.coeff 0)
have refine : ∀ (h : p.roots = 0), p = (C : (a : k) → k[X]) (p.coeff 0)
Tactic: refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)
have inl : ∀ (hd : p.degree ≤ 0), p = (C : (a : k) → k[X]) (p.coeff 0)
Tactic: rcases le_or_gt (degree p) 0 with hd | hd
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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)
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)
have inr : ∀ (hd : 0 < p.degree), p = (C : (a : k) → k[X]) (p.coeff 0)
Tactic: rcases le_or_gt (degree p) 0 with hd | hd
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)
have inr : ∀ (z : k) (hz : p.IsRoot z), p = (C : (a : k) → k[X]) (p.coeff 0)
Tactic: obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
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
⊢ p = (C : (a : k) → k[X]) (p.coeff 0)
have hz₁ : Membership.mem (γ := Multiset k) 0 z
Tactic: rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ eval₂ f x p = 0
have rwa : eval x (map f p) = 0
Tactic: rwa [eval₂_eq_eval_map, ← IsRoot]
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
have 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
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))
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ (x : k), eval x p = 0
⊢ IsSepClosed k
have H₁ : ∀ (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⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
have refine : ∀ (p : k[X]) (hp : p.Separable), p.Splits
Tactic: refine ⟨fun p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ p.Splits
have pos : ∀ (hp0 : p = 0), p.Splits
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ p.Splits
have neg : ∀ (hp0 : ¬p = 0), p.Splits
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
have neg : ∀ (u : k[X]ˣ) (hu : (UniqueFactorizationMonoid.factors p).prod * (↑u : k[X]) = p), p.Splits
Tactic: obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hp0
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
⊢ p.Splits
have neg : ((UniqueFactorizationMonoid.factors p).prod * (↑u : k[X])).Splits
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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
have neg : ∀ (f : k[X]) (hf : f ∈ UniqueFactorizationMonoid.factors p), f.Splits
Tactic: refine (Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
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 := ⋯
⊢ f.Splits
have neg : ∀ (x : k) (hx : eval x f = 0), f.Splits
Tactic: obtain ⟨x, hx⟩ := H f h (hp.of_dvd (UniqueFactorizationMonoid.dvd_of_mem_factors hf))
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
⊢ Function.Surjective.{u + 1, v + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)
have refine : ∀ (x : K), (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
Tactic: refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
have hq : leadingCoeff (minpoly k x) = 1
Tactic: have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsSeparable.isIntegral k x)
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
have hsep : IsSeparable k x
Tactic: have hsep : IsSeparable k x := Algebra.IsSeparable.isSeparable k x
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
have h : degree (minpoly k x) = 1
Tactic: have h : (minpoly k x).degree = 1 :=
    degree_eq_one_of_irreducible k (minpoly.irreducible (Algebra.IsSeparable.isIntegral k x)) hsep
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
h : degree (minpoly k x) = 1
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
have this : Eq.{v + 1} (α := K) ((aeval x : (a : k[X]) → K) (minpoly k x) : K) (0 : K)
Tactic: have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (hypothesis)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : IsSeparable k x
h : degree (minpoly k x) = 1
this : Eq.{v + 1} (α := K) ((aeval x : (a : k[X]) → K) (minpoly k x) : K) (0 : K)
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
have this₁ : x = -(algebraMap k K : (a : k) → K) (coeff (minpoly k x) 0)
Tactic: rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
    add_eq_zero_iff_eq_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IsSepClosed (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
inst_3 : Algebra k K
L : IntermediateField k K
inst_4 : Algebra.IsSeparable.{u, v} k ↥L
x : K
hx : x ∈ L
⊢ Membership.mem (γ := IntermediateField k K) ⊥ x
have obtain : ∀ (y : k) (hy : (algebraMap k ↥L : (a : k) → ↥L) y = Subtype.mk (p := fun (x : K) ↦ x ∈ L) x hx),
  Membership.mem (γ := IntermediateField k K) ⊥ x
Tactic: obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
⊢ Nonempty (E →ₐ[F] K)
have refine : (S : Finset E) → AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
Tactic: refine Lifts.nonempty_algHom_of_exist_lifts_finset fun S ↦ ⟨⟨adjoin F S, ?_⟩, subset_adjoin _ _⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
⊢ (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
have apply : Polynomial.map (algebraMap F K') (minpoly F s) ∣ Polynomial.map (algebraMap K p.SplittingField) p
Tactic: apply (SplittingField.splits p).of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
      fun _ _ ↦ Polynomial.map_ne_zero (minpoly.ne_zero <| alg.isIntegral.1 _))) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
⊢ Polynomial.map (algebraMap F K') (minpoly F s) ∣ Polynomial.map (algebraMap K p.SplittingField) p
have rw : Polynomial.map (algebraMap F K) (minpoly F s) ∣ p
Tactic: rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (hypothesis)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
⊢ AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
have splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
Tactic: have splits s (hs : s ∈ S) : ((minpoly F s).map (algebraMap F K')).Splits := by
    apply (SplittingField.splits p).of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
      fun _ _ ↦ Polynomial.map_ne_zero (minpoly.ne_zero <| alg.isIntegral.1 _))) ?_
    rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']
    exact Finset.dvd_prod_of_mem _ hs
-- Lean 4 proof step from Mathlib.FieldTheory.Isaacs (hypothesis)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ (y : K), Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ (s : E) (hs : s ∈ S), (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F (L' := K) ⊥
FS : IntermediateField F E := adjoin F (↑S : Set E)
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥FS) K'
⊢ AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
have this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
Tactic: have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _