-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_eq_gcd_leadingCoeff_content_eraseLead (p : R[X]) :
    p.content = GCDMonoid.gcd p.leadingCoeff (eraseLead p).content

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ∈ p.support.erase p.natDegree
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
rw [Finset.mem_erase] at hi

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content,
  eraseLead_support]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] at h

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)

Tactic:
refine congr rfl (Finset.gcd_congr rfl fun i hi => ?_)

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ∈ p.support.erase p.natDegree
⊢ p.coeff i = p.eraseLead.coeff i

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
rw [eraseLead_coeff, if_neg hi.1]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
simp [h]

Result:
no goals