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

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ content p = gcd (leadingCoeff p) (content (eraseLead p))
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ content p = gcd (leadingCoeff p) (content (eraseLead p))
by_cases h : p = 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
⊢ content p = gcd (leadingCoeff p) (content (eraseLead p))
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ content p = gcd (leadingCoeff p) (content (eraseLead p))
rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne.def, ← mem_support_iff] at h
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
⊢ gcd (coeff p (natDegree p)) (Finset.gcd (Finset.erase (support p) (natDegree p)) (coeff p)) =
    gcd (coeff p (natDegree p)) (Finset.gcd (Finset.erase (support p) (natDegree p)) (coeff (eraseLead p)))
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
⊢ content p = gcd (leadingCoeff p) (content (eraseLead p))
rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content,
  eraseLead_support]
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
i : ℕ
hi : i ∈ Finset.erase (support p) (natDegree p)
⊢ coeff p i = coeff (eraseLead p) i
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
⊢ gcd (coeff p (natDegree p)) (Finset.gcd (Finset.erase (support p) (natDegree p)) (coeff p)) =
    gcd (coeff p (natDegree p)) (Finset.gcd (Finset.erase (support p) (natDegree p)) (coeff (eraseLead p)))
refine' congr rfl (Finset.gcd_congr rfl fun i hi => _)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
i : ℕ
hi : i ≠ natDegree p ∧ i ∈ support p
⊢ coeff p i = coeff (eraseLead p) i
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
i : ℕ
hi : i ∈ Finset.erase (support p) (natDegree p)
⊢ coeff p i = coeff (eraseLead p) i
rw [Finset.mem_erase] at hi
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : natDegree p ∈ support p
i : ℕ
hi : i ≠ natDegree p ∧ i ∈ support p
⊢ coeff p i = coeff (eraseLead p) i
rw [eraseLead_coeff, if_neg hi.1]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ content p = gcd (leadingCoeff p) (content (eraseLead p))
simp [h]