case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ content p ∣ Finset.gcd (Finset.range n) (coeff p)

case hba
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ Finset.gcd (Finset.range n) (coeff p) ∣ content p
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ content p = Finset.gcd (Finset.range n) (coeff p)
apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ ∀ (b : ℕ), b ∈ Finset.range n → content p ∣ coeff p b
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ content p ∣ Finset.gcd (Finset.range n) (coeff p)
rw [Finset.dvd_gcd_iff]
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
a✝ : i ∈ Finset.range n
⊢ content p ∣ coeff p i
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ ∀ (b : ℕ), b ∈ Finset.range n → content p ∣ coeff p b
intro i _
no goals
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
a✝ : i ∈ Finset.range n
⊢ content p ∣ coeff p i
apply content_dvd_coeff _
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ support p ⊆ Finset.range n
case hba
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ Finset.gcd (Finset.range n) (coeff p) ∣ content p
apply Finset.gcd_mono
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
⊢ i ∈ support p → i ∈ Finset.range n
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
⊢ support p ⊆ Finset.range n
intro i
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
⊢ ¬coeff p i = 0 → i < n
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
⊢ i ∈ support p → i ∈ Finset.range n
simp only [Nat.lt_succ_iff, mem_support_iff, Ne.def, Finset.mem_range]
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
⊢ n ≤ i → coeff p i = 0
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
⊢ ¬coeff p i = 0 → i < n
contrapose!
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
h1 : n ≤ i
⊢ coeff p i = 0
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
⊢ n ≤ i → coeff p i = 0
intro h1
no goals
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : natDegree p < n
i : ℕ
h1 : n ≤ i
⊢ coeff p i = 0
apply coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le h h1)