awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
z : AlgebraicClosure k
p : MvPolynomial (Vars k) k
hp : (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z
C :
  ∀ (a : k) (z : AlgebraicClosure k)
    (hp :
      (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          ((MvPolynomial.C : (a : k) → MvPolynomial (Vars k) k) a) =
        z),
    IsIntegral k (A := AlgebraicClosure k)
      ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k)
          ((MvPolynomial.C : (a : k) → MvPolynomial (Vars k) k) a) :
        HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
⊢ IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
have add : ∀ (p q : MvPolynomial (Vars k) k)
  (ha :
    ∀ (z : AlgebraicClosure k)
      (hp :
        (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p = z),
      IsIntegral k (A := AlgebraicClosure k)
        ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) p :
          HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)))
  (hb :
    ∀ (z : AlgebraicClosure k)
      (hp :
        (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) q = z),
      IsIntegral k (A := AlgebraicClosure k)
        ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) q :
          HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k)))
  (z : AlgebraicClosure k)
  (hp :
    (Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) (p + q) =
      z),
  IsIntegral k (A := AlgebraicClosure k)
    ((Ideal.Quotient.mk (maxIdeal k) : (a : MvPolynomial (Vars k) k) → MvPolynomial (Vars k) k ⧸ maxIdeal k) (p + q) :
      HasQuotient.Quotient (MvPolynomial (Vars k) k) (B := Ideal (MvPolynomial (Vars k) k)) (maxIdeal k))
Tactic: induction p using MvPolynomial.induction_on generalizing z with
        | C => exact isIntegral_algebraMap
        | add _ _ ha hb => exact (ha _ rfl).add (hb _ rfl)
        | mul_X p fi ih =>
          rw [map_mul]
          refine (ih _ rfl).mul ⟨_, fi.1.2, ?_⟩
          simp_rw [← eval_map, Monics.map_eq_prod, eval_prod, Polynomial.map_sub, eval_sub]
          apply Finset.prod_eq_zero (Finset.mem_univ fi.2)
          rw [map_C]
          -- The `erw` is needed here because the `R` in `eval` is `AlgebraicClosure k`,
          -- but this has been unfolded in the arguments of `eval`.
          erw [eval_C]
          simp
