case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
integral : IsIntegral R x
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J
obtain ⟨p, p_monic, hpx⟩ := integral
case intro.intro.refine'_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ R[X]

case intro.intro.refine'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ Polynomial.map (Quotient.mk (comap (algebraMap R S) I)) ?intro.intro.refine'_1 ≠ 0

case intro.intro.refine'_3
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x ?intro.intro.refine'_1 ∈ I
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J
refine' comap_lt_comap_of_root_mem_sdiff hIJ mem _ _
case intro.intro.refine'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ Polynomial.map (Quotient.mk (comap (algebraMap R S) I)) ?intro.intro.refine'_1 ≠ 0

case intro.intro.refine'_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ R[X]

case intro.intro.refine'_3
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x ?intro.intro.refine'_1 ∈ I
case intro.intro.refine'_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ R[X]

case intro.intro.refine'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ Polynomial.map (Quotient.mk (comap (algebraMap R S) I)) ?intro.intro.refine'_1 ≠ 0

case intro.intro.refine'_3
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x ?intro.intro.refine'_1 ∈ I
swap
no goals
case intro.intro.refine'_3
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x p ∈ I
convert I.zero_mem
no goals
case intro.intro.refine'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : Algebra R S
hI : IsPrime I
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : Monic p
hpx : eval₂ (algebraMap R S) x p = 0
⊢ Polynomial.map (Quotient.mk (comap (algebraMap R S) I)) ?intro.intro.refine'_1 ≠ 0
apply map_monic_ne_zero p_monic