-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
lemma Polynomial.Monic.quotient_isIntegral {g : S[X]} (mon : g.Monic) {I : Ideal S[X]} (h : g ∈ I) :
    ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral

Proof state:
case h.mp
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} → g ∈ ⊤

Tactic:
simp only [Algebra.mem_top, implies_true]

Result:
no goals

Proof state:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
eq_top : Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤
⊢ ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral

Tactic:
exact fun a ↦ (eq_top ▸ adjoin_le_integralClosure <| mon.quotient_isIntegralElem h)
  Algebra.mem_top

Result:
no goals

Proof state:
case h
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} ↔ g ∈ ⊤

Tactic:
constructor

Result:
case h.mp
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} → g ∈ ⊤

case h.mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Proof state:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ ∑ x ∈ Finset.range (g'.natDegree + 1), (Ideal.Quotient.mkₐ S I) (C (g'.coeff x) * X ^ x) =
    ∑ i ∈ Finset.range (g'.natDegree + 1), g'.coeff i • (Ideal.Quotient.mkₐ S I) X ^ i

Tactic:
simp only [Polynomial.C_mul', ← map_pow, map_smul]

Result:
no goals

Proof state:
case h.mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Tactic:
obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g

Result:
case h.mpr.intro
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Proof state:
case h.mpr.intro
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
this : g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Tactic:
exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))

Result:
no goals

Proof state:
case h.mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Tactic:
intro _

Result:
case h.mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Proof state:
case h.mpr.intro
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Tactic:
have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
  nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
    as_sum_range_C_mul_X_pow g', map_sum]
  simp only [Polynomial.C_mul', ← map_pow, map_smul]

Result:
case h.mpr.intro
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
this : g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X}

Proof state:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'

Tactic:
nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
  as_sum_range_C_mul_X_pow g', map_sum]

Result:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ ∑ x ∈ Finset.range (g'.natDegree + 1), (Ideal.Quotient.mkₐ S I) (C (g'.coeff x) * X ^ x) =
    ∑ i ∈ Finset.range (g'.natDegree + 1), g'.coeff i • (Ideal.Quotient.mkₐ S I) X ^ i

Proof state:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤

Tactic:
ext g

Result:
case h
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} ↔ g ∈ ⊤