awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 := ⋯
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.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 := ⋯
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.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
H : ∀ (p : k'[X]), p.Monic → Irreducible p → ∃ (x : k'), eval x p = 0
⊢ IsAlgClosed k'

Tactic:
apply IsAlgClosed.of_exists_root

Premises used: IsAlgClosed.of_exists_root
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
rw : p.degree ≠ 0
⊢ (map e.symm.toRingHom p).degree ≠ 0

Tactic:
rw [degree_map]

Premises used: Polynomial.degree_map
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ p.degree ≠ 0

Tactic:
ne_of_gt (degree_pos_of_irreducible hp)

Premises used: ne_of_gt, Polynomial.degree_pos_of_irreducible
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ p.degree ≠ 0

Tactic:
exact ne_of_gt (degree_pos_of_irreducible hp)

Premises used: ne_of_gt, Polynomial.degree_pos_of_irreducible
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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

Tactic:
have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
    rw [degree_map]
    exact ne_of_gt (degree_pos_of_irreducible hp)
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
H : ∀ (x : k) (hx : (map e.symm.toRingHom p).IsRoot x), ∃ (x : k'), eval x p = 0
⊢ ∃ (x : k'), eval x p = 0

Tactic:
rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩

Premises used: IsAlgClosed.exists_root, RingEquiv.toRingHom, Polynomial.map, RingEquiv.symm
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
h : Eq (α := k') (eval ((e : (a : k) → k') x) p : k') (0 : k')
⊢ ∃ (x : k'), eval x p = 0

Tactic:
use e x

Premises used: DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ eval x (map e.symm.toRingHom p) = 0

Tactic:
rw [IsRoot] at hx

Premises used: Polynomial.IsRoot
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
h : Eq (α := k) ((e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') : k) ((e.symm : (a : k') → k) 0 : k)
⊢ Eq (α := k') (eval ((e : (a : k) → k') x) p : k') (0 : k')

Tactic:
apply e.symm.injective

Premises used: RingEquiv.injective, RingEquiv.symm
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
h : (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)
⊢ Eq (α := k) ((e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') : k) ((e.symm : (a : k') → k) 0 : k)

Tactic:
rw [map_zero, ← hx]

Premises used: map_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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))
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))))
⊢ (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)

Tactic:
induction p using Polynomial.induction_on
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
x : k
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:
simp_all
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
x : k
p q : k'[X]
h : (e.symm : (a : k') → k) (eval ((e : (a : k) → k') x) p : k') = eval x (map e.symm.toRingHom p)
h_1 : (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:
simp_all
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
k' : Type u
inst_1 : Field k'
e : k ≃+* k'
inst_2 : IsAlgClosed k
x : k
n : ℕ
a : k'
h :
  (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:
simp_all
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
inst_1 : IsAlgClosed k
p : k[X]
hp : Irreducible p
⊢ p.degree = 1

Tactic:
(IsAlgClosed.splits p).degree_eq_one_of_irreducible hp

Premises used: Polynomial.Splits.degree_eq_one_of_irreducible, IsAlgClosed.splits
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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)

Tactic:
⟨RingHom.injective _, fun x ↦ ⟨-(minpoly k x).coeff 0, ?_⟩⟩

Premises used: RingHom.injective, minpoly, Polynomial.coeff, And.intro, Exists.intro, Function.Bijective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
refine : ∀ (x : K), (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)

Tactic:
refine ⟨RingHom.injective _, fun x ↦ ⟨-(minpoly k x).coeff 0, ?_⟩⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ leadingCoeff (minpoly k x) = 1

Tactic:
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsIntegral.isIntegral x)
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ 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))
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
⊢ 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
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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)
⊢ 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

Premises used: Polynomial.C_1, Polynomial.eq_X_add_C_of_degree_eq_one, add_eq_zero_iff_eq_neg, Polynomial.aeval_C, Polynomial.aeval_add, one_mul, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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 : x = -(algebraMap k K : (a : k) → K) (coeff (minpoly k x) 0)
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x

Tactic:
(map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm

Premises used: Algebra.algebraMap, Eq.rec, map_neg, minpoly, Polynomial.coeff, OfNat.ofNat, Eq.symm
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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 : x = -(algebraMap k K : (a : k) → K) (coeff (minpoly k x) 0)
⊢ (algebraMap k K : (a : k) → K) (-coeff (minpoly k x) 0) = x

Tactic:
exact (map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : CommRing K
inst_2 : IsDomain K
inst_3 : IsAlgClosed k
f : k →+* K
hf : f.IsIntegral
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑f : (a : k) → K)

Tactic:
let _ : Algebra k K := f.toAlgebra
  have : Algebra.IsIntegral k K := ⟨hf⟩
  algebraMap_bijective_of_isIntegral

Premises used: IsAlgClosed.algebraMap_bijective_of_isIntegral, Algebra.IsIntegral.mk, RingHom.toAlgebra
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
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
⊢ Membership.mem (γ := IntermediateField k K) ⊥ x

Tactic:
obtain ⟨y, hy⟩ := (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)).2 (⟨x, hx⟩ : L)

