case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ↑C (content p) = 0
⊢ natDegree (primPart p) = natDegree p

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬↑C (content p) = 0
⊢ natDegree (primPart p) = natDegree p
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ natDegree (primPart p) = natDegree p
by_cases h : C p.content = 0
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬↑C (content p) = 0
⊢ natDegree (primPart p) = natDegree p
conv_rhs =>
  rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ natDegree (primPart p) = natDegree p
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ↑C (content p) = 0
⊢ natDegree (primPart p) = natDegree p
rw [C_eq_zero, content_eq_zero_iff] at h
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ natDegree (primPart p) = natDegree p
simp [h]