-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_eq_gcd_range_of_lt (p : R[X]) (n : ℕ) (h : p.natDegree < n) :
    p.content = (Finset.range n).gcd p.coeff

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

Tactic:
apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd

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

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

Proof state:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.support ⊆ Finset.range n

Tactic:
intro i

Result:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ i ∈ p.support → i ∈ Finset.range n

Proof state:
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
a✝ : i ∈ Finset.range n
⊢ p.content ∣ p.coeff i

Tactic:
apply content_dvd_coeff _

Result:
no goals

Proof state:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ n ≤ i → p.coeff i = 0

Tactic:
intro h1

Result:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
h1 : n ≤ i
⊢ p.coeff i = 0

Proof state:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ ¬p.coeff i = 0 → i < n

Tactic:
contrapose!

Result:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ n ≤ i → p.coeff i = 0

Proof state:
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∀ b ∈ Finset.range n, p.content ∣ p.coeff b

Tactic:
intro i _

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

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

Tactic:
rw [Finset.dvd_gcd_iff]

Result:
case hab
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∀ b ∈ Finset.range n, p.content ∣ p.coeff b

Proof state:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ i ∈ p.support → i ∈ Finset.range n

Tactic:
simp only [Nat.lt_succ_iff, mem_support_iff, Ne, Finset.mem_range]

Result:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ ¬p.coeff i = 0 → i < n

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

Tactic:
apply Finset.gcd_mono

Result:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.support ⊆ Finset.range n

Proof state:
case hba.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
h1 : n ≤ i
⊢ p.coeff i = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le h h1)

Result:
no goals