Premises used: Subtype.mk, And.right, IsAlgClosed.algebraMap_bijective_of_isIntegral
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
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:
⟨y, congr_arg (algebraMap L K) hy⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, Membership.mem, Subtype, congr_arg, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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
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:
exact ⟨y, congr_arg (algebraMap L K) hy⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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)

Tactic:
⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩

Premises used: isCoprime_of_dvd, Polynomial.aeval_ne_zero_of_isCoprime, Iff.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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)
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
⊢ 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)

Tactic:
refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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]
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)
⊢ Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∨
    Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)

Tactic:
replace h := h 0
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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]
h :
  Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∨
    Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
refine_1 :
  ∀ (h : p = 0 ∧ q = 0),
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
      Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
⊢ ¬(p = 0 ∧ q = 0)

Tactic:
contrapose! h
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
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]
h : p = 0 ∧ q = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
refine_1₁ :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K)
refine_1₂ : Eq.{v + 1} (α := K) 0 0 ∧ Eq.{v + 1} (α := K) 0 0
refine_1₃ refine_1₄ : Eq.{v + 1} (α := K) 0 0
⊢ Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)

Tactic:
rw [h.left, h.right, map_zero, and_self]

Premises used: and_self, map_zero, And.right, And.left
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
⊢ degree (map (algebraMap k K) x) ≠ 0

Tactic:
simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm

Premises used: Ne.symm, Polynomial.degree_pos_of_ne_zero_of_nonunit, Polynomial.degree_map, ne_of_lt
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
refine_2 : ∀ (a : K) (ha : eval a (map (algebraMap k K) x) = 0), False
⊢ False

Tactic:
obtain ⟨a, ha : _ = _⟩ := IsAlgClosed.exists_root (x.map <| algebraMap k K) <| by
      simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm

Premises used: Algebra.algebraMap, IsAlgClosed.exists_root, Polynomial.map
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
a : K
ha : eval a (map (algebraMap k K) x) = 0
simp_rw :
  HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w : K) = 0 ∧
    HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w_1 : K) = 0
simp_rw₁ :
  eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w) = 0 ∧
    eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w_1) = 0
simp_rw₂ : 0 * eval a (map (algebraMap k K) w) = 0 ∧ 0 * eval a (map (algebraMap k K) w_1) = 0
simp_rw₃ : True ∧ True
⊢ Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)

Tactic:
simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]

Premises used: MulZeroClass.zero_mul, map_mul, Polynomial.eval_map_algebraMap, true_and
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
a : K
ha : eval a (map (algebraMap k K) x) = 0
⊢ False

Tactic:
exact not_and_or.mpr (h a) (by simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and])

Premises used: Iff.mpr, not_and_or
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : Algebra k K
⊢ IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K

Tactic:
⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩

Premises used: IsAlgClosure.mk, IsAlgClosure.isAlgClosed, And.right, And.left, IsAlgClosure.isAlgebraic, And.intro, Iff.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
R : Type u_1
K : Type u_2
inst_1 : Field R
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsAlgClosure R K
inst_5 : CharZero R
⊢ Algebra.IsSeparable R K

Tactic:
⟨fun _ => (minpoly.irreducible (Algebra.IsIntegral.isIntegral _)).separable⟩

Premises used: Algebra.IsIntegral.isIntegral, Irreducible.separable, minpoly.irreducible, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : p.natDegree ≠ 0
x : M
rw : ∀ (hp : 0 < p.degree) (x : M), ∃ (a : M), (fun (x : M) ↦ eval x p) a = x
⊢ ∃ (a : M), (fun (x : M) ↦ eval x p) a = x

Tactic:
rw [← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at hp

Premises used: Nat.pos_iff_ne_zero, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x : M
⊢ (HSub.hSub (β := M[X]) p ((C : (a : M) → M[X]) x : M[X])).degree ≠ 0

Tactic:
simpa only [degree_sub_C hp] using hp.ne'

Premises used: LT.lt.ne', Polynomial.degree_sub_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x : M
have :
  ∀ (y : M) (hy : eval y (HSub.hSub (β := M[X]) p ((C : (a : M) → M[X]) x : M[X])) = 0),
    ∃ (a : M), (fun (x : M) ↦ eval x p) a = x
⊢ ∃ (a : M), (fun (x : M) ↦ eval x p) a = x

Tactic:
have ⟨y, hy⟩ := (IsAlgClosed.splits (p - C x)).exists_eval_eq_zero <| by
      simpa only [degree_sub_C hp] using hp.ne'
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x y : M
hy : eval y (HSub.hSub (β := M[X]) p ((C : (a : M) → M[X]) x : M[X])) = 0
⊢ (fun (x : M) ↦ eval x p) y = x

Tactic:
simpa [eval_sub, sub_eq_zero] using hy

Premises used: sub_eq_zero, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x y : M
hy : eval y (HSub.hSub (β := M[X]) p ((C : (a : M) → M[X]) x : M[X])) = 0
⊢ ∃ (a : M), (fun (x : M) ↦ eval x p) a = x

Tactic:
exact ⟨y, by simpa [eval_sub, sub_eq_zero] using hy⟩