Cleared hypotheses: z, p, hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure (goal)
Goal:
k : Type u
inst : Field k
f : k[X]
hf : f.Monic
h : Irreducible f
⊢ Splits (R := AlgebraicClosure k) (map (algebraMap k (AlgebraicClosure k)) f)
have rw : 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: rw [show f = (⟨f, hf⟩ : Monics k) from rfl, Monics.map_eq_prod]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
have rw : Ne (α := WithBot ℕ) (↑n : WithBot ℕ) 0
Tactic: rw [degree_X_pow_sub_C hn x]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
n : ℕ
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 ne_of_gt (WithBot.coe_lt_coe.2 hn)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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), z ^ n = x
have 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
Tactic: obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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 : k), z ^ n = x
have h : z ^ n = x
Tactic: use z
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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
have hz₁ : z ^ n - x = 0
Tactic: simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
x : k
⊢ ∃ (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 zero_lt_two with ⟨z, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
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.IsAlgClosed.Basic (goal)
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
⊢ p.roots = 0
have rw₁ : Eq.{u + 1} (α := Multiset k) 0 0
Tactic: rw [hp, roots_C]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
⊢ 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.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
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.IsAlgClosed.Basic (goal)
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)
⊢ 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.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
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⟩ := IsAlgClosed.exists_root p hd.ne'
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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
⊢ 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.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
⊢ p.roots.card = p.natDegree
have 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
Tactic: have ⟨_, _, hdeg, hroots⟩ := exists_prod_multiset_X_sub_C_mul p
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ 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.IsAlgClosed.Basic (goal)
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
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)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ (x : k), eval x p = 0
⊢ IsAlgClosed k
have H₁ : ∀ (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⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
⊢ IsAlgClosed k
have refine : ∀ (p : k[X]), p.Splits
Tactic: refine ⟨fun p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
H : ∀ (p : k[X]) (hp : Irreducible p), ∃ (x : k), eval x p = 0
p : k[X]
⊢ p.Splits
have pos : ∀ (hp0 : p = 0), p.Splits
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ p.Splits
have neg : ∀ (hp0 : ¬p = 0), p.Splits
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
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.IsAlgClosed.Basic (goal)
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
⊢ p.Splits
have neg : ((UniqueFactorizationMonoid.factors p).prod * (↑u : k[X])).Splits
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
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.IsAlgClosed.Basic (goal)
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 := ⋯
⊢ f.Splits
have neg : ∀ (x : k) (hx : eval x f = 0), f.Splits
Tactic: obtain ⟨x, hx⟩ := H f h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
⊢ IsAlgClosed k'
have H : ∀ (p : k'[X]), p.Monic → Irreducible p → ∃ (x : k'), eval x p = 0
Tactic: apply IsAlgClosed.of_exists_root
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ (map e.symm.toRingHom p).degree ≠ 0
have rw : p.degree ≠ 0
Tactic: rw [degree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ ∃ (x : k'), eval x p = 0
have hpe : (map e.symm.toRingHom p).degree ≠ 0
Tactic: have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
    rw [degree_map]
    exact ne_of_gt (degree_pos_of_irreducible hp)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
⊢ ∃ (x : k'), eval x p = 0
have H : ∀ (x : k) (hx : (map e.symm.toRingHom p).IsRoot x), ∃ (x : k'), eval x p = 0
Tactic: rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : (map e.symm.toRingHom p).IsRoot x
⊢ ∃ (x : k'), eval x p = 0
have h : Eq (α := k') (eval ((e : (a : k) → k') x) p : k') (0 : k')
Tactic: use e x
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : (map e.symm.toRingHom p).IsRoot x
⊢ Eq (α := k') (eval ((e : (a : k) → k') x) p : k') (0 : k')
have hx₁ : eval x (map e.symm.toRingHom p) = 0
Tactic: rw [IsRoot] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ Eq (α := k') (eval ((e : (a : k) → k') x) p : k') (0 : k')
have h : Eq (α := k) ((e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') : k) ((e.symm : (a : k') → k) 0 : k)
Tactic: apply e.symm.injective
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ Eq (α := k) ((e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') : k) ((e.symm : (a : k') → k) 0 : k)
have h : (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)
Tactic: rw [map_zero, ← hx]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
x : k
⊢ (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)
have h : ∀ (a : k'),
  (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) ((C : (a : k') → k'[X]) a) : k') =
    eval x (map e.symm.toRingHom ((C : (a : k') → k'[X]) a))
Tactic: induction p using Polynomial.induction_on
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
x : k
h :
  ∀ (a : k'),
    (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) ((C : (a : k') → k'[X]) a) : k') =
      eval x (map e.symm.toRingHom ((C : (a : k') → k'[X]) a))
⊢ (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)
have h₁ : ∀ (p q : k'[X]),
  (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p) →
    (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) q : k') = eval x (map e.symm.toRingHom q) →
      (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) (p + q) : k') = eval x (map e.symm.toRingHom (p + q))
Tactic: induction p using Polynomial.induction_on
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
p : k'[X]
x : k
h :
  ∀ (a : k'),
    (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) ((C : (a : k') → k'[X]) a) : k') =
      eval x (map e.symm.toRingHom ((C : (a : k') → k'[X]) a))
h₁ :
  ∀ (p q : k'[X]),
    (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p) →
      (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) q : k') = eval x (map e.symm.toRingHom q) →
        (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) (p + q) : k') = eval x (map e.symm.toRingHom (p + q))
⊢ (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)
have h₂ : ∀ (n : ℕ) (a : k'),
  (e.symm : (a : k') → k)
        (eval ((e : (a : k) → k') x)
            (HMul.hMul (α := k'[X]) ((C : (a : k') → k'[X]) a : k'[X]) (HPow.hPow (α := k'[X]) X n)) :
          k') =
      eval x
        (map e.symm.toRingHom
          (HMul.hMul (α := k'[X]) ((C : (a : k') → k'[X]) a : k'[X]) (HPow.hPow (α := k'[X]) X n))) →
    (e.symm : (a : k') → k)
        (eval ((e : (a : k) → k') x)
            (HMul.hMul (α := k'[X]) ((C : (a : k') → k'[X]) a : k'[X]) (HPow.hPow (α := k'[X]) X (n + 1))) :
          k') =
      eval x
        (map e.symm.toRingHom
          (HMul.hMul (α := k'[X]) ((C : (a : k') → k'[X]) a : k'[X]) (HPow.hPow (α := k'[X]) X (n + 1))))
Tactic: induction p using Polynomial.induction_on
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Ring K
inst_2 : IsDomain K
hk : IsAlgClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsIntegral k K
⊢ Function.Bijective.{u_1 + 1, u_2 + 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 ⟨RingHom.injective _, fun x ↦ ⟨-(minpoly k x).coeff 0, ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Ring K
inst_2 : IsDomain K
hk : IsAlgClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsIntegral 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.IsIntegral.isIntegral x)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Ring K
inst_2 : IsDomain K
hk : IsAlgClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ (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.IsIntegral.isIntegral x))
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Ring K
inst_2 : IsDomain K
hk : IsAlgClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
have this : Eq.{u_2 + 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.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Ring K
inst_2 : IsDomain K
hk : IsAlgClosed k
inst_3 : Algebra k K
inst_4 : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
this : Eq.{u_2 + 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.IsAlgClosed.Basic (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : IsAlgClosed k
inst_3 : Algebra k K
L : IntermediateField k K
inst_4 : Algebra.IsAlgebraic.{u_1, u_2} 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⟩ := (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)).2 (⟨x, hx⟩ : L)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
⊢ IsCoprime p q ↔
    ∀ (a : K),
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) p : K) (0 : K) ∨
        Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) q : K) (0 : K)
have refine_1 : ∀
  (h :
    ∀ (a : K),
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) p : K) (0 : K) ∨
        Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) q : K) (0 : K)),
  ¬(p = 0 ∧ q = 0)
Tactic: refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
refine_1 :
  ∀
    (h :
      ∀ (a : K),
        Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) p : K) (0 : K) ∨
          Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) q : K) (0 : K)),
    ¬(p = 0 ∧ q = 0)
⊢ IsCoprime p q ↔
    ∀ (a : K),
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) p : K) (0 : K) ∨
        Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) q : K) (0 : K)
have refine_2 : ∀
  (h :
    ∀ (a : K),
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) p : K) (0 : K) ∨
        Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) q : K) (0 : K))
  (x : k[X]) (hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x) (h0 : x ≠ 0), x ∣ p → ¬x ∣ q
Tactic: refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