awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
pos : ∀ (hs : ¬IsIntegral R s), degree (minpoly R s) ≤ p.degree
neg : ∀ (hs : IsIntegral R s), degree (minpoly R s) ≤ p.degree
⊢ degree (minpoly R s) ≤ p.degree

Tactic:
by_cases! hs : ¬IsIntegral R s

Premises used: IsIntegral
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
hs : ¬IsIntegral R s
⊢ degree (minpoly R s) ≤ p.degree

Tactic:
simp [minpoly, hs]

Premises used: minpoly
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
hs : IsIntegral R s
neg : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly R s)) : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
⊢ degree (minpoly R s) ≤ p.degree

Tactic:
rw [degree_eq_natDegree (minpoly.ne_zero hs), degree_eq_natDegree hp0]

Premises used: Polynomial.degree_eq_natDegree, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
hs : IsIntegral R s
neg : natDegree (minpoly R s) ≤ p.natDegree
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly R s)) : WithBot ℕ) (↑p.natDegree : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
hs : IsIntegral R s
⊢ natDegree (minpoly R s) ≤ p.natDegree

Tactic:
natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0

Premises used: Polynomial.natDegree_le_of_dvd, minpoly.isIntegrallyClosed_dvd_iff, Iff.mp
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
hs : IsIntegral R s
⊢ natDegree (minpoly R s) ≤ p.natDegree

Tactic:
exact natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0

Premises used: Polynomial.natDegree_le_of_dvd, minpoly.isIntegrallyClosed_dvd_iff, Iff.mp
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
p : R[X]
hirr : Irreducible p
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) p : S) (0 : S)
int_x : IsIntegral R x
obtain :
  ∀ (p : R[X]) (hirr : Irreducible (minpoly R x * p))
    (hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (minpoly R x * p) : S) (0 : S)),
    IsUnit (minpoly R x * p).leadingCoeff
⊢ IsUnit p.leadingCoeff

Tactic:
obtain ⟨p, rfl⟩ := isIntegrallyClosed_dvd int_x hp

Premises used: minpoly.isIntegrallyClosed_dvd, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
int_x : IsIntegral R x
p : R[X]
hirr : Irreducible (minpoly R x * p)
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (minpoly R x * p) : S) (0 : S)
rw : IsUnit p.leadingCoeff
⊢ IsUnit (minpoly R x * p).leadingCoeff

Tactic:
rw [leadingCoeff_mul, monic int_x, one_mul]

Premises used: minpoly.monic, Polynomial.leadingCoeff_mul, one_mul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
int_x : IsIntegral R x
p : R[X]
hirr : Irreducible (minpoly R x * p)
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (minpoly R x * p) : S) (0 : S)
⊢ IsUnit p.leadingCoeff

Tactic:
((of_irreducible_mul hirr).resolve_left (not_isUnit R x)).map leadingCoeffHom

Premises used: Polynomial.leadingCoeffHom, Or.resolve_left, Polynomial.leadingCoeff, Polynomial.coeff, of_irreducible_mul, minpoly.not_isUnit, IsUnit.map
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
int_x : IsIntegral R x
p : R[X]
hirr : Irreducible (minpoly R x * p)
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (minpoly R x * p) : S) (0 : S)
⊢ IsUnit p.leadingCoeff

Tactic:
exact ((of_irreducible_mul hirr).resolve_left (not_isUnit R x)).map leadingCoeffHom

Premises used: Polynomial.leadingCoeffHom, Or.resolve_left, of_irreducible_mul, minpoly.not_isUnit, IsUnit.map
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
p : R[X]
hirr : Irreducible p
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) p : S) (0 : S)
isUnit : IsUnit p.leadingCoeff
⊢ IsIntegral R x

Tactic:
simpa [smul_smul] using (isIntegral_leadingCoeff_smul _ _ hp).smul ((isUnit.unit⁻¹ : Rˣ) : R)

Premises used: Units.val, smul_smul, IsIntegral.smul, Inv.inv, IsUnit.unit, isIntegral_leadingCoeff_smul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
⊢ IsIntegral R s

Tactic:
have hs : IsIntegral R s := ⟨P, hmo, hP⟩
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
symm : minpoly R s = P
⊢ P = minpoly R s

Tactic:
symm
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
h : minpoly R s - P = 0
⊢ minpoly R s = P

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
h : ∀ (hnz : ¬minpoly R s - P = 0), False
⊢ minpoly R s - P = 0

Tactic:
by_contra hnz
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) (minpoly R s - P) : S) (0 : S)

Tactic:
simp [hP]
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
h : (minpoly R s - P).degree < degree (minpoly R s)
⊢ False

Tactic:
refine IsIntegrallyClosed.degree_le_of_ne_zero (s := s) hnz (by simp [hP]) |>.not_gt ?_

Premises used: minpoly.IsIntegrallyClosed.degree_le_of_ne_zero, LE.le.not_gt
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ (minpoly R s - P).degree < degree (minpoly R s)

Tactic:
degree_sub_lt ?_ (ne_zero hs) ?_

