case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p ∣ q
⊢ content p ∣ content q ∧ primPart p ∣ primPart q

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : content p ∣ content q ∧ primPart p ∣ primPart q
⊢ p ∣ q
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p ∣ q ↔ content p ∣ content q ∧ primPart p ∣ primPart q
constructor <;> intro h
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ content p ∣ content (p * r) ∧ primPart p ∣ primPart (p * r)
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p ∣ q
⊢ content p ∣ content q ∧ primPart p ∣ primPart q
rcases h with ⟨r, rfl⟩
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ content p ∣ content p * content r ∧ primPart p ∣ p * r
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ content p ∣ content (p * r) ∧ primPart p ∣ primPart (p * r)
rw [content_mul, p.isPrimitive_primPart.dvd_primPart_iff_dvd hq]
no goals
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ content p ∣ content p * content r ∧ primPart p ∣ p * r
exact ⟨Dvd.intro _ rfl, p.primPart_dvd.trans (Dvd.intro _ rfl)⟩
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : content p ∣ content q ∧ primPart p ∣ primPart q
⊢ ↑C (content p) * primPart p ∣ ↑C (content q) * primPart q
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : content p ∣ content q ∧ primPart p ∣ primPart q
⊢ p ∣ q
rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
no goals
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : content p ∣ content q ∧ primPart p ∣ primPart q
⊢ ↑C (content p) * primPart p ∣ ↑C (content q) * primPart q
exact mul_dvd_mul (RingHom.map_dvd C h.1) h.2