R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd (leadingCoeff p) (content (eraseLead (p * q))) = gcd (leadingCoeff p) (content (eraseLead p * q))
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd (content (eraseLead (p * q))) (leadingCoeff p) = gcd (content (eraseLead p * q)) (leadingCoeff p)
rw [gcd_comm (content _) _, gcd_comm (content _) _]
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ↑C (leadingCoeff p) ∣ eraseLead (p * q) - eraseLead p * q
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd (leadingCoeff p) (content (eraseLead (p * q))) = gcd (leadingCoeff p) (content (eraseLead p * q))
apply gcd_content_eq_of_dvd_sub
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ↑C (leadingCoeff p) ∣
    ↑C (leadingCoeff p) * (X ^ natDegree p * q) - ↑C (leadingCoeff p) * (↑C (leadingCoeff q) * X ^ natDegree (p * q))
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ↑C (leadingCoeff p) ∣ eraseLead (p * q) - eraseLead p * q
rw [← self_sub_C_mul_X_pow, ← self_sub_C_mul_X_pow, sub_mul, sub_sub, add_comm, sub_add,
  sub_sub_cancel, leadingCoeff_mul, RingHom.map_mul, mul_assoc, mul_assoc]
no goals
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ↑C (leadingCoeff p) ∣
    ↑C (leadingCoeff p) * (X ^ natDegree p * q) - ↑C (leadingCoeff p) * (↑C (leadingCoeff q) * X ^ natDegree (p * q))
apply dvd_sub (Dvd.intro _ rfl) (Dvd.intro _ rfl)