-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
lemma comp_eq_zero_iff [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q = C (q.coeff 0)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0

Tactic:
rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p = 0
⊢ p.comp q = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key

Result:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
⊢ p.comp q = 0

Tactic:
rw [h.2, comp_C, h.1, C_0]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
exact Or.inr ⟨h, key⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ p.comp q = 0 ↔ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
rw [key, comp_C, C_eq_zero] at h

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
rw [key, C_comp] at h

Result:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : C (p.coeff 0) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : C (p.coeff 0) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
exact Or.inl (key.trans h)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
  rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)