R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (x : ℕ), x ∈ support p → coeff p x = 0) ↔ p = 0
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ content p = 0 ↔ p = 0
rw [content, Finset.gcd_eq_zero_iff]
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
⊢ p = 0

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ ∀ (x : ℕ), x ∈ support p → coeff p x = 0
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (x : ℕ), x ∈ support p → coeff p x = 0) ↔ p = 0
constructor <;> intro h
case mp.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
⊢ coeff p n = coeff 0 n
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
⊢ p = 0
ext n
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : n ∈ support p
⊢ coeff p n = coeff 0 n

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : ¬n ∈ support p
⊢ coeff p n = coeff 0 n
case mp.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
⊢ coeff p n = coeff 0 n
by_cases h0 : n ∈ p.support
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : n ∈ support p
⊢ coeff p n = coeff 0 n
rw [h n h0, coeff_zero]
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : ¬coeff p n ≠ 0
⊢ coeff p n = coeff 0 n
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : ¬n ∈ support p
⊢ coeff p n = coeff 0 n
rw [mem_support_iff] at h0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : coeff p n = 0
⊢ coeff p n = coeff 0 n
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : ¬coeff p n ≠ 0
⊢ coeff p n = coeff 0 n
push_neg  at h0
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ (x : ℕ), x ∈ support p → coeff p x = 0
n : ℕ
h0 : coeff p n = 0
⊢ coeff p n = coeff 0 n
simp [h0]
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
x : ℕ
⊢ x ∈ support p → coeff p x = 0
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ ∀ (x : ℕ), x ∈ support p → coeff p x = 0
intro x
no goals
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
x : ℕ
⊢ x ∈ support p → coeff p x = 0
simp [h]