Premises used: Polynomial.degree_sub_lt, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
h : degree (minpoly R s) = P.degree
h₁ : leadingCoeff (minpoly R s) = P.leadingCoeff
⊢ (minpoly R s - P).degree < degree (minpoly R s)

Tactic:
refine degree_sub_lt ?_ (ne_zero hs) ?_

Premises used: Polynomial.degree_sub_lt, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ degree (minpoly R s) = P.degree

Tactic:
le_antisymm (min R s hmo hP) (Pmin (minpoly R s) (monic hs) (aeval R s))

Premises used: minpoly.monic, minpoly.aeval, minpoly, le_antisymm, minpoly.min
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ degree (minpoly R s) = P.degree

Tactic:
exact le_antisymm (min R s hmo hP) (Pmin (minpoly R s) (monic hs) (aeval R s))

Premises used: minpoly.monic, minpoly.aeval, minpoly, le_antisymm, minpoly.min
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
Pmin :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
h : 1 = P.leadingCoeff
h₁ h₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ leadingCoeff (minpoly R s) = P.leadingCoeff

Tactic:
rw [(monic hs).leadingCoeff, hmo.leadingCoeff]

Premises used: minpoly.monic, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hmo : p.Monic
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
pmin : p.degree ≤ degree (minpoly R s)
⊢ p = minpoly R s

Tactic:
IsIntegrallyClosed.minpoly.unique hmo hp fun _ qm hq ↦ pmin.trans <| min _ _ qm hq

Premises used: IsIntegrallyClosed.minpoly.unique, minpoly.min, LE.le.trans
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
⊢ IsIntegral R s ↔ (C : (a : R) → R[X]) p.leadingCoeff ∣ p

Tactic:
⟨fun hInt ↦ ?_, fun ⟨q, hMul⟩ ↦ minpoly.ne_zero_iff.mp ?_⟩

Premises used: minpoly.ne_zero_iff, _private.0.minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd.match_1, IsIntegral, Iff.intro, Iff.mp
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
refine_1 : ∀ (hInt : IsIntegral R s), (C : (a : R) → R[X]) p.leadingCoeff ∣ p
refine_2 :
  (C : (a : R) → R[X]) p.leadingCoeff ∣ p →
    ∀ (q : R[X]) (hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q),
      Ne (α := R[X]) (minpoly R s) 0
⊢ IsIntegral R s ↔ (C : (a : R) → R[X]) p.leadingCoeff ∣ p

Tactic:
refine ⟨fun hInt ↦ ?_, fun ⟨q, hMul⟩ ↦ minpoly.ne_zero_iff.mp ?_⟩
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
h : p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)
⊢ (C : (a : R) → R[X]) p.leadingCoeff ∣ p

Tactic:
use minpoly R s

Premises used: minpoly
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
h :
  ∀ (q : R[X]) (hMul : p = minpoly R s * q),
    p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)
⊢ p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)

Tactic:
have ⟨q, hMul⟩ := isIntegrallyClosed_dvd hInt hp
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
this : q.degree ≤ 0
⊢ p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)

Tactic:
simp [degree_le_zero_iff.mp this ▸ hMul, minpoly.monic hInt, mul_comm]

Premises used: minpoly.monic, mul_comm
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h : q.degree ≤ 0
⊢ p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)

Tactic:
suffices q.degree ≤ 0 by simp [degree_le_zero_iff.mp this ▸ hMul, minpoly.monic hInt, mul_comm]
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h : degree (minpoly R s) + q.degree ≤ degree (minpoly R s) + 0
⊢ q.degree ≤ 0

Tactic:
apply WithBot.le_of_add_le_add_left <| Polynomial.degree_ne_bot.mpr <| minpoly.ne_zero hInt

Premises used: WithBot.le_of_add_le_add_left, Iff.mpr, Polynomial.degree_ne_bot, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ p.degree ≤ degree (minpoly R s)

Tactic:
pmin _ (minpoly.monic hInt) (minpoly.aeval ..)

Premises used: minpoly.monic, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h : degree (minpoly R s) + q.degree = p.degree
h₁ : degree (minpoly R s) + 0 = degree (minpoly R s)
⊢ degree (minpoly R s) + q.degree ≤ degree (minpoly R s) + 0

Tactic:
convert! pmin _ (minpoly.monic hInt) (minpoly.aeval ..)

Premises used: minpoly.monic, minpoly.aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h : degree (minpoly R s) + q.degree = (minpoly R s * q).degree
h₁ h₂ : degree (minpoly R s) + q.degree = degree (minpoly R s) + q.degree
⊢ degree (minpoly R s) + q.degree = p.degree

Tactic:
rw [hMul, degree_mul]

Premises used: Polynomial.degree_mul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h h₁ : degree (minpoly R s) = degree (minpoly R s)
⊢ degree (minpoly R s) + 0 = degree (minpoly R s)

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
⊢ q ≠ 0

Tactic:
right_ne_zero_of_mul <| hMul ▸ h₀

Premises used: right_ne_zero_of_mul