awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
f_aeval :
  Eq.{u_2 + 1} (α := Module.End A B)
    (((Polynomial.aeval ((Algebra.lmul A B : (a : B) → Module.End A B) x) :
            AlgHom.{u_1, u_1, u_2} A A[X] (Module.End A B)) :
          (a : A[X]) → Module.End A B)
        f :
      Module.End A B)
    (0 : Module.End A B)
refine : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)
⊢ natDegree (minpoly A x) ≤ Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤

Tactic:
refine f_deg ▸ (natDegree_le_natDegree <| minpoly.min _ _ f_monic ?_)
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
f_aeval :
  Eq.{u_2 + 1} (α := Module.End A B)
    (((Polynomial.aeval ((Algebra.lmul A B : (a : B) → Module.End A B) x) :
            AlgHom.{u_1, u_1, u_2} A A[X] (Module.End A B)) :
          (a : A[X]) → Module.End A B)
        f :
      Module.End A B)
    (0 : Module.End A B)
⊢ Eq (α := Module.End A B)
    ((Algebra.lmul A B : (a : B) → Module.End A B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) : Module.End A B)
    (0 : Module.End A B)

Tactic:
rw [aeval_algHom_apply] at f_aeval

Premises used: Polynomial.aeval_algHom_apply
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
f_aeval :
  Eq (α := Module.End A B)
    ((Algebra.lmul A B : (a : B) → Module.End A B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) : Module.End A B)
    (0 : Module.End A B)
⊢ Eq (α := Module.End A B)
    ((Algebra.lmul A B : (a : B) → Module.End A B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) : Module.End A B)
    ((Algebra.lmul A B : (a : B) → Module.End A B) 0 : Module.End A B)

Tactic:
simpa using f_aeval
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = Submodule.spanFinrank.{u_2, u_1} (R := A) (M := B) ⊤
f_aeval :
  Eq (α := Module.End A B)
    ((Algebra.lmul A B : (a : B) → Module.End A B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) : Module.End A B)
    (0 : Module.End A B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)

Tactic:
exact Algebra.lmul_injective (R := A) <| by simpa using f_aeval

Premises used: Algebra.lmul_injective
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
inst_4 : Module.Free A B
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
inst_4 : Module.Free A B
h : Nontrivial A
⊢ natDegree (minpoly A x) ≤ Module.finrank A B

Tactic:
simpa [Module.finrank_eq_spanFinrank_of_free] using natDegree_le_spanFinrank A x

Premises used: minpoly.natDegree_le_spanFinrank, Module.finrank_eq_spanFinrank_of_free
-- Module: Mathlib.FieldTheory.Minpoly.Finite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
x : B
inst_4 : Module.Free A B
⊢ degree (minpoly A x) ≤ (↑(Module.finrank A B) : WithBot ℕ)

Tactic:
degree_le_of_natDegree_le <| natDegree_le x

Premises used: Polynomial.degree_le_of_natDegree_le, minpoly.natDegree_le
-- 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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Eq (α := K[X]) (minpoly.{u_3, u_4} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))

Tactic:
(eq_of_irreducible_of_monic ?_ ?_ ?_).symm

Premises used: minpoly.eq_of_irreducible_of_monic, Eq.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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_1 : Irreducible (M := K[X]) (map (algebraMap R K) (minpoly R s))
refine_2 :
  Eq.{u_4 + 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)
refine_3 : Monic (map (algebraMap R K) (minpoly R s))
⊢ Eq (α := K[X]) (minpoly.{u_3, u_4} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))

Tactic:
refine (eq_of_irreducible_of_monic ?_ ?_ ?_).symm

Premises used: minpoly.eq_of_irreducible_of_monic, Eq.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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Irreducible (M := K[X]) (map (algebraMap R K) (minpoly R s))

Tactic:
((monic hs).irreducible_iff_irreducible_map_fraction_map).1 (irreducible hs)

Premises used: minpoly.monic, Iff.mp, Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map, minpoly.irreducible
-- 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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Irreducible (M := K[X]) (map (algebraMap R K) (minpoly R s))

Tactic:
exact ((monic hs).irreducible_iff_irreducible_map_fraction_map).1 (irreducible hs)

Premises used: minpoly.monic, Iff.mp, Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map, minpoly.irreducible
-- 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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
refine_2 :
  Eq.{u_4 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : R[X] →ₐ[R] L) : (a : R[X]) → L) (minpoly R s) : L) (0 : L)
refine_2₁ :
  Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) ((Polynomial.aeval s : (a : R[X]) → S) (minpoly R s) : S) : L)
    (0 : L)
refine_2₂ : Eq.{u_4 + 1} (α := L) ((algebraMap S L : (a : S) → L) 0 : L) (0 : L)
refine_2₃ refine_2₄ : Eq.{u_4 + 1} (α := L) 0 0
⊢ Eq.{u_4 + 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)

