case mk
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
x✝ : S ⧸ I
x : S
⊢ IsIntegralElem (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) (Quot.mk Setoid.r x)
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
⊢ IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))
rintro ⟨x⟩
case mk.intro.intro
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : Monic p
hpx : eval₂ f x p = 0
⊢ IsIntegralElem (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) (Quot.mk Setoid.r x)
case mk
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
x✝ : S ⧸ I
x : S
⊢ IsIntegralElem (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) (Quot.mk Setoid.r x)
obtain ⟨p, ⟨p_monic, hpx⟩⟩ := hf x
case mk.intro.intro
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : Monic p
hpx : eval₂ f x p = 0
⊢ eval₂ (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) (Quot.mk Setoid.r x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0
case mk.intro.intro
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : Monic p
hpx : eval₂ f x p = 0
⊢ IsIntegralElem (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) (Quot.mk Setoid.r x)
refine' ⟨p.map (Ideal.Quotient.mk _), ⟨p_monic.map _, _⟩⟩
no goals
case mk.intro.intro
R : Type u_2
A : Type ?u.1581561
B : Type ?u.1581564
S : Type u_1
T : Type ?u.1581570
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
hf : IsIntegral f
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : Monic p
hpx : eval₂ f x p = 0
⊢ eval₂ (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) (Quot.mk Setoid.r x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0
simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx