no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
⊢ primPart p = p
rw [← one_mul p.primPart, ← C_1, ← hp.content_eq_one, ← p.eq_C_content_mul_primPart]