R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : q ≠ 0
h : p ∣ q
⊢ p ∣ primPart q
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : q ≠ 0
⊢ p ∣ primPart q ↔ p ∣ q
refine' ⟨fun h => h.trans (Dvd.intro_left _ q.eq_C_content_mul_primPart.symm), fun h => _⟩
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
r : R[X]
hq : p * r ≠ 0
⊢ p ∣ primPart (p * r)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : q ≠ 0
h : p ∣ q
⊢ p ∣ primPart q
rcases h with ⟨r, rfl⟩
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
r : R[X]
hq : p * r ≠ 0
⊢ p * ?m.597922 = primPart (p * r)

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
r : R[X]
hq : p * r ≠ 0
⊢ R[X]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
r : R[X]
hq : p * r ≠ 0
⊢ p ∣ primPart (p * r)
apply Dvd.intro _
no goals
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
r : R[X]
hq : p * r ≠ 0
⊢ p * ?m.597922 = primPart (p * r)

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
r : R[X]
hq : p * r ≠ 0
⊢ R[X]
rw [primPart_mul hq, hp.primPart_eq]