case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ content (↑C r * p) = ↑normalize r * content p

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ content (↑C r * p) = ↑normalize r * content p
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
⊢ content (↑C r * p) = ↑normalize r * content p
by_cases h0 : r = 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r * p)) (coeff (↑C r * p)) = ↑normalize r * content p
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ content (↑C r * p) = ↑normalize r * content p
rw [content]
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r * p)) (coeff (↑C r * p)) = ↑normalize r * Finset.gcd (support p) (coeff p)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r * p)) (coeff (↑C r * p)) = ↑normalize r * content p
rw [content]
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r * p)) (coeff (↑C r * p)) = Finset.gcd (support p) fun x => r * coeff p x
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r * p)) (coeff (↑C r * p)) = ↑normalize r * Finset.gcd (support p) (coeff p)
rw [← Finset.gcd_mul_left]
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ Finset.gcd (support (↑C r * p)) (coeff (↑C r * p)) = Finset.gcd (support p) fun x => r * coeff p x
refine' congr (congr rfl _) _ <;> ext <;> simp [h0, mem_support_iff]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ content (↑C r * p) = ↑normalize r * content p
simp [h0]