awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
h₁ : IsUnit.{u_1} (M := A[X]) 1
⊢ IsUnit c

Tactic:
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
    C_1]

Premises used: Polynomial.C_1, Polynomial.eq_C_of_natDegree_le_zero, Polynomial.leadingCoeff, Polynomial.Monic.leadingCoeff, Nat.eq_zero_of_le_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit.{u_1} (M := A[X]) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit.{u_1} (M := A[X]) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
⊢ Irreducible (M := A[X]) (minpoly A x)

Tactic:
(irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => ?_

Premises used: Iff.mpr, minpoly.monic, Polynomial.irreducible_of_monic, minpoly.ne_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
refine : ∀ (f g : A[X]) (hf : f.Monic) (hg : g.Monic) (he : f * g = minpoly A x), f = 1 ∨ g = 1
⊢ Irreducible (M := A[X]) (minpoly A x)

Tactic:
refine (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => ?_

Premises used: Iff.mpr, minpoly.monic, Polynomial.irreducible_of_monic, minpoly.ne_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
rw : IsUnit f ∨ IsUnit g
⊢ f = 1 ∨ g = 1

Tactic:
rw [← hf.isUnit_iff, ← hg.isUnit_iff]

Premises used: Polynomial.Monic.isUnit_iff
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
by_contra! : ∀ (h : ¬IsUnit f ∧ ¬IsUnit g), False
⊢ IsUnit f ∨ IsUnit g

Tactic:
by_contra! h
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (f * g) : B)
    ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)

Tactic:
have heval := congr_arg (Polynomial.aeval x) he
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (f * g) : B)
    ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)

Tactic:
rw [aeval A x, aeval_mul, mul_eq_zero] at heval

Premises used: minpoly.aeval, mul_eq_zero, Polynomial.aeval_mul
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
inl : ∀ (heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)), False
inr : ∀ (heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)), False
⊢ False

Tactic:
rcases heval with heval | heval
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)
⊢ False

Tactic:
aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval

Premises used: minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly, And.right, And.intro, Exists.intro, Eq.symm, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)
⊢ False

Tactic:
exact aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval

Premises used: minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly, And.right, And.intro, Exists.intro, Eq.symm, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
⊢ False

Tactic:
aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, ?_⟩ heval

Premises used: minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly, And.left, And.intro, Exists.intro, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
inr : minpoly A x = g * f
⊢ False

Tactic:
refine aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, ?_⟩ heval

Premises used: minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly, And.left, And.intro, Exists.intro, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
inr : minpoly A x = f * g
inr₁ inr₂ : Eq (α := A[X]) (minpoly A x) (minpoly A x)
⊢ minpoly A x = g * f

Tactic:
rw [mul_comm, he]

Premises used: mul_comm
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ ⟦x⟧ = mk K x

Tactic:
rfl

Premises used: ConjRootClass.mk, rfl
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
motive : ConjRootClass K L → Prop
h : ∀ (x : L), motive (mk K x)
c : ConjRootClass K L
⊢ motive c

Tactic:
Quotient.ind h c

Premises used: Quotient.ind
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
⊢ Eq (α := ConjRootClass K L) (mk K x) (mk K y) ↔ IsConjRoot K x y

Tactic:
Quotient.eq

