case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : content p = 0
⊢ normUnit (content p) = 1

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ normUnit (content p) = 1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ normUnit (content p) = 1
by_cases hp0 : p.content = 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ normUnit (content p) = 1
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : content p = 0
⊢ normUnit (content p) = 1

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ normUnit (content p) = 1
. simp [hp0]
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ normUnit (content p) = 1
. ext
  apply mul_left_cancel₀ hp0
  erw [← normalize_apply, normalize_content, mul_one]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : content p = 0
⊢ normUnit (content p) = 1
simp [hp0]
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ ↑(normUnit (content p)) = ↑1
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ normUnit (content p) = 1
ext
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ content p * ↑(normUnit (content p)) = content p * ↑1
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ ↑(normUnit (content p)) = ↑1
apply mul_left_cancel₀ hp0
no goals
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬content p = 0
⊢ content p * ↑(normUnit (content p)) = content p * ↑1
erw [← normalize_apply, normalize_content, mul_one]