awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.IsSeparable K L
c : ConjRootClass K L
h : ∀ (x : L), Separable (ConjRootClass.minpoly (mk K x))
⊢ c.minpoly.Separable

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.IsSeparable K L
x : L
⊢ Separable (ConjRootClass.minpoly (mk K x))

Tactic:
Algebra.IsSeparable.isSeparable K _

Premises used: Algebra.IsSeparable.isSeparable, ConjRootClass.minpoly, IsSeparable
-- 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.IsSeparable K L
x : L
⊢ Separable (ConjRootClass.minpoly (mk K x))

Tactic:
exact Algebra.IsSeparable.isSeparable K _

Premises used: Algebra.IsSeparable.isSeparable
-- 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.IsSeparable K L
c : ConjRootClass K L
⊢ (c.minpoly.aroots L).Nodup

Tactic:
nodup_roots c.separable_minpoly.map

Premises used: ConjRootClass.separable_minpoly, Polynomial.Separable.map, Polynomial.nodup_roots
-- 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.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
simp_rw₂ : c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val
simp_rw₃ : c.minpoly.aroots L = (c.minpoly.aroots L).dedup
⊢ c.minpoly.aroots L = c.carrier.toFinset.val

Tactic:
simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]

Premises used: ConjRootClass.rootSet_minpoly_eq_carrier, Finset.toFinset_coe, Polynomial.rootSet_def, ConjRootClass.nodup_aroots_minpoly, Multiset.Nodup.dedup, Multiset.toFinset_val
-- 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.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
simp_rw : c.minpoly.aroots L = (c.minpoly.rootSet L).toFinset.val
simp_rw₁ : c.minpoly.aroots L = (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val
simp_rw₂ : c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val
simp_rw₃ : c.minpoly.aroots L = (c.minpoly.aroots L).dedup
⊢ c.minpoly.aroots L = c.carrier.toFinset.val

Tactic:
classical
  simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]

Premises used: ConjRootClass.rootSet_minpoly_eq_carrier, Finset.toFinset_coe, Polynomial.rootSet_def, Multiset.toFinset_val
-- 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.IsSeparable K L
c : ConjRootClass K L
inst_4 : Fintype (↑c.carrier : Type u_2)
⊢ c.carrier.toFinset = { val := c.minpoly.aroots L, nodup := ⋯ }

Tactic:
simp only [aroots_minpoly_eq_carrier_val]

Premises used: ConjRootClass.aroots_minpoly_eq_carrier_val
-- 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.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).dedup))
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))

Tactic:
simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]

Premises used: ConjRootClass.rootSet_minpoly_eq_carrier, Finset.toFinset_coe, Polynomial.rootSet_def, Finset.prod_eq_multiset_prod, Multiset.toFinset_val
-- 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.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
rw : (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).dedup))

Tactic:
rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]

Premises used: Iff.mpr, Multiset.dedup_eq_self, Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq, ConjRootClass.separable_minpoly, ConjRootClass.monic_minpoly, Polynomial.Separable.map, Polynomial.Monic.map, Polynomial.nodup_roots
-- 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.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
rw : Splits (map (algebraMap K L) c.minpoly)
⊢ (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)

Tactic:
rw [← splits_iff_card_roots]

Premises used: Polynomial.splits_iff_card_roots
-- 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.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
⊢ Splits (map (algebraMap K L) c.minpoly)

Tactic:
c.splits_minpoly

Premises used: ConjRootClass.splits_minpoly
-- 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.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
⊢ Splits (map (algebraMap K L) c.minpoly)

Tactic:
exact c.splits_minpoly

Premises used: ConjRootClass.splits_minpoly
-- 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.IsSeparable K L
inst_4 : Normal K L
c : ConjRootClass K L
inst_5 : Fintype (↑c.carrier : Type u_2)
simp_rw :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ (c.minpoly.rootSet L).toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
simp_rw₁ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.rootSet L).toFinset.val))
simp_rw₂ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (↑(c.minpoly.aroots L).toFinset : Set L).toFinset.val))
simp_rw₃ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).toFinset.val))
simp_rw₄ :
  Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (Multiset.prod
      (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))
        (c.minpoly.aroots L).dedup))