Premises used: ConjRootClass, ConjRootClass.mk, Quotient.eq
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ Eq.{u_2 + 1} (α := ConjRootClass K L) (mk K 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
rw : Eq (α := ConjRootClass K L) 0 (mk K x) ↔ x = 0
rw₁ : Eq (α := ConjRootClass K L) (mk K 0) (mk K x) ↔ x = 0
rw₂ : IsConjRoot K 0 x ↔ x = 0
rw₃ rw₄ : x = 0 ↔ x = 0
⊢ Eq (α := ConjRootClass K L) (mk K x) 0 ↔ x = 0

Tactic:
rw [eq_comm (b := 0), ← mk_zero, mk_eq_mk, isConjRoot_zero_iff_eq_zero]

Premises used: ConjRootClass.mk_zero, eq_comm, isConjRoot_zero_iff_eq_zero, ConjRootClass.mk_eq_mk
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
c : ConjRootClass K L
⊢ x ∈ c.carrier ↔ mk K x = c

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton, ConjRootClass.carrier
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
h : ∀ (x : L), Membership.mem (γ := Set L) (carrier.{u_1, u_2} (K := K) 0) x ↔ Membership.mem (γ := Set L) {0} x
⊢ Eq (α := Set L) (carrier.{u_1, u_2} (K := K) 0) {0}

Tactic:
ext
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : Eq (α := ConjRootClass K L) (mk K x) 0 ↔ Membership.mem (γ := Set L) {0} x
h₁ : x = 0 ↔ Membership.mem (γ := Set L) {0} x
h₂ h₃ : x = 0 ↔ x = 0
⊢ Membership.mem (γ := Set L) (carrier.{u_1, u_2} (K := K) 0) x ↔ Membership.mem (γ := Set L) {0} x

Tactic:
rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]

Premises used: ConjRootClass.mk_eq_zero_iff, Set.mem_singleton_iff, ConjRootClass.mem_carrier
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : ConjRootClass K L
x : L
H : carrier (mk K x) = y.carrier
⊢ mk K x = y

Tactic:
?_
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : ConjRootClass K L
H : x.carrier = y.carrier
h : ∀ (x : L) (H : carrier (mk K x) = y.carrier), mk K x = y
⊢ x = y

Tactic:
induction x with | h x => ?_
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
H : carrier (mk K x) = carrier (mk K y)
⊢ Eq (α := ConjRootClass K L) (mk K x) (mk K y)

Tactic:
?_
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : ConjRootClass K L
x : L
H : carrier (mk K x) = y.carrier
h : ∀ (y : L) (H : carrier (mk K x) = carrier (mk K y)), Eq (α := ConjRootClass K L) (mk K x) (mk K y)
⊢ mk K x = y

Tactic:
induction y with | h y => ?_
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
H : carrier (mk K x) = carrier (mk K y)
⊢ ∀ (x_1 : L), Eq (α := ConjRootClass K L) (mk K x_1) (mk K x) ↔ Eq (α := ConjRootClass K L) (mk K x_1) (mk K y)

Tactic:
simp_rw [Set.ext_iff, mem_carrier] at H

Premises used: Set.ext_iff, ConjRootClass.mem_carrier
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
H : ∀ (x_1 : L), Eq (α := ConjRootClass K L) (mk K x_1) (mk K x) ↔ Eq (α := ConjRootClass K L) (mk K x_1) (mk K y)
h h₁ : Eq (α := ConjRootClass K L) (mk K x) (mk K x)
⊢ Eq (α := ConjRootClass K L) (mk K x) (mk K y)

Tactic:
rw [← H]
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ Eq (α := ConjRootClass K L) (-mk K x) (mk K (-x))

Tactic:
rfl

Premises used: Quotient.map, Quot.map, ConjRootClass.mk, rfl
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
c : ConjRootClass K L
h : ∀ (x : L), Eq (α := ConjRootClass K L) (- -mk K x) (mk K x)
⊢ - -c = c

Tactic:
induction c
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
x : L
h : Eq (α := ConjRootClass K L) (-mk K (-x)) (mk K x)
h₁ : Eq (α := ConjRootClass K L) (mk K (- -x)) (mk K x)
h₂ h₃ : Eq (α := ConjRootClass K L) (mk K x) (mk K x)
⊢ Eq (α := ConjRootClass K L) (- -mk K x) (mk K x)

Tactic:
rw [mk_neg, mk_neg, neg_neg]

Premises used: neg_neg, ConjRootClass.mk_neg
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
c : ConjRootClass K L
h : ∀ (x : L), x ∈ (-c).carrier ↔ x ∈ -c.carrier
⊢ (-c).carrier = -c.carrier

