R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
⊢ eval₂ f s (primPart p) = 0
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s p = 0
⊢ eval₂ f s (primPart p) = 0
rw [eq_C_content_mul_primPart p, eval₂_mul, eval₂_C] at hp
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
hcont : content p ≠ 0
⊢ eval₂ f s (primPart p) = 0
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
⊢ eval₂ f s (primPart p) = 0
have hcont : p.content ≠ 0 := fun h => hpzero (content_eq_zero_iff.1 h)
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
hcont : ↑f (content p) ≠ ↑f 0
⊢ eval₂ f s (primPart p) = 0
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
hcont : content p ≠ 0
⊢ eval₂ f s (primPart p) = 0
replace hcont := Function.Injective.ne hinj hcont
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
hcont : ↑f (content p) ≠ 0
⊢ eval₂ f s (primPart p) = 0
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
hcont : ↑f (content p) ≠ ↑f 0
⊢ eval₂ f s (primPart p) = 0
rw [map_zero] at hcont
no goals
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : NormalizedGCDMonoid R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ↑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑f (content p) * eval₂ f s (primPart p) = 0
hcont : ↑f (content p) ≠ 0
⊢ eval₂ f s (primPart p) = 0
exact eq_zero_of_ne_zero_of_mul_left_eq_zero hcont hp