simp_rw₅ : (roots (map (algebraMap K L) c.minpoly)).card = natDegree (map (algebraMap K L) c.minpoly)
simp_rw₆ : Splits (map (algebraMap K L) c.minpoly)
⊢ Eq (α := L[X]) (map (algebraMap K L) c.minpoly)
    (∏ x ∈ c.carrier.toFinset, HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X]))

Tactic:
classical
  simp_rw [← rootSet_minpoly_eq_carrier, Finset.prod_eq_multiset_prod, rootSet_def,
    Finset.toFinset_coe, Multiset.toFinset_val]
  rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]
  rw [← splits_iff_card_roots]
  exact c.splits_minpoly

Premises used: Iff.mpr, Multiset.dedup_eq_self, Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq, ConjRootClass.separable_minpoly, ConjRootClass.rootSet_minpoly_eq_carrier, Finset.toFinset_coe, ConjRootClass.monic_minpoly, Polynomial.rootSet_def, ConjRootClass.splits_minpoly, Polynomial.splits_iff_card_roots, Polynomial.Separable.map, Finset.prod_eq_multiset_prod, Polynomial.Monic.map, Polynomial.nodup_roots, Multiset.toFinset_val
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)

Tactic:
simp [hp]
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
e : B
inst_3 : FiniteDimensional A B
⊢ Ne (α := A[X]) (minpoly A e) 0

Tactic:
minpoly.ne_zero <| .of_finite A _

Premises used: IsIntegral.of_finite, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
⊢ IsIntegral A x

Tactic:
have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
symm : minpoly A x = p
⊢ p = minpoly A x

Tactic:
symm
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
h : minpoly A x - p = 0
⊢ minpoly A x = p

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
h : ∀ (hnz : ¬minpoly A x - p = 0), False
⊢ minpoly A x - p = 0

Tactic:
by_contra hnz
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x - p) : B) (0 : B)

Tactic:
simp [hp]
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
h : (minpoly A x - p).degree < degree (minpoly A x)
⊢ False

Tactic:
apply degree_le_of_ne_zero A x hnz (by simp [hp]) |>.not_gt

Premises used: minpoly.degree_le_of_ne_zero, LE.le.not_gt
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
h : leadingCoeff (minpoly A x) = p.leadingCoeff
apply : degree (minpoly A x) = p.degree
⊢ (minpoly A x - p).degree < degree (minpoly A x)

Tactic:
apply degree_sub_lt _ (minpoly.ne_zero hx)

Premises used: Polynomial.degree_sub_lt, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
h : 1 = p.leadingCoeff
h₁ h₂ : Eq.{u_1 + 1} (α := A) 1 1
⊢ leadingCoeff (minpoly A x) = p.leadingCoeff

Tactic:
rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]

Premises used: minpoly.monic, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ degree (minpoly A x) = p.degree

Tactic:
le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))

Premises used: minpoly.monic, minpoly.aeval, minpoly, le_antisymm, minpoly.min
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ degree (minpoly A x) = p.degree

Tactic:
exact le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))

Premises used: minpoly.monic, minpoly.aeval, minpoly, le_antisymm, minpoly.min
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin : p.degree ≤ degree (minpoly A x)
⊢ p = minpoly A x

Tactic:
unique _ _ pmonic hp fun _ qm hq ↦ pmin.trans <| min _ _ qm hq

Premises used: minpoly.unique, minpoly.min, LE.le.trans
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pos : ∀ (hp0 : p = 0), minpoly A x ∣ p
neg : ∀ (hp0 : ¬p = 0), minpoly A x ∣ p
⊢ minpoly A x ∣ p

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : p = 0
⊢ minpoly A x ∣ p

Tactic:
simp only [hp0, dvd_zero]

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
⊢ IsIntegral A x

Tactic:
have hx : IsIntegral A x := IsAlgebraic.isIntegral ⟨p, hp0, hp⟩
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
neg : p %ₘ minpoly A x = 0
⊢ minpoly A x ∣ p

Tactic:
rw [← modByMonic_eq_zero_iff_dvd (monic hx)]

Premises used: minpoly.monic, Polynomial.modByMonic_eq_zero_iff_dvd
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
neg : ∀ (hnz : ¬p %ₘ minpoly A x = 0), False
⊢ p %ₘ minpoly A x = 0