Tactic:
ext
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
c : ConjRootClass K L
x : L
⊢ x ∈ (-c).carrier ↔ x ∈ -c.carrier

Tactic:
simp [mem_carrier, ← mk_neg, neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg, ConjRootClass.mk_neg, ConjRootClass.mem_carrier
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : ConjRootClass K L
mp : (∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0) → x = -y
mpr : x = -y → ∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0
⊢ (∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0) ↔ x = -y

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a b : L
h : a + b = 0
mp : Eq (α := ConjRootClass K L) (mk K a) (mk K (-b))
mp₁ : IsConjRoot K a (-b)
mp₂ mp₃ : IsConjRoot K (-b) (-b)
⊢ Eq (α := ConjRootClass K L) (mk K a) (-mk K b)

Tactic:
rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]

Premises used: add_eq_zero_iff_eq_neg, ConjRootClass.mk_neg, Iff.mp, ConjRootClass.mk_eq_mk
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : L
⊢ ∃ (a : L),
    Eq (α := ConjRootClass K L) (mk K a) (-mk K y) ∧
      ∃ (b : L), Eq (α := ConjRootClass K L) (mk K b) (mk K y) ∧ a + b = 0

Tactic:
⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩

Premises used: ConjRootClass.mk_neg, neg_add_cancel, And.intro, Exists.intro, Neg.neg, rfl
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : L
⊢ ∃ (a : L),
    Eq (α := ConjRootClass K L) (mk K a) (-mk K y) ∧
      ∃ (b : L), Eq (α := ConjRootClass K L) (mk K b) (mk K y) ∧ a + b = 0

Tactic:
exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : ConjRootClass K L
mpr :
  ∀ (y : L),
    ∃ (a : L),
      Eq (α := ConjRootClass K L) (mk K a) (-mk K y) ∧
        ∃ (b : L), Eq (α := ConjRootClass K L) (mk K b) (mk K y) ∧ a + b = 0
⊢ ∃ (a : L), mk K a = -y ∧ ∃ (b : L), mk K b = y ∧ a + b = 0

Tactic:
induction y with
    | h y => exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
inst_7 : Normal K L
inst_8 : DecidableEq L
inst_9 : Fintype Gal(L/K)
c : ConjRootClass K L
x : L
⊢ mk K x = c ↔ (fun (x : L) ↦ x ∈ c.carrier) x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
inst_7 : Normal K L
inst_8 : DecidableEq L
inst_9 : Fintype Gal(L/K)
c : ConjRootClass K L
x x_1 : L
⊢ Membership.mem (γ := Finset L) (Finset.image (fun (x_2 : Gal(L/K)) ↦ (x_2 : (a : L) → L) x) Finset.univ) x_1 ↔
    x_1 ∈ carrier ⟦x⟧

Tactic:
simp [← isConjRoot_iff_exists_algEquiv, ← mk_eq_mk]

Premises used: isConjRoot_iff_exists_algEquiv, ConjRootClass.mk_eq_mk
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ Eq (α := K[X]) (ConjRootClass.minpoly (mk K x)) (minpoly K x)

Tactic:
rfl

Premises used: ConjRootClass.minpoly, rfl
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
c d : ConjRootClass K L
h : ∀ (x : L), ConjRootClass.minpoly (mk K x) = d.minpoly ↔ mk K x = d
⊢ c.minpoly = d.minpoly ↔ c = d

Tactic:
induction c
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
d : ConjRootClass K L
x : L
h :
  ∀ (x_1 : L),
    Eq (α := K[X]) (ConjRootClass.minpoly (mk K x)) (ConjRootClass.minpoly (mk K x_1)) ↔
      Eq (α := ConjRootClass K L) (mk K x) (mk K x_1)
⊢ ConjRootClass.minpoly (mk K x) = d.minpoly ↔ mk K x = d

