-- Mathlib/RingTheory/Polynomial/Content.lean
theorem gcd_content_eq_of_dvd_sub {a : R} {p q : R[X]} (h : C a ∣ p - q) :
    GCDMonoid.gcd a p.content = GCDMonoid.gcd a q.content

Proof state:
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 p.content = gcd a q.content

Tactic:
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 _))]

Result:
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.range (p.natDegree ⊔ q.natDegree).succ).gcd p.coeff) = gcd a q.content

Proof state:
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.range (p.natDegree ⊔ q.natDegree).succ).gcd p.coeff) = gcd a q.content

Tactic:
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 _))]

Result:
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.range (p.natDegree ⊔ q.natDegree).succ).gcd p.coeff) =
    gcd a ((Finset.range (p.natDegree ⊔ q.natDegree).succ).gcd q.coeff)

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (p.natDegree ⊔ q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ p.coeff x - q.coeff x = a * w.coeff x

Tactic:
rw [← coeff_sub, hw, coeff_C_mul]

Result:
no goals

Proof state:
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 (p.natDegree ⊔ q.natDegree).succ
⊢ a ∣ p.coeff x - q.coeff x

Tactic:
obtain ⟨w, hw⟩ := h

Result:
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 (p.natDegree ⊔ q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ a ∣ p.coeff x - q.coeff x

Proof state:
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 ∈ Finset.range (p.natDegree ⊔ q.natDegree).succ, a ∣ p.coeff x - q.coeff x

Tactic:
intro x _

Result:
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 (p.natDegree ⊔ q.natDegree).succ
⊢ a ∣ p.coeff x - q.coeff x

Proof state:
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 (p.natDegree ⊔ q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ a ∣ p.coeff x - q.coeff x

Tactic:
use w.coeff x

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (p.natDegree ⊔ q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ p.coeff x - q.coeff x = a * w.coeff x

Proof state:
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.range (p.natDegree ⊔ q.natDegree).succ).gcd p.coeff) =
    gcd a ((Finset.range (p.natDegree ⊔ q.natDegree).succ).gcd q.coeff)

Tactic:
apply Finset.gcd_eq_of_dvd_sub

Result:
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 ∈ Finset.range (p.natDegree ⊔ q.natDegree).succ, a ∣ p.coeff x - q.coeff x