R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r (divX p) * r + ↑f (coeff p 0) ∈ I
⊢ coeff p 0 ∈ comap f I
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p ∈ I
⊢ coeff p 0 ∈ comap f I
rw [← p.divX_mul_X_add, eval₂_add, eval₂_C, eval₂_mul, eval₂_X] at hp
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r (divX p) * r + ↑f (coeff p 0) ∈ I
⊢ eval₂ f r (divX p) * r ∈ I
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r (divX p) * r + ↑f (coeff p 0) ∈ I
⊢ coeff p 0 ∈ comap f I
refine' mem_comap.mpr ((I.add_mem_iff_right _).mp hp)
no goals
R : Type u_2
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r (divX p) * r + ↑f (coeff p 0) ∈ I
⊢ eval₂ f r (divX p) * r ∈ I
exact I.mul_mem_left _ hr