Tactic:
induction d
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x x_1 : L
⊢ Eq (α := K[X]) (ConjRootClass.minpoly (mk K x)) (ConjRootClass.minpoly (mk K x_1)) ↔
    Eq (α := ConjRootClass K L) (mk K x) (mk K x_1)

Tactic:
simp [isConjRoot_def]

Premises used: isConjRoot_def
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (α := ConjRootClass K L) ConjRootClass.minpoly

Tactic:
fun _ _ ↦ minpoly_inj.mp

Premises used: ConjRootClass.minpoly_inj, Iff.mp, Function.Injective
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n : Normal K L
c : ConjRootClass K L
h : ∀ (x : L), Splits (map (algebraMap K L) (ConjRootClass.minpoly (mk K x)))
⊢ Splits (map (algebraMap K L) c.minpoly)

Tactic:
induction c
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n : Normal K L
x : L
⊢ Splits (map (algebraMap K L) (minpoly K x))

Tactic:
n.splits _

Premises used: Normal.splits
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n : Normal K L
x : L
⊢ Splits (map (algebraMap K L) (minpoly K x))

Tactic:
exact n.splits _

Premises used: Normal.splits
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
h : ∀ (x : L), Monic (ConjRootClass.minpoly (mk K x))
⊢ c.minpoly.Monic

Tactic:
induction c
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x : L
⊢ Monic (minpoly K x)

Tactic:
minpoly.monic (Algebra.IsIntegral.isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x : L
⊢ Monic (minpoly K x)

Tactic:
exact minpoly.monic (Algebra.IsIntegral.isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ c.minpoly ≠ 0

Tactic:
c.monic_minpoly.ne_zero

Premises used: ConjRootClass.monic_minpoly, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
h : ∀ (x : L), Irreducible (M := K[X]) (ConjRootClass.minpoly (mk K x))
⊢ Irreducible c.minpoly

Tactic:
induction c
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x : L
⊢ Irreducible (M := K[X]) (minpoly K x)

Tactic:
minpoly.irreducible (Algebra.IsIntegral.isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.irreducible
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x : L
⊢ Irreducible (M := K[X]) (minpoly K x)

Tactic:
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.irreducible
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x : L
c : ConjRootClass K L
h :
  ∀ (x_1 : L),
    Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) (ConjRootClass.minpoly (mk K x_1)) : L) (0 : L) ↔
      Eq (α := ConjRootClass K L) (mk K x) (mk K x_1)
⊢ Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) c.minpoly : L) (0 : L) ↔ mk K x = c

Tactic:
induction c
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
x x_1 : L
⊢ Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) (ConjRootClass.minpoly (mk K x_1)) : L) (0 : L) ↔
    Eq (α := ConjRootClass K L) (mk K x) (mk K x_1)

Tactic:
simpa [← isConjRoot_iff_aeval_eq_zero (Algebra.IsIntegral.isIntegral _)] using comm

Premises used: Algebra.IsIntegral.isIntegral, comm, isConjRoot_iff_aeval_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
h : ∀ (x : L), x ∈ c.minpoly.rootSet L ↔ x ∈ c.carrier
⊢ c.minpoly.rootSet L = c.carrier

Tactic:
ext x
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
x : L
h : c.minpoly ≠ 0 ∧ mk K x = c ↔ mk K x = c
⊢ x ∈ c.minpoly.rootSet L ↔ x ∈ c.carrier

Tactic:
rw [mem_carrier, mem_rootSet, aeval_minpoly_iff x c]

Premises used: ConjRootClass.aeval_minpoly_iff, Polynomial.mem_rootSet, ConjRootClass.mem_carrier
-- Module: Mathlib.FieldTheory.Minpoly.ConjRootClass
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
x : L
⊢ c.minpoly ≠ 0 ∧ mk K x = c ↔ mk K x = c

Tactic:
simp [c.minpoly_ne_zero]

Premises used: ConjRootClass.minpoly_ne_zero