Tactic:
by_contra hnz
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
neg : (p %ₘ minpoly A x).degree < degree (minpoly A x)
⊢ False

Tactic:
apply degree_le_of_ne_zero A x hnz
    ((aeval_modByMonic_eq_self_of_root (aeval _ _)).trans hp) |>.not_gt

Premises used: minpoly.degree_le_of_ne_zero, Polynomial.aeval_modByMonic_eq_self_of_root, minpoly.aeval, LE.le.not_gt, Eq.trans
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ (p %ₘ minpoly A x).degree < degree (minpoly A x)

Tactic:
degree_modByMonic_lt _ (monic hx)

Premises used: minpoly.monic, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ (p %ₘ minpoly A x).degree < degree (minpoly A x)

Tactic:
exact degree_modByMonic_lt _ (monic hx)

Premises used: minpoly.monic, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
h : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
rw : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x * q) : B) (0 : B)
rw₁ :
  HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
      ((Polynomial.aeval x : (a : A[X]) → B) q : B) =
    0
rw₂ : HMul.hMul (α := B) (β := B) (0 : B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := B) 0 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)

Tactic:
rw [hq, map_mul, aeval, zero_mul]

Premises used: MulZeroClass.zero_mul, minpoly.aeval, map_mul
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsReduced B
n : ℕ
p : A[X]
dvd : minpoly A x ∣ p ^ n
rw :
  ∀ (dvd : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p ^ n) : B) (0 : B)),
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ minpoly A x ∣ p

Tactic:
rw [dvd_iff] at dvd ⊢

Premises used: minpoly.dvd_iff
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsReduced B
n : ℕ
p : A[X]
dvd : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p ^ n) : B) (0 : B)
⊢ HPow.hPow (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) n = 0

Tactic:
rw [map_pow] at dvd

Premises used: map_pow
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsReduced B
n : ℕ
p : A[X]
dvd : HPow.hPow (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) n = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)

Tactic:
IsReduced.eq_zero _ ⟨n, dvd⟩

Premises used: Exists.intro, IsReduced.eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsReduced B
n : ℕ
p : A[X]
dvd : HPow.hPow (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) n = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)

Tactic:
exact IsReduced.eq_zero _ ⟨n, dvd⟩

Premises used: Exists.intro, IsReduced.eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_3
K : Type u_4
R : Type u_5
inst : CommRing A
inst_1 : Field K
inst_2 : Ring R
inst_3 : Algebra A K
inst_4 : Algebra A R
inst_5 : Algebra K R
inst_6 : IsScalarTower A K R
x : R
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (map (algebraMap A K) (minpoly A x))

Tactic:
minpoly.dvd K x ?_

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_3
K : Type u_4
R : Type u_5
inst : CommRing A
inst_1 : Field K
inst_2 : Ring R
inst_3 : Algebra A K
inst_4 : Algebra A R
inst_5 : Algebra K R
inst_6 : IsScalarTower A K R
x : R
refine : Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : K[X]) → R) (map (algebraMap A K) (minpoly A x)) : R) (0 : R)
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (map (algebraMap A K) (minpoly A x))

Tactic:
refine minpoly.dvd K x ?_

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
A : Type u_3
K : Type u_4
R : Type u_5
inst : CommRing A
inst_1 : Field K
inst_2 : Ring R
inst_3 : Algebra A K
inst_4 : Algebra A R
inst_5 : Algebra K R
inst_6 : IsScalarTower A K R
x : R
rw : Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : A[X]) → R) (minpoly A x) : R) (0 : R)
rw₁ rw₂ : Eq.{u_5 + 1} (α := R) 0 0
⊢ Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : K[X]) → R) (map (algebraMap A K) (minpoly A x)) : R) (0 : R)

Tactic:
rw [aeval_map_algebraMap, minpoly.aeval]

Premises used: Polynomial.aeval_map_algebraMap, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.Field
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
apply :
  Eq.{u_6 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
⊢ Dvd.dvd (α := K[X]) (minpoly.{u_5, u_6} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))

Tactic:
apply minpoly.dvd K (algebraMap S L s)

Premises used: Algebra.algebraMap, minpoly.dvd, DFunLike.coe