R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ primPart (p * q) = primPart p * primPart q
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : p * q ≠ 0
⊢ primPart (p * q) = primPart p * primPart q
rw [Ne.def, ← content_eq_zero_iff, ← C_eq_zero] at h0
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ ↑C (content (p * q)) * primPart (p * q) = ↑C (content (p * q)) * (primPart p * primPart q)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ primPart (p * q) = primPart p * primPart q
apply mul_left_cancel₀ h0
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ ↑C (content p) * primPart p * (↑C (content q) * primPart q) = ↑C (content (p * q)) * (primPart p * primPart q)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ ↑C (content (p * q)) * primPart (p * q) = ↑C (content (p * q)) * (primPart p * primPart q)
conv_lhs =>
  rw [← (p * q).eq_C_content_mul_primPart, p.eq_C_content_mul_primPart,
    q.eq_C_content_mul_primPart]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ ↑C (content p) * primPart p * (↑C (content q) * primPart q) =
    ↑C (content p) * ↑C (content q) * (primPart p * primPart q)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ ↑C (content p) * primPart p * (↑C (content q) * primPart q) = ↑C (content (p * q)) * (primPart p * primPart q)
rw [content_mul, RingHom.map_mul]
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0✝ : ¬p * q = 0
h0 : ¬↑C (content (p * q)) = 0
⊢ ↑C (content p) * primPart p * (↑C (content q) * primPart q) =
    ↑C (content p) * ↑C (content q) * (primPart p * primPart q)
ring