R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ content p ↔ ∀ (i : ℕ), r ∣ coeff p i
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ content p ↔ ↑C r ∣ p
rw [C_dvd_iff_dvd_coeff]
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ content p → ∀ (i : ℕ), r ∣ coeff p i

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ (∀ (i : ℕ), r ∣ coeff p i) → r ∣ content p
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ content p ↔ ∀ (i : ℕ), r ∣ coeff p i
constructor
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ content p
i : ℕ
⊢ r ∣ coeff p i
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ content p → ∀ (i : ℕ), r ∣ coeff p i
intro h i
no goals
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ content p
i : ℕ
⊢ r ∣ coeff p i
apply h.trans (content_dvd_coeff _)
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ coeff p i
⊢ r ∣ content p
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ (∀ (i : ℕ), r ∣ coeff p i) → r ∣ content p
intro h
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ coeff p i
⊢ ∀ (b : ℕ), b ∈ support p → r ∣ coeff p b
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ coeff p i
⊢ r ∣ content p
rw [content, Finset.dvd_gcd_iff]
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ coeff p i
i : ℕ
a✝ : i ∈ support p
⊢ r ∣ coeff p i
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ coeff p i
⊢ ∀ (b : ℕ), b ∈ support p → r ∣ coeff p b
intro i _
no goals
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ coeff p i
i : ℕ
a✝ : i ∈ support p
⊢ r ∣ coeff p i
apply h i