R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ content (↑C r) = ↑normalize r
rw [content]
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
by_cases h0 : r = 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : support (↑C r) = {0}
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
have h : (C r).support = {0} := support_monomial _ h0
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : support (↑C r) = {0}
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
simp [h]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ Finset.gcd (support (↑C r)) (coeff (↑C r)) = ↑normalize r
simp [h0]