awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
K : Type u_3
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsIntegrallyClosed R
inst_8 : IsDomain S
inst_9 : Algebra K S
inst_10 : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ Eq (α := K[X]) (minpoly K s) (map (algebraMap R K) (minpoly R s))
have rw : Eq (α := K[X]) (minpoly K s) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L))
Tactic: rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
K : Type u_3
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsIntegrallyClosed R
inst_8 : IsDomain S
inst_9 : Algebra K S
inst_10 : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
rw : Eq (α := K[X]) (minpoly K s) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L))
⊢ Eq (α := K[X]) (minpoly K s) (map (algebraMap R K) (minpoly R s))
have rw₁ : Eq (α := K[X]) (minpoly K s) (minpoly K s)
Tactic: rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
have rw : minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣
  map (algebraMap R K) p -
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
Tactic: rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣
    map (algebraMap R K) p -
      map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
have refine_1 : Eq.{u_2 + 1} (α := L)
  (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L) (map (algebraMap R K) p) : L)
  (0 : L)
Tactic: refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
refine_1 :
  Eq.{u_2 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L) (map (algebraMap R K) p) :
      L)
    (0 : L)
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣
    map (algebraMap R K) p -
      map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
have refine_2 : minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣
  map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
Tactic: refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq.{u_2 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L) (map (algebraMap R K) p) :
      L)
    (0 : L)
have refine_1 : Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
Tactic: rw [← map_aeval_eq_aeval_map, hp, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
have refine_1 : Eq (α := R →+* L) (algebraMap R L)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
Tactic: rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
refine_1 :
  Eq (α := R →+* L) (algebraMap R L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
⊢ Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
have refine_1₁ : Eq (α := R →+* L) (algebraMap R L) (algebraMap R L)
Tactic: rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣
    map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
have refine_2 : minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (minpoly R s)
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (minpoly R s)
have refine_2 : map (algebraMap R K) (minpoly R s) ∣ map (algebraMap R K) (minpoly R s)
Tactic: rw [isIntegrallyClosed_eq_field_fractions K L hs]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly R s ∣ p
have this : minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
Tactic: have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) := by
    rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
    refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
    · rw [← map_aeval_eq_aeval_map, hp, map_zero]
      rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
    apply dvd_mul_of_dvd_left
    rw [isIntegrallyClosed_eq_field_fractions K L hs]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
this : minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
⊢ minpoly R s ∣ p
have this₁ : minpoly R s ∣ p %ₘ minpoly R s
Tactic: rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
    map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x : Algebra K L := FractionRing.liftAlgebra R L
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ minpoly R s ∣ p
have rw : p %ₘ minpoly R s = 0
Tactic: rw [← modByMonic_eq_zero_iff_dvd (minpoly.monic hs)]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
⊢ Eq (α := Ideal R[X]) (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (AlgHom.toRingHom (Polynomial.aeval s)))
    (Ideal.span {minpoly R s})
have h : ∀ (p : R[X]),
  Membership.mem (γ := Ideal R[X])
      (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (AlgHom.toRingHom (Polynomial.aeval s))) p ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
⊢ Membership.mem (γ := Ideal R[X])
      (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (AlgHom.toRingHom (Polynomial.aeval s))) p ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
have h : Eq.{u_2 + 1} (α := S) ((AlgHom.toRingHom (Polynomial.aeval s) : (a : R[X]) → S) p : S) (0 : S) ↔
  Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
Tactic: simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
h :
  Eq.{u_2 + 1} (α := S) ((AlgHom.toRingHom (Polynomial.aeval s) : (a : R[X]) → S) p : S) (0 : S) ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
⊢ Membership.mem (γ := Ideal R[X])
      (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (AlgHom.toRingHom (Polynomial.aeval s))) p ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
have h₁ : Eq.{u_2 + 1} (α := S) (((↑(Polynomial.aeval s) : R[X] →+* S) : (a : R[X]) → S) p : S) (0 : S) ↔
  Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
Tactic: simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
h :
  Eq.{u_2 + 1} (α := S) ((AlgHom.toRingHom (Polynomial.aeval s) : (a : R[X]) → S) p : S) (0 : S) ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
h₁ :
  Eq.{u_2 + 1} (α := S) (((↑(Polynomial.aeval s) : R[X] →+* S) : (a : R[X]) → S) p : S) (0 : S) ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
⊢ Membership.mem (γ := Ideal R[X])
      (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (AlgHom.toRingHom (Polynomial.aeval s))) p ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
have h₂ : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S) ↔
  Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
Tactic: simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hs : IsIntegral R s
p : R[X]
h :
  Eq.{u_2 + 1} (α := S) ((AlgHom.toRingHom (Polynomial.aeval s) : (a : R[X]) → S) p : S) (0 : S) ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
h₁ :
  Eq.{u_2 + 1} (α := S) (((↑(Polynomial.aeval s) : R[X] →+* S) : (a : R[X]) → S) p : S) (0 : S) ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
h₂ :
  Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S) ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
⊢ Membership.mem (γ := Ideal R[X])
      (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (AlgHom.toRingHom (Polynomial.aeval s))) p ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
have h₃ : minpoly R s ∣ p ↔ Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R s}) p
Tactic: simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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)
⊢ degree (minpoly R s) ≤ p.degree
have pos : ∀ (hs : ¬IsIntegral R s), degree (minpoly R s) ≤ p.degree
Tactic: by_cases! hs : ¬IsIntegral R s
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ degree (minpoly R s) ≤ p.degree
have neg : ∀ (hs : IsIntegral R s), degree (minpoly R s) ≤ p.degree
Tactic: by_cases! hs : ¬IsIntegral R s
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
have neg : LE.le (α := WithBot ℕ) (↑(natDegree (minpoly R s)) : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree (minpoly.ne_zero hs), degree_eq_natDegree hp0]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ LE.le (α := WithBot ℕ) (↑(natDegree (minpoly R s)) : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
have neg : natDegree (minpoly R s) ≤ p.natDegree
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ IsUnit p.leadingCoeff
have 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
Tactic: obtain ⟨p, rfl⟩ := isIntegrallyClosed_dvd int_x hp
Cleared hypotheses: p, hirr, hp
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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 (minpoly R x * p).leadingCoeff
have rw : IsUnit p.leadingCoeff
Tactic: rw [leadingCoeff_mul, monic int_x, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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
⊢ P = minpoly R s
have hs : IsIntegral R s
Tactic: have hs : IsIntegral R s := ⟨P, hmo, hP⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ P = minpoly R s
have symm : minpoly R s = P
Tactic: symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ minpoly R s = P
have h : minpoly R s - P = 0
Tactic: apply eq_of_sub_eq_zero
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ minpoly R s - P = 0
have h : ∀ (hnz : ¬minpoly R s - P = 0), False
Tactic: by_contra hnz
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ False
have h : (minpoly R s - P).degree < degree (minpoly R s)
Tactic: refine IsIntegrallyClosed.degree_le_of_ne_zero (s := s) hnz (by simp [hP]) |>.not_gt ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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)
have h : degree (minpoly R s) = P.degree
Tactic: refine degree_sub_lt ?_ (ne_zero hs) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ (minpoly R s - P).degree < degree (minpoly R s)
have h₁ : leadingCoeff (minpoly R s) = P.leadingCoeff
Tactic: refine degree_sub_lt ?_ (ne_zero hs) ?_