-- Mathlib/RingTheory/Polynomial/Content.lean
theorem aeval_primPart_eq_zero {S : Type*} [Ring S] [IsDomain S] [Algebra R S]
    [NoZeroSMulDivisors R S] {p : R[X]} {s : S} (hpzero : p ≠ 0) (hp : aeval s p = 0) :
    aeval s p.primPart = 0

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
hcont : (algebraMap R S) p.content ≠ (algebraMap R S) 0
⊢ (aeval s) p.primPart = 0

Tactic:
rw [map_zero] at hcont

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
hcont : (algebraMap R S) p.content ≠ 0
⊢ (aeval s) p.primPart = 0

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
hcont : (algebraMap R S) p.content ≠ 0
⊢ (aeval s) p.primPart = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_left_eq_zero hcont hp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
⊢ (aeval s) p.primPart = 0

Tactic:
have hcont : p.content ≠ 0 := fun h => hpzero (content_eq_zero_iff.1 h)

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
hcont : p.content ≠ 0
⊢ (aeval s) p.primPart = 0

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (aeval s) p = 0
⊢ (aeval s) p.primPart = 0

Tactic:
rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
⊢ (aeval s) p.primPart = 0

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
hcont : p.content ≠ 0
⊢ (aeval s) p.primPart = 0

Tactic:
replace hcont := Function.Injective.ne (FaithfulSMul.algebraMap_injective R S) hcont

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0
hcont : (algebraMap R S) p.content ≠ (algebraMap R S) 0
⊢ (aeval s) p.primPart = 0