R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ gcd a (Finset.gcd (Finset.range (Nat.succ (max (natDegree p) (natDegree q)))) (coeff p)) = gcd a (content q)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ gcd a (content p) = gcd a (content q)
rw [content_eq_gcd_range_of_lt p (max p.natDegree q.natDegree).succ
    (lt_of_le_of_lt (le_max_left _ _) (Nat.lt_succ_self _))]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ gcd a (Finset.gcd (Finset.range (Nat.succ (max (natDegree p) (natDegree q)))) (coeff p)) =
    gcd a (Finset.gcd (Finset.range (Nat.succ (max (natDegree p) (natDegree q)))) (coeff q))
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ gcd a (Finset.gcd (Finset.range (Nat.succ (max (natDegree p) (natDegree q)))) (coeff p)) = gcd a (content q)
rw [content_eq_gcd_range_of_lt q (max p.natDegree q.natDegree).succ
    (lt_of_le_of_lt (le_max_right _ _) (Nat.lt_succ_self _))]
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ ∀ (x : ℕ), x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q))) → a ∣ coeff p x - coeff q x
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ gcd a (Finset.gcd (Finset.range (Nat.succ (max (natDegree p) (natDegree q)))) (coeff p)) =
    gcd a (Finset.gcd (Finset.range (Nat.succ (max (natDegree p) (natDegree q)))) (coeff q))
apply Finset.gcd_eq_of_dvd_sub
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
x : ℕ
a✝ : x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q)))
⊢ a ∣ coeff p x - coeff q x
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
⊢ ∀ (x : ℕ), x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q))) → a ∣ coeff p x - coeff q x
intro x _
case h.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q)))
w : (fun x => R[X]) a
hw : p - q = ↑C a * w
⊢ a ∣ coeff p x - coeff q x
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : ↑C a ∣ p - q
x : ℕ
a✝ : x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q)))
⊢ a ∣ coeff p x - coeff q x
cases' h with w hw
case h.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q)))
w : (fun x => R[X]) a
hw : p - q = ↑C a * w
⊢ coeff p x - coeff q x = a * coeff w x
case h.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q)))
w : (fun x => R[X]) a
hw : p - q = ↑C a * w
⊢ a ∣ coeff p x - coeff q x
use w.coeff x
no goals
case h.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (Nat.succ (max (natDegree p) (natDegree q)))
w : (fun x => R[X]) a
hw : p - q = ↑C a * w
⊢ coeff p x - coeff q x = a * coeff w x
rw [← coeff_sub, hw, coeff_C_mul]