-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_eq_zero_iff {p : R[X]} : content p = 0 ↔ p = 0

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
⊢ p = 0

Tactic:
ext n

Result:
case mp.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
⊢ p.coeff n = coeff 0 n

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
x : ℕ
⊢ x ∈ p.support → p.coeff x = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : ¬p.coeff n ≠ 0
⊢ p.coeff n = coeff 0 n

Tactic:
push_neg at h0

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : p.coeff n = 0
⊢ p.coeff n = coeff 0 n

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff 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 ∈ p.support, p.coeff x = 0

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : p.coeff n = 0
⊢ p.coeff n = coeff 0 n

Tactic:
simp [h0]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : n ∈ p.support
⊢ p.coeff n = coeff 0 n

Tactic:
rw [h n h0, coeff_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = 0 ↔ p = 0

Tactic:
rw [content, Finset.gcd_eq_zero_iff]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0

Proof state:
case mp.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
⊢ p.coeff n = coeff 0 n

Tactic:
by_cases h0 : n ∈ p.support

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : n ∈ p.support
⊢ p.coeff n = coeff 0 n

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : n ∉ p.support
⊢ p.coeff n = coeff 0 n

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : n ∉ p.support
⊢ p.coeff n = coeff 0 n

Tactic:
rw [mem_support_iff] at h0

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
n : ℕ
h0 : ¬p.coeff n ≠ 0
⊢ p.coeff n = coeff 0 n

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ ∀ x ∈ p.support, p.coeff x = 0

Tactic:
intro x

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
x : ℕ
⊢ x ∈ p.support → p.coeff x = 0