Tactic:
rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]

Premises used: Polynomial.aeval_map_algebraMap, map_zero, minpoly.aeval, Polynomial.aeval_algebraMap_apply
-- 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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Monic (map (algebraMap R K) (minpoly R s))

Tactic:
(monic hs).map _

Premises used: minpoly.monic, Polynomial.Monic.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
K : Type u_3
L : Type u_4
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : CommRing L
inst_8 : Nontrivial L
inst_9 : Algebra R L
inst_10 : Algebra S L
inst_11 : Algebra K L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
inst_14 : IsIntegrallyClosed R
inst_15 : IsDomain S
s : S
hs : IsIntegral R s
⊢ Monic (map (algebraMap R K) (minpoly R s))

Tactic:
exact (monic hs).map _

Premises used: minpoly.monic, Polynomial.Monic.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
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))
rw₁ rw₂ : Eq (α := K[X]) (minpoly K s) (minpoly K s)
⊢ Eq (α := K[X]) (minpoly K s) (map (algebraMap R K) (minpoly R s))

Tactic:
rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]

Premises used: IsFractionRing.injective, minpoly.isIntegrallyClosed_eq_field_fractions, minpoly.algebraMap_eq
-- 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
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
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))
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (p %ₘ minpoly R s)

Tactic:
rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]

Premises used: minpoly.monic, Polynomial.map_modByMonic, Polynomial.modByMonic_eq_sub_mul_div
-- 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
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))

Tactic:
dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_

Premises used: Algebra.algebraMap, dvd_sub, minpoly.dvd, DFunLike.coe
-- 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
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)
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))
⊢ 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:
refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_

Premises used: Algebra.algebraMap, dvd_sub, minpoly.dvd, DFunLike.coe
-- 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
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) (RingHom.comp (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
⊢ 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:
rw [← map_aeval_eq_aeval_map, hp, map_zero]

Premises used: map_zero, Polynomial.map_aeval_eq_aeval_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
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))
refine_1₁ refine_1₂ : Eq (α := R →+* L) (algebraMap R L) (algebraMap R L)
⊢ Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))

Tactic:
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq
-- 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
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_2 : minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (minpoly R s)
⊢ 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:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- 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
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_2 refine_2₁ : map (algebraMap R K) (minpoly R s) ∣ map (algebraMap R K) (minpoly R s)
⊢ minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L) ∣ map (algebraMap R K) (minpoly R s)

Tactic:
rw [isIntegrallyClosed_eq_field_fractions K L hs]

Premises used: minpoly.isIntegrallyClosed_eq_field_fractions
-- 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
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)

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]
-- 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
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 %ₘ 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

Premises used: minpoly.monic, Algebra.algebraMap, IsFractionRing.injective, minpoly.isIntegrallyClosed_eq_field_fractions, Polynomial.map_dvd_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
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
rw : p %ₘ minpoly R s = 0
⊢ minpoly R s ∣ p

Tactic:
rw [← modByMonic_eq_zero_iff_dvd (minpoly.monic hs)]

Premises used: minpoly.monic, Polynomial.modByMonic_eq_zero_iff_dvd
-- 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
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
⊢ p %ₘ minpoly R s = 0

Tactic:
Polynomial.eq_zero_of_dvd_of_degree_lt this (degree_modByMonic_lt p <| minpoly.monic hs)

Premises used: minpoly.monic, Polynomial.degree_modByMonic_lt, Polynomial.eq_zero_of_dvd_of_degree_lt
-- 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
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
⊢ p %ₘ minpoly R s = 0

Tactic:
exact Polynomial.eq_zero_of_dvd_of_degree_lt this (degree_modByMonic_lt p <| minpoly.monic hs)

Premises used: minpoly.monic, Polynomial.degree_modByMonic_lt, Polynomial.eq_zero_of_dvd_of_degree_lt
-- 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
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)

Tactic:
simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom,
      Function.comp_apply, eval_map_algebraMap] using
      aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)

Premises used: RingHom.mem_ker, minpoly.aeval, Polynomial.coe_mapRingHom, Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero, RingHom.coe_comp, Polynomial.eval_map_algebraMap, Function.comp_apply, Polynomial.coe_evalRingHom
-- 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
hs : IsIntegral R s
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
⊢ 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})

Tactic:
ext p
-- 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
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
h₃ : minpoly R s ∣ p ↔ 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

Tactic:
simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]

Premises used: AlgHom.coe_toRingHom, RingHom.mem_ker, minpoly.isIntegrallyClosed_dvd_iff, AlgHom.toRingHom_eq_coe, Ideal.mem_span_singleton