awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
e :
  Eq.{u_2 + 1} (α := S)
    (∑ b ∈ Finset.range (p.natDegree + 1),
      (HMul.hMul (α := S[X])
            ((algebraMap
                    (↥(Algebra.adjoin R
                        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                    S[X] :
                  (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
                (p.coeff b) :
              S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ b)).coeff
        p.natDegree)
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ HMul.hMul (β := S) (x ^ i) ((algebraMap R S : (a : R) → S) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : S) =
    x ^ i *
      coeff
        ((algebraMap
              (↥(Algebra.adjoin R
                  {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
              S[X] :
            (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
          (p.coeff i))
        (p.natDegree - i)

Tactic:
simp [Subalgebra.algebraMap_def]

Premises used: Subalgebra.algebraMap_def
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
e :
  eval₂
      (algebraMap
        (↥(Algebra.adjoin R
            {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
        S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X) p =
    0
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
inr : ∀ (i : ℕ), q.coeff i ∈ I ^ (p.natDegree - i)
⊢ ∀ (i : ℕ), q.coeff i ∈ I ^ (q.natDegree - i)

Tactic:
rw [hq]
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
e :
  eval₂
      (algebraMap
        (↥(Algebra.adjoin R
            {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
        S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X) p =
    0
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
⊢ ∀ (i : ℕ), q.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
simp [q, apply_ite, coeff_mem_pow_of_mem_adjoin_C_mul_X (p.coeff _).2]

Premises used: apply_ite, Polynomial.coeff, Polynomial.coeff_mem_pow_of_mem_adjoin_C_mul_X, Subtype.property
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral ?_

Premises used: Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
refine :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
refine exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral ?_

Premises used: Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) 0) X)

Tactic:
simp [isIntegral_zero]

Premises used: isIntegral_zero
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
x y : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hy_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) y
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
hy :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (x + y) : S[X]) X)

Tactic:
simpa [add_mul] using hx.add hy

Premises used: add_mul, IsIntegral.add
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
x : S
h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)) x
mem :
  ∀ (x : R) (hx : x ∈ (↑I : Set R)),
    IsIntegral.{u_1, u_2}
      (↥(Algebra.adjoin R
          {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap R S : (a : R) → S) x) : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)

Tactic:
obtain ⟨x, hx, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
x : R
hx : x ∈ (↑I : Set R)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap R S : (a : R) → S) x) : S[X]) X)

Tactic:
simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)

Premises used: isIntegral_algebraMap
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
smul :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) a : S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (a • x) : S[X]) X)

Tactic:
simp only [smul_eq_mul, map_mul, mul_assoc]

Premises used: mul_assoc, map_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) a : S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))

Tactic:
.mul ?_ hx

Premises used: IsIntegral.mul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
smul :
  IsIntegral.{u_1, u_2}
    ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
    (A := S[X]) ((C : (a : S) → S[X]) a : S[X])
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) a : S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))

Tactic:
refine .mul ?_ hx
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
    (A := S[X]) ((C : (a : S) → S[X]) a : S[X])

Tactic:
((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

Premises used: Algebra.IsIntegral.isIntegral, IsScalarTower.toAlgHom, IsIntegral.map, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
    (A := S[X]) ((C : (a : S) → S[X]) a : S[X])

Tactic:
exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

Premises used: Algebra.IsIntegral.isIntegral, IsScalarTower.toAlgHom, IsIntegral.map, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
let let₁ let₂ let₃ :
  ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
let₄ :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
classical
  let A : Subalgebra R R[X] := Algebra.adjoin R { C r * X | r ∈ I }
  letI := Polynomial.algebra R S
  refine exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral ?_
  induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

Premises used: add_mul, mul_assoc, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, map_mul, smul_eq_mul, isIntegral_zero, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
obtain :
  ∀ (p : R[X]) (hp : p.Monic) (e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S))
    (h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)),
    ∃ (p : R[X]),
      p.Monic ∧
        Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I

Tactic:
obtain ⟨p, hp, e, h⟩ := exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map hx

Premises used: Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I

Tactic:
⟨p, hp, e, fun i hi ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
refine : ∀ (i : ℕ) (hi : i ≠ p.natDegree), p.coeff i ∈ I
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I

Tactic:
refine ⟨p, hp, e, fun i hi ↦ ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi : i ≠ p.natDegree
inl : ∀ (hi : i < p.natDegree), p.coeff i ∈ I
inr : ∀ (hi : p.natDegree < i), p.coeff i ∈ I
⊢ p.coeff i ∈ I

Tactic:
obtain hi | hi := hi.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi_1 : i ≠ p.natDegree
hi : i < p.natDegree
⊢ p.natDegree - i ≠ 0

Tactic:
lia
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi_1 : i ≠ p.natDegree
hi : i < p.natDegree
⊢ p.coeff i ∈ I

Tactic:
exact Ideal.pow_le_self (by lia) (h _)

Premises used: Ideal.pow_le_self
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi_1 : i ≠ p.natDegree
hi : p.natDegree < i
⊢ p.coeff i ∈ I

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
rw :
  ∀ ⦃I : Ideal R⦄,
    Membership.mem (γ := Set (Ideal R))
        {J : Ideal R | Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ J ∧ J.IsPrime} I →
      q.coeff i ∈ I
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x})) (q.coeff i)

Tactic:
rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]

Premises used: Ideal.mem_sInf, Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
a : ∀ (i : ℕ), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
⊢ map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree

Tactic:
ext i
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i_1 : ℕ
hi : i_1 ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
a :
  ∀ (hi : i < p.natDegree), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
a₁ : (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff p.natDegree
a₂ :
  ∀ (hi : p.natDegree < i), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i

Tactic:
obtain hi | rfl | hi := lt_trichotomy i p.natDegree

Premises used: Polynomial.natDegree, rfl, lt_trichotomy
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i_1 : ℕ
hi_1 : i_1 ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : i < p.natDegree
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i

Tactic:
simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using hPJ (Ideal.subset_span ⟨_, hi, rfl⟩)

Premises used: Ideal.subset_span, Ideal.Quotient.eq_zero_iff_mem, And.intro, Exists.intro, rfl, LT.lt.ne
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
⊢ (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff p.natDegree

Tactic:
